helm/ocaml/cic_disambiguation/parser.ml

   1
   2 open Ast
   3
   4 let grammar = Grammar.gcreate Lexer.lex
   5
   6 let term = Grammar.Entry.create grammar "term"
   7 (* let tactic = Grammar.Entry.create grammar "tactic" *)
   8 (* let tactical = Grammar.Entry.create grammar "tactical" *)
   9
  10 let return_term loc term = LocatedTerm (loc, term)
  11
  12 EXTEND
  13   GLOBAL: term;
  14   meta_subst: [
  15     [ s = SYMBOL "_" -> None
  16     | t = term -> Some t ]
  17   ];
  18   binder: [
  19     [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
  20     | SYMBOL <:unicode<pi>> (* π *) -> `Pi
  21     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
  22     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
  23     ]
  24   ];
  25   substituted_name: [ (* a subs.name is an explicit substitution subject *)
  26     [ s = [ IDENT | SYMBOL ];
  27       subst = OPT [
  28         SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
  29         LPAREN "[";
  30         substs = LIST1 [
  31           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
  32         ] SEP SYMBOL ";";
  33         RPAREN "]" ->
  34           substs
  35       ] ->
  36         (match subst with
  37         | Some l -> Ident (s, l)
  38         | None -> Ident (s, []))
  39     ]
  40   ];
  41   name: [ (* as substituted_name with no explicit substitution *)
  42     [ s = [ IDENT | SYMBOL ] -> s ]
  43   ];
  44   pattern: [
  45     [ n = name -> [n]
  46     | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ]
  47   ];
  48   term:
  49     [ "add" LEFTA   [ (* nothing here by default *) ]
  50     | "mult" LEFTA  [ (* nothing here by default *) ]
  51     | "inv" NONA    [ (* nothing here by default *) ]
  52     | "simple" NONA
  53       [
  54         b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
  55         typ = OPT [ SYMBOL ":"; t = term -> t ];
  56         SYMBOL "."; body = term ->
  57           let binder =
  58             List.fold_right (fun var body -> Binder (b, var, typ, body))
  59               vars body
  60           in
  61           return_term loc binder
  62       | n = substituted_name -> return_term loc n
  63       | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
  64           return_term loc (Appl (head :: args))
  65       | i = INT -> return_term loc (Int (int_of_string i))
  66       | m = META;
  67         substs = [
  68           LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" ->
  69             substs
  70         ] ->
  71             return_term loc (Meta (m, substs))
  72         (* actually "in" and "and" are _not_ keywords. Parsing works anyway
  73          * since applications are required to be bound by parens *)
  74       | "let"; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *); t1 = term;
  75         IDENT "in"; t2 = term ->
  76           return_term loc (LetIn (name, t1, t2))
  77       | "let"; "rec"; defs = LIST1 [
  78           name = IDENT;
  79           index = OPT [ LPAREN "("; index = INT; RPAREN ")" ->
  80             int_of_string index
  81           ];
  82           typ = OPT [ SYMBOL ":"; typ = term -> typ ];
  83           SYMBOL <:unicode<def>> (* ≝ *); t1 = term ->
  84             (name, t1, typ, (match index with None -> 1 | Some i -> i))
  85         ] SEP (IDENT "and");
  86         IDENT "in"; body = term ->
  87           return_term loc (LetRec (defs, body))
  88       | typ = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ];
  89         "match"; t = term; "with";
  90         LPAREN "[";
  91         patterns = LIST0 [
  92           p = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒*); t = term -> (p, t)
  93         ] SEP SYMBOL "|";
  94         RPAREN "]" ->
  95           return_term loc (Case (t, typ, patterns))
  96       | LPAREN "("; t = term; RPAREN ")" -> return_term loc t
  97       ]
  98     ];
  99 END
 100
 101 let parse_term = Grammar.Entry.parse term
 102