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