helm/ocaml/cic_notation/cicNotationParser.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 open CicNotationEnv
  29 open CicNotationPt
  30
  31 exception Parse_error of Token.flocation * string
  32 exception Level_not_found of int
  33
  34 let level1_pattern_grammar =
  35   Grammar.gcreate CicNotationLexer.level1_pattern_lexer
  36 let level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexer
  37 let level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
  38
  39 let min_precedence = 0
  40 let max_precedence = 100
  41
  42 let level1_pattern =
  43   Grammar.Entry.create level1_pattern_grammar "level1_pattern"
  44 let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"
  45 let term = Grammar.Entry.create level2_ast_grammar "term"
  46 let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
  47 let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
  48
  49 let return_term loc term = ()
  50
  51 let int_of_string s =
  52   try
  53     Pervasives.int_of_string s
  54   with Failure _ ->
  55     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
  56
  57 (** {2 Grammar extension} *)
  58
  59 let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
  60 let gram_ident s = Gramext.Stoken ("IDENT", s)
  61 let gram_number s = Gramext.Stoken ("NUMBER", s)
  62 let gram_keyword s = Gramext.Stoken ("", s)
  63 let gram_term = Gramext.Sself
  64
  65 let gram_of_literal =
  66   function
  67   | `Symbol s -> gram_symbol s
  68   | `Keyword s -> gram_keyword s
  69   | `Number s -> gram_number s
  70
  71 type binding =
  72   | NoBinding
  73   | Binding of string * value_type
  74   | Env of (string * value_type) list
  75
  76 let make_action action bindings =
  77   let rec aux (vl : CicNotationEnv.t) =
  78     function
  79       [] -> Gramext.action (fun (loc: location) -> action vl loc)
  80     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
  81     (* LUCA: DEFCON 5 BEGIN *)
  82     | Binding (name, TermType) :: tl ->
  83         Gramext.action
  84           (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl)
  85     | Binding (name, StringType) :: tl ->
  86         Gramext.action
  87           (fun (v:string) ->
  88             aux ((name, (StringType, StringValue v)) :: vl) tl)
  89     | Binding (name, NumType) :: tl ->
  90         Gramext.action
  91           (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
  92     | Binding (name, OptType t) :: tl ->
  93         Gramext.action
  94           (fun (v:'a option) ->
  95             aux ((name, (OptType t, OptValue v)) :: vl) tl)
  96     | Binding (name, ListType t) :: tl ->
  97         Gramext.action
  98           (fun (v:'a list) ->
  99             aux ((name, (ListType t, ListValue v)) :: vl) tl)
 100     | Env _ :: tl ->
 101         Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
 102     (* LUCA: DEFCON 5 END *)
 103   in
 104     aux [] (List.rev bindings)
 105
 106 let flatten_opt =
 107   let rec aux acc =
 108     function
 109       [] -> List.rev acc
 110     | NoBinding :: tl -> aux acc tl
 111     | Env names :: tl -> aux (List.rev names @ acc) tl
 112     | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
 113   in
 114   aux []
 115
 116   (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
 117 let extract_term_production pattern =
 118   let rec aux = function
 119     | AttributedTerm (_, t) -> aux t
 120     | Literal l -> aux_literal l
 121     | Layout l -> aux_layout l
 122     | Magic m -> aux_magic m
 123     | Variable v -> aux_variable v
 124     | t ->
 125         prerr_endline (CicNotationPp.pp_term t);
 126         assert false
 127   and aux_literal =
 128     function
 129     | `Symbol s -> [NoBinding, gram_symbol s]
 130     | `Keyword s ->
 131         (* assumption: s will be registered as a keyword with the lexer *)
 132         [NoBinding, gram_keyword s]
 133     | `Number s -> [NoBinding, gram_number s]
 134   and aux_layout = function
 135     | Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
 136     | Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
 137     | Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
 138     | Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
 139     | Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
 140     | Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
 141     | Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
 142     | Root (p1, p2) ->
 143         [NoBinding, gram_symbol "\\root"] @ aux p2
 144         @ [NoBinding, gram_symbol "\\of"] @ aux p1
 145     | Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
 146     | Break -> []
 147     | Box (_, pl) -> List.flatten (List.map aux pl)
 148     | Group pl -> List.flatten (List.map aux pl)
 149   and aux_magic magic =
 150     match magic with
 151     | Opt p ->
 152         let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
 153         let action (env_opt : CicNotationEnv.t option) (loc : location) =
 154           match env_opt with
 155           | Some env -> List.map opt_binding_some env
 156           | None -> List.map opt_binding_of_name p_names
 157         in
 158         [ Env (List.map opt_declaration p_names),
 159           Gramext.srules
 160             [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ],
 161               Gramext.action action ] ]
 162     | List0 (p, _)
 163     | List1 (p, _) ->
 164         let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
 165 (*         let env0 = List.map list_binding_of_name p_names in
 166         let grow_env_entry env n v =
 167           List.map
 168             (function
 169               | (n', (ty, ListValue vl)) as entry ->
 170                   if n' = n then n', (ty, ListValue (v :: vl)) else entry
 171               | _ -> assert false)
 172             env
 173         in
 174         let grow_env env_i env =
 175           List.fold_left
 176             (fun env (n, (_, v)) -> grow_env_entry env n v)
 177             env env_i
 178         in *)
 179         let action (env_list : CicNotationEnv.t list) (loc : location) =
 180           CicNotationEnv.coalesce_env p_names env_list
 181         in
 182         let gram_of_list s =
 183           match magic with
 184           | List0 (_, None) -> Gramext.Slist0 s
 185           | List1 (_, None) -> Gramext.Slist1 s
 186           | List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
 187           | List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
 188           | _ -> assert false
 189         in
 190         [ Env (List.map list_declaration p_names),
 191           Gramext.srules
 192             [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ],
 193               Gramext.action action ] ]
 194     | _ -> assert false
 195   and aux_variable =
 196     function
 197     | NumVar s -> [Binding (s, NumType), gram_number ""]
 198     | TermVar s -> [Binding (s, TermType), gram_term]
 199     | IdentVar s -> [Binding (s, StringType), gram_ident ""]
 200     | Ascription (p, s) -> assert false (* TODO *)
 201     | FreshVar _ -> assert false
 202   and inner_pattern p =
 203     let p_bindings, p_atoms = List.split (aux p) in
 204     let p_names = flatten_opt p_bindings in
 205     let action =
 206       make_action (fun (env : CicNotationEnv.t) (loc : location) -> env)
 207         p_bindings
 208     in
 209     p_bindings, p_atoms, p_names, action
 210   in
 211   aux pattern
 212
 213 let level_of precedence associativity =
 214   if precedence < min_precedence || precedence > max_precedence then
 215     raise (Level_not_found precedence);
 216   let assoc_string =
 217     match associativity with
 218     | Gramext.NonA -> "N"
 219     | Gramext.LeftA -> "L"
 220     | Gramext.RightA -> "R"
 221   in
 222   string_of_int precedence ^ assoc_string
 223
 224 type rule_id = Token.t Gramext.g_symbol list
 225
 226   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 227 let owned_keywords = Hashtbl.create 23
 228
 229 let extend level1_pattern ~precedence ~associativity action =
 230   let p_bindings, p_atoms =
 231     List.split (extract_term_production level1_pattern)
 232   in
 233   let level = level_of precedence associativity in
 234   let p_names = flatten_opt p_bindings in
 235   let _ =
 236     Grammar.extend
 237       [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
 238         Some (Gramext.Level level),
 239         [ None,
 240           Some associativity,
 241           [ p_atoms,
 242             (make_action
 243               (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
 244               p_bindings) ]]]
 245   in
 246   let keywords = CicNotationUtil.keywords_of_term level1_pattern in
 247   let rule_id = p_atoms in
 248   List.iter CicNotationLexer.add_level2_ast_keyword keywords;
 249   Hashtbl.add owned_keywords rule_id keywords;  (* keywords may be [] *)
 250   rule_id
 251
 252 let delete rule_id =
 253   let atoms = rule_id in
 254   (try
 255     let keywords = Hashtbl.find owned_keywords rule_id in
 256     List.iter CicNotationLexer.remove_level2_ast_keyword keywords
 257   with Not_found -> assert false);
 258   Grammar.delete_rule term atoms
 259
 260 (** {2 Grammar} *)
 261
 262 let parse_level1_pattern_ref = ref (fun _ -> assert false)
 263 let parse_level2_ast_ref = ref (fun _ -> assert false)
 264 let parse_level2_meta_ref = ref (fun _ -> assert false)
 265
 266 let fold_cluster binder terms ty body =
 267   List.fold_right
 268     (fun term body -> Binder (binder, (term, ty), body))
 269     terms body  (* terms are names: either Ident or FreshVar *)
 270
 271 let fold_binder binder pt_names body =
 272   List.fold_right
 273     (fun (names, ty) body -> fold_cluster binder names ty body)
 274     pt_names body
 275
 276 let return_term loc term = AttributedTerm (`Loc loc, term)
 277
 278 let _ = (* create empty precedence level for "term" *)
 279   let mk_level_list first last =
 280     let rec aux acc = function
 281       | i when i < first -> acc
 282       | i ->
 283           aux
 284             ((Some (string_of_int i ^ "N"), Some Gramext.NonA, [])
 285              :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, [])
 286              :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, [])
 287              :: acc)
 288             (i - 1)
 289     in
 290     aux [] last
 291   in
 292   Grammar.extend
 293     [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
 294       None,
 295       mk_level_list min_precedence max_precedence ]
 296
 297 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
 298 EXTEND
 299   GLOBAL: level1_pattern;
 300
 301   level1_pattern: [ [ p = l1_pattern; EOI -> CicNotationUtil.boxify p ] ];
 302   l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ];
 303   literal: [
 304     [ s = SYMBOL -> `Symbol s
 305     | k = QKEYWORD -> `Keyword k
 306     | n = NUMBER -> `Number n
 307     ]
 308   ];
 309   sep:       [ [ "sep";      sep = literal -> sep ] ];
 310 (*   row_sep:   [ [ "rowsep";   sep = literal -> sep ] ];
 311   field_sep: [ [ "fieldsep"; sep = literal -> sep ] ]; *)
 312   l1_magic_pattern: [
 313     [ "list0"; p = l1_simple_pattern; sep = OPT sep -> List0 (p, sep)
 314     | "list1"; p = l1_simple_pattern; sep = OPT sep -> List1 (p, sep)
 315     | "opt";   p = l1_simple_pattern -> Opt p
 316     ]
 317   ];
 318   l1_pattern_variable: [
 319     [ "term"; id = IDENT -> TermVar id
 320     | "number"; id = IDENT -> NumVar id
 321     | "ident"; id = IDENT -> IdentVar id
 322     ]
 323   ];
 324   l1_simple_pattern:
 325     [ "layout" LEFTA
 326       [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
 327           return_term loc (Layout (Sub (p1, p2)))
 328       | p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
 329           return_term loc (Layout (Sup (p1, p2)))
 330       | p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
 331           return_term loc (Layout (Below (p1, p2)))
 332       | p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
 333           return_term loc (Layout (Above (p1, p2)))
 334       | p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
 335           return_term loc (Layout (Over (p1, p2)))
 336       | p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
 337           return_term loc (Layout (Atop (p1, p2)))
 338 (*       | "array"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
 339           return_term loc (Array (p, csep, rsep)) *)
 340       | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
 341           return_term loc (Layout (Frac (p1, p2)))
 342       | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Layout (Sqrt p))
 343       | SYMBOL "\\root"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
 344           return_term loc (Layout (Root (arg, index)))
 345       | "hbox"; LPAREN; p = l1_pattern; RPAREN ->
 346           return_term loc (Layout (Box ((H, false, false), p)))
 347       | "vbox"; LPAREN; p = l1_pattern; RPAREN ->
 348           return_term loc (Layout (Box ((V, false, false), p)))
 349       | "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
 350           return_term loc (Layout (Box ((HV, false, false), p)))
 351       | "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
 352           return_term loc (Layout (Box ((HOV, false, false), p)))
 353       | "break" -> return_term loc (Layout Break)
 354 (*       | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
 355       | LPAREN; p = l1_pattern; RPAREN ->
 356           return_term loc (CicNotationUtil.group p)
 357       ]
 358     | "simple" NONA
 359       [ i = IDENT -> return_term loc (Variable (TermVar i))
 360       | m = l1_magic_pattern -> return_term loc (Magic m)
 361       | v = l1_pattern_variable -> return_term loc (Variable v)
 362       | l = literal -> return_term loc (Literal l)
 363       ]
 364     ];
 365   END
 366 (* }}} *)
 367
 368 (* {{{ Grammar for ast magics, notation level 2 *)
 369 EXTEND
 370   GLOBAL: level2_meta;
 371   l2_variable: [
 372     [ "term"; id = IDENT -> TermVar id
 373     | "number"; id = IDENT -> NumVar id
 374     | "ident"; id = IDENT -> IdentVar id
 375     | "fresh"; id = IDENT -> FreshVar id
 376     | "anonymous" -> TermVar "_"
 377     | id = IDENT -> TermVar id
 378     ]
 379   ];
 380   l2_magic: [
 381     [ "fold"; kind = [ "left" -> `Left | "right" -> `Right ];
 382       base = level2_meta; "rec"; id = IDENT; recursive = level2_meta ->
 383         Fold (kind, base, [id], recursive)
 384     | "default"; some = level2_meta; none = level2_meta -> Default (some, none)
 385     | "if"; p_test = level2_meta;
 386       "then"; p_true = level2_meta;
 387       "else"; p_false = level2_meta ->
 388         If (p_test, p_true, p_false)
 389     | "fail" -> Fail
 390     ]
 391   ];
 392   level2_meta: [
 393     [ magic = l2_magic -> Magic magic
 394     | var = l2_variable -> Variable var
 395     | blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob)
 396     ]
 397   ];
 398 END
 399 (* }}} *)
 400
 401 (* {{{ Grammar for ast patterns, notation level 2 *)
 402 EXTEND
 403   GLOBAL: level2_ast term let_defs;
 404   level2_ast: [ [ p = term -> p ] ];
 405   sort: [
 406     [ "Prop" -> `Prop
 407     | "Set" -> `Set
 408     | "Type" -> `Type
 409     | "CProp" -> `CProp
 410     ]
 411   ];
 412   explicit_subst: [
 413     [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
 414       SYMBOL "[";
 415       substs = LIST1 [
 416         i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
 417       ] SEP SYMBOL ";";
 418       SYMBOL "]" ->
 419         substs
 420     ]
 421   ];
 422   meta_subst: [
 423     [ s = SYMBOL "_" -> None
 424     | p = term -> Some p ]
 425   ];
 426   meta_substs: [
 427     [ SYMBOL "["; substs = LIST0 meta_subst; SYMBOL "]" -> substs ]
 428   ];
 429   possibly_typed_name: [
 430     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
 431         id, Some typ
 432     | arg = single_arg -> arg, None
 433     ]
 434   ];
 435   match_pattern: [
 436     [ id = IDENT -> id, []
 437     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
 438         id, vars
 439     ]
 440   ];
 441   binder: [
 442     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
 443     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
 444     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
 445     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
 446     ]
 447   ];
 448   arg: [
 449     [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
 450       SYMBOL ":"; ty = term; RPAREN ->
 451         List.map (fun n -> Ident (n, None)) names, Some ty
 452     | name = IDENT -> [Ident (name, None)], None
 453     | blob = UNPARSED_META ->
 454         let meta = !parse_level2_meta_ref (Stream.of_string blob) in
 455         match meta with
 456         | Variable (FreshVar _) -> [meta], None
 457         | Variable (TermVar "_") -> [Ident ("_", None)], None
 458         | _ -> failwith "Invalid bound name."
 459    ]
 460   ];
 461   single_arg: [
 462     [ name = IDENT -> Ident (name, None)
 463     | blob = UNPARSED_META ->
 464         let meta = !parse_level2_meta_ref (Stream.of_string blob) in
 465         match meta with
 466         | Variable (FreshVar _) -> meta
 467         | Variable (TermVar "_") -> Ident ("_", None)
 468         | _ -> failwith "Invalid index name."
 469     ]
 470   ];
 471   induction_kind: [
 472     [ "rec" -> `Inductive
 473     | "corec" -> `CoInductive
 474     ]
 475   ];
 476   let_defs: [
 477     [ defs = LIST1 [
 478         name = single_arg;
 479         args = LIST1 arg;
 480         index_name = OPT [ "on"; id = single_arg -> id ];
 481         ty = OPT [ SYMBOL ":" ; p = term -> p ];
 482         SYMBOL <:unicode<def>> (* ≝ *); body = term ->
 483           let body = fold_binder `Lambda args body in
 484           let ty =
 485             match ty with
 486             | None -> None
 487             | Some ty -> Some (fold_binder `Pi args ty)
 488           in
 489           let rec position_of name p = function
 490             | [] -> None, p
 491             | n :: _ when n = name -> Some p, p
 492             | _ :: tl -> position_of name (p + 1) tl
 493           in
 494           let rec find_arg name n = function
 495             | [] ->
 496                 fail loc (sprintf "Argument %s not found"
 497                   (CicNotationPp.pp_term name))
 498             | (l,_) :: tl ->
 499                 (match position_of name 0 l with
 500                 | None, len -> find_arg name (n + len) tl
 501                 | Some where, len -> n + where)
 502           in
 503           let index =
 504             match index_name with
 505             | None -> 0
 506             | Some index_name -> find_arg index_name 0 args
 507           in
 508           (name, ty), body, index
 509       ] SEP "and" ->
 510         defs
 511     ]
 512   ];
 513   binder_vars: [
 514     [ vars = [
 515           l = LIST1 single_arg SEP SYMBOL "," -> l
 516         | SYMBOL "_" -> [Ident ("_", None)] ];
 517       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
 518     | LPAREN;
 519         vars = [
 520             l =  LIST1 single_arg SEP SYMBOL "," -> l
 521           | SYMBOL "_" -> [Ident ("_", None)] ];
 522       typ = OPT [ SYMBOL ":"; t = term -> t ];
 523       RPAREN -> (vars, typ)
 524     ]
 525   ];
 526   term: LEVEL "10N" [ (* let in *)
 527     [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
 528       p1 = term; "in"; p2 = term ->
 529         return_term loc (LetIn (var, p1, p2))
 530     | "let"; k = induction_kind; defs = let_defs; "in";
 531       body = term ->
 532         return_term loc (LetRec (k, defs, body))
 533     ]
 534   ];
 535   term: LEVEL "20R"  (* binder *)
 536     [
 537       [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
 538           return_term loc (fold_cluster b vars typ body)
 539       ]
 540     ];
 541   term: LEVEL "70L"  (* apply *)
 542     [
 543       [ p1 = term; p2 = term ->
 544           let rec aux = function
 545             | Appl (hd :: tl)
 546             | AttributedTerm (_, Appl (hd :: tl)) ->
 547                 aux hd @ tl
 548             | term -> [term]
 549           in
 550           return_term loc (Appl (aux p1 @ [p2]))
 551       ]
 552     ];
 553   term: LEVEL "90N"  (* simple *)
 554     [
 555       [ id = IDENT -> return_term loc (Ident (id, None))
 556       | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
 557       | s = CSYMBOL -> return_term loc (Symbol (s, 0))
 558       | u = URI -> return_term loc (Uri (u, None))
 559       | n = NUMBER -> return_term loc (Num (n, 0))
 560       | IMPLICIT -> return_term loc (Implicit)
 561       | PLACEHOLDER -> return_term loc UserInput
 562       | m = META -> return_term loc (Meta (int_of_string m, []))
 563       | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
 564       | s = sort -> return_term loc (Sort s)
 565       | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
 566         "match"; t = term;
 567         indty_ident = OPT [ "in"; id = IDENT -> id ];
 568         "with"; SYMBOL "[";
 569         patterns = LIST0 [
 570           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
 571           rhs = term ->
 572             lhs, rhs
 573         ] SEP SYMBOL "|";
 574         SYMBOL "]" ->
 575           return_term loc (Case (t, indty_ident, outtyp, patterns))
 576       | LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
 577           return_term loc (Cast (p1, p2))
 578       | LPAREN; p = term; RPAREN -> p
 579       | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
 580       ]
 581     ];
 582 END
 583 (* }}} *)
 584
 585 (** {2 API implementation} *)
 586
 587 let exc_located_wrapper f =
 588   try
 589     f ()
 590   with
 591   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 592       raise (Parse_error (floc, msg))
 593   | Stdpp.Exc_located (floc, exn) ->
 594       raise (Parse_error (floc, (Printexc.to_string exn)))
 595
 596 let parse_level1_pattern stream =
 597   exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
 598 let parse_level2_ast stream =
 599   exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast stream)
 600 let parse_level2_meta stream =
 601   exc_located_wrapper (fun () -> Grammar.Entry.parse level2_meta stream)
 602
 603 let _ =
 604   parse_level1_pattern_ref := parse_level1_pattern;
 605   parse_level2_ast_ref := parse_level2_ast;
 606   parse_level2_meta_ref := parse_level2_meta
 607
 608 (** {2 Debugging} *)
 609
 610 let print_l2_pattern () =
 611   Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term);
 612   Format.pp_print_flush Format.std_formatter ();
 613   flush stdout
 614
 615 (* vim:set encoding=utf8 foldmethod=marker: *)