blob: d3eb22fe11545ff9faee3f339cb6380641c62795 (
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
49
50
51
52
53
54
55
|
(****************************************************************************)
(* *)
(* OCaml *)
(* *)
(* INRIA Rocquencourt *)
(* *)
(* Copyright 2007 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 *)
open Camlp4.PreCast;;
module CamlSyntax = Camlp4OCamlParser.Make(Camlp4OCamlRevisedParser.Make(Syntax));;
let expr_of_string = CamlSyntax.Gram.parse_string CamlSyntax.expr_eoi;;
module LambdaGram = MakeGram(Lexer);;
let term = LambdaGram.Entry.mk "term";;
let term_eoi = LambdaGram.Entry.mk "lambda term quotation";;
Camlp4_config.antiquotations := true;;
EXTEND LambdaGram
GLOBAL: term term_eoi;
term:
[ "top"
[ "fun"; v = var; "->"; t = term -> <:expr< `Lam($v$, $t$) >> ]
| "app"
[ t1 = SELF; t2 = SELF -> <:expr< `App($t1$, $t2$) >> ]
| "simple"
[ `ANTIQUOT((""|"term"), a) -> expr_of_string _loc a
| v = var -> <:expr< `Var($v$) >>
| "("; t = term; ")" -> t ]
];
var:
[[ v = LIDENT -> <:expr< $str:v$ >>
| `ANTIQUOT((""|"var"), a) -> expr_of_string _loc a
]];
term_eoi:
[[ t = term; `EOI -> t ]];
END;;
let expand_lambda_quot_expr loc _loc_name_opt quotation_contents =
LambdaGram.parse_string term_eoi loc quotation_contents;;
(* to have this syntax <:lam< fun k -> k >> *)
Syntax.Quotation.add "lam" Syntax.Quotation.DynAst.expr_tag expand_lambda_quot_expr;;
Syntax.Quotation.default := "lam";;
|
