code/caml-lambda/q_lambda.ml

   1 (* Please keep me in sync with brion.inria.fr/gallium/index.php/Lambda_calculus_quotations *)
   2
   3 open Camlp4.PreCast;;
   4 module CamlSyntax = Camlp4OCamlParser.Make(Camlp4OCamlRevisedParser.Make(Syntax));;
   5
   6 let expr_of_string = CamlSyntax.Gram.parse_string CamlSyntax.expr_eoi;;
   7
   8 module LambdaGram = MakeGram(Lexer);;
   9
  10 let term = LambdaGram.Entry.mk "term";;
  11 let term_eoi = LambdaGram.Entry.mk "lambda term quotation";;
  12
  13 Camlp4_config.antiquotations := true;;
  14
  15 EXTEND LambdaGram
  16   GLOBAL: term term_eoi;
  17   term:
  18     [ "top"
  19       [ "fun"; v = var; "->"; t = term -> <:expr< `Lam(var $v$, $t$) >>
  20       | "fun"; v = var; v' = var; "->"; t = term -> <:expr< `Lam(var $v$, `Lam(var $v'$, $t$)) >>
  21       | "fun"; v = var; v' = var; v'' = var; "->"; t = term -> <:expr< `Lam(var $v$, `Lam(var $v'$, `Lam(var $v''$, $t$))) >>
  22       | "fun"; v = var; v' = var; v'' = var; v''' = var; "->"; t = term -> <:expr< `Lam(var $v$, `Lam(var $v'$, `Lam(var $v''$, `Lam(var $v'''$, $t$)))) >>
  23       | "fun"; v = var; v' = var; v'' = var; v''' = var; v'''' = var; "->"; t = term -> <:expr< `Lam(var $v$, `Lam(var $v'$, `Lam(var $v''$, `Lam(var $v'''$, `Lam(var $v''''$, $t$))))) >>
  24       ]
  25
  26     | "app"
  27       [ t1 = SELF; t2 = SELF           -> <:expr< `App($t1$, $t2$) >> ]
  28
  29     | "simple"
  30       [ `ANTIQUOT((""|"term"), a)      -> expr_of_string _loc a
  31        | v = var                        -> <:expr< `Var(var $v$) >>
  32        | "("; t = term; ")"             -> t
  33       ]
  34
  35     ];
  36   var:
  37     [[ v = LIDENT               -> <:expr< $str:v$ >>
  38      | `ANTIQUOT((""|"var"), a) -> expr_of_string _loc a
  39     ]];
  40   term_eoi:
  41     [[ t = term; `EOI -> t ]];
  42 END;;
  43
  44 let expand_lambda_quot_expr loc _loc_name_opt quotation_contents =
  45   LambdaGram.parse_string term_eoi loc quotation_contents;;
  46
  47 (* to have this syntax <:lam< fun k -> k >> *)
  48 Syntax.Quotation.add "lam" Syntax.Quotation.DynAst.expr_tag expand_lambda_quot_expr;;
  49
  50 Syntax.Quotation.default := "lam";;
  51