blob: 82ab3b8b59ee642a3e36a254062bb58c9da75a0b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
(****************************************************************************)
(* *)
(* OCaml *)
(* *)
(* INRIA Rocquencourt *)
(* *)
(* Copyright 2008 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed under *)
(* the terms of the GNU Library General Public License, with the special *)
(* exception on linking described in LICENSE at the top of the OCaml *)
(* source tree. *)
(* *)
(****************************************************************************)
(* Please keep me in sync with brion.inria.fr/gallium/index.php/Lambda_calculus_quotations *)
type term =
| Lam of var * term
| App of term * term
| Int of int
| Var of var
and var = string
module LambdaGram = Camlp4.PreCast.MakeGram(Camlp4.PreCast.Lexer);;
module Loc = Camlp4.PreCast.Loc;; (* should not be necessary when camlp4 will be fixed *)
open Camlp4.Sig;; (* from tokens *)
let term = LambdaGram.Entry.mk "term";;
let term_eoi = LambdaGram.Entry.mk "lambda term quotation";;
EXTEND LambdaGram
GLOBAL: term term_eoi;
term:
[ "top"
[ "fun"; v = var; "->"; t = term -> Lam(v, t) ]
| "app"
[ t1 = SELF; t2 = SELF -> App(t1, t2) ]
| "simple"
[ v = var -> Var(v)
| `INT(i, _) -> Int(i)
| "("; t = term; ")" -> t ]
];
var:
[[ `LIDENT v -> v ]];
term_eoi:
[[ t = term; `EOI -> t ]];
END;;
let lambda_parser = LambdaGram.parse_string term_eoi;;
|
