helm/ocaml/cic_notation/cicNotationParser.expanded.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 oopen Printf
  27 mmodule Ast = CicNotationPtmmodule Env = CicNotationEnv
  28 eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
  29 llet level1_pattern_grammar =
  30   Grammar.gcreate CicNotationLexer.level1_pattern_lexerllet level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexerllet level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
  31 llet min_precedence = 0llet max_precedence = 100
  32 llet level1_pattern =
  33   Grammar.Entry.create level1_pattern_grammar "level1_pattern"llet level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"llet term = Grammar.Entry.create level2_ast_grammar "term"llet let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"llet level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
  34 llet return_term loc term = ()
  35 llet int_of_string s =
  36   try Pervasives.int_of_string s with
  37     Failure _ ->
  38       failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
  39 (** {2 Grammar extension} *)
  40
  41 llet gram_symbol s = Gramext.Stoken ("SYMBOL", s)llet gram_ident s = Gramext.Stoken ("IDENT", s)llet gram_number s = Gramext.Stoken ("NUMBER", s)llet gram_keyword s = Gramext.Stoken ("", s)llet gram_term = Gramext.Sself
  42 llet gram_of_literal =
  43   function
  44     `Symbol s -> gram_symbol s
  45   | `Keyword s -> gram_keyword s
  46   | `Number s -> gram_number s
  47 ttype binding =
  48     NoBinding
  49   | Binding of string * Env.value_type
  50   | Env of (string * Env.value_type) list
  51 llet make_action action bindings =
  52   let rec aux (vl : CicNotationEnv.t) =
  53     function
  54       [] -> Gramext.action (fun (loc : Ast.location) -> action vl loc)
  55     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
  56     | Binding (name, Env.TermType) :: tl ->
  57         Gramext.action
  58           (fun (v : Ast.term) ->
  59              aux ((name, (Env.TermType, Env.TermValue v)) :: vl) tl)
  60     | Binding (name, Env.StringType) :: tl ->
  61         Gramext.action
  62           (fun (v : string) ->
  63              aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
  64     | Binding (name, Env.NumType) :: tl ->
  65         Gramext.action
  66           (fun (v : string) ->
  67              aux ((name, (Env.NumType, Env.NumValue v)) :: vl) tl)
  68     | Binding (name, Env.OptType t) :: tl ->
  69         Gramext.action
  70           (fun (v : 'a option) ->
  71              aux ((name, (Env.OptType t, Env.OptValue v)) :: vl) tl)
  72     | Binding (name, Env.ListType t) :: tl ->
  73         Gramext.action
  74           (fun (v : 'a list) ->
  75              aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
  76     | Env _ :: tl ->
  77         Gramext.action (fun (v : CicNotationEnv.t) -> aux (v @ vl) tl)
  78   in
  79   aux [] (List.rev bindings)
  80 llet flatten_opt =
  81   let rec aux acc =
  82     function
  83       [] -> List.rev acc
  84     | NoBinding :: tl -> aux acc tl
  85     | Env names :: tl -> aux (List.rev names @ acc) tl
  86     | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
  87   in
  88   aux []
  89   (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
  90 llet extract_term_production pattern =
  91   let rec aux =
  92     function
  93       Ast.AttributedTerm (_, t) -> aux t
  94     | Ast.Literal l -> aux_literal l
  95     | Ast.Layout l -> aux_layout l
  96     | Ast.Magic m -> aux_magic m
  97     | Ast.Variable v -> aux_variable v
  98     | t -> prerr_endline (CicNotationPp.pp_term t); assert false
  99   and aux_literal =
 100     function
 101       `Symbol s -> [NoBinding, gram_symbol s]
 102     | `Keyword s -> [NoBinding, gram_keyword s]
 103     | `Number s -> [NoBinding, gram_number s]
 104   and aux_layout =
 105     function
 106       Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
 107     | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
 108     | Ast.Below (p1, p2) ->
 109         aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
 110     | Ast.Above (p1, p2) ->
 111         aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
 112     | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
 113     | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
 114     | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
 115     | Ast.Root (p1, p2) ->
 116         [NoBinding, gram_symbol "\\root"] @ aux p2 @
 117           [NoBinding, gram_symbol "\\of"] @ aux p1
 118     | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
 119     | Ast.Break -> []
 120     | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
 121     | Ast.Group pl -> List.flatten (List.map aux pl)
 122   and aux_magic magic =
 123     match magic with
 124       Ast.Opt p ->
 125         let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
 126         let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) =
 127           match env_opt with
 128             Some env -> List.map Env.opt_binding_some env
 129           | None -> List.map Env.opt_binding_of_name p_names
 130         in
 131         [Env (List.map Env.opt_declaration p_names),
 132          Gramext.srules
 133            [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])],
 134             Gramext.action action]]
 135     | Ast.List0 (p, _) | Ast.List1 (p, _) ->
 136         let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
 137         let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
 138           CicNotationEnv.coalesce_env p_names env_list
 139         in
 140         let gram_of_list s =
 141           match magic with
 142             Ast.List0 (_, None) -> Gramext.Slist0 s
 143           | Ast.List1 (_, None) -> Gramext.Slist1 s
 144           | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
 145           | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
 146           | _ -> assert false
 147         in
 148         [Env (List.map Env.list_declaration p_names),
 149          Gramext.srules
 150            [[gram_of_list (Gramext.srules [p_atoms, p_action])],
 151             Gramext.action action]]
 152     | _ -> assert false
 153   and aux_variable =
 154     function
 155       Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
 156     | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
 157     | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
 158     | Ast.Ascription (p, s) -> assert false
 159     | Ast.FreshVar _ -> assert false
 160   and inner_pattern p =
 161     let (p_bindings, p_atoms) = List.split (aux p) in
 162     let p_names = flatten_opt p_bindings in
 163     let action =
 164       make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env)
 165         p_bindings
 166     in
 167     p_bindings, p_atoms, p_names, action
 168   in
 169   aux pattern
 170
 171 let level_of precedence associativity =
 172   if precedence < min_precedence || precedence > max_precedence then
 173     raise (Level_not_found precedence);
 174   let assoc_string =
 175     match associativity with
 176       Gramext.NonA -> "N"
 177     | Gramext.LeftA -> "L"
 178     | Gramext.RightA -> "R"
 179   in
 180   string_of_int precedence ^ assoc_string
 181
 182 type rule_id = Token.t Gramext.g_symbol list
 183
 184   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 185 let owned_keywords = Hashtbl.create 23
 186
 187 let extend level1_pattern ~precedence ~associativity action =
 188   let (p_bindings, p_atoms) =
 189     List.split (extract_term_production level1_pattern)
 190   in
 191   let level = level_of precedence associativity in
 192   let p_names = flatten_opt p_bindings in
 193   let _ =
 194     Grammar.extend
 195       [Grammar.Entry.obj (term : 'a Grammar.Entry.e),
 196        Some (Gramext.Level level),
 197        [None, Some associativity,
 198         [p_atoms,
 199          make_action
 200            (fun (env : CicNotationEnv.t) (loc : Ast.location) ->
 201               action env loc)
 202            p_bindings]]]
 203   in
 204   let keywords = CicNotationUtil.keywords_of_term level1_pattern in
 205   let rule_id = p_atoms in
 206   List.iter CicNotationLexer.add_level2_ast_keyword keywords;
 207   Hashtbl.add owned_keywords rule_id keywords;
 208   rule_id
 209
 210 let delete rule_id =
 211   let atoms = rule_id in
 212   begin try
 213     let keywords = Hashtbl.find owned_keywords rule_id in
 214     List.iter CicNotationLexer.remove_level2_ast_keyword keywords
 215   with
 216     Not_found -> assert false
 217   end;
 218   Grammar.delete_rule term atoms
 219
 220 (** {2 Grammar} *)
 221
 222 let parse_level1_pattern_ref = ref (fun _ -> assert false)
 223 let parse_level2_ast_ref = ref (fun _ -> assert false)
 224 let parse_level2_meta_ref = ref (fun _ -> assert false)
 225
 226 let fold_cluster binder terms ty body =
 227   List.fold_right (fun term body -> Ast.Binder (binder, (term, ty), body))
 228     terms body  (* terms are names: either Ident or FreshVar *)
 229
 230 let fold_exists terms ty body =
 231   List.fold_right
 232     (fun term body ->
 233        let lambda = Ast.Binder (`Lambda, (term, ty), body) in
 234        Ast.Appl [Ast.Symbol ("exists", 0); lambda])
 235     terms body
 236
 237 let fold_binder binder pt_names body =
 238   List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
 239     pt_names body
 240
 241 let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
 242
 243   (* create empty precedence level for "term" *)
 244 let _ =
 245   let dummy_action =
 246     Gramext.action
 247       (fun _ -> failwith "internal error, lexer generated a dummy token")
 248   in
 249   let dummy_prod = [[Gramext.Stoken ("DUMMY", "")], dummy_action] in
 250   let mk_level_list first last =
 251     let rec aux acc =
 252       function
 253         i when i < first -> acc
 254       | i ->
 255           aux
 256             ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod) ::
 257                (Some (string_of_int i ^ "L"), Some Gramext.LeftA,
 258                 dummy_prod) ::
 259                (Some (string_of_int i ^ "R"), Some Gramext.RightA,
 260                 dummy_prod) ::
 261                acc)
 262             (i - 1)
 263     in
 264     aux [] last
 265   in
 266   Grammar.extend
 267     [Grammar.Entry.obj (term : 'a Grammar.Entry.e), None,
 268      mk_level_list min_precedence max_precedence]
 269
 270 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
 271 let _ =
 272   Grammar.extend
 273     (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e) in
 274      let grammar_entry_create s =
 275        Grammar.Entry.create (Grammar.of_entry level1_pattern) s
 276      in
 277      let l1_pattern : 'l1_pattern Grammar.Entry.e =
 278        grammar_entry_create "l1_pattern"
 279      and literal : 'literal Grammar.Entry.e = grammar_entry_create "literal"
 280      and sep : 'sep Grammar.Entry.e = grammar_entry_create "sep"
 281      and l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e =
 282        grammar_entry_create "l1_magic_pattern"
 283      and l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e =
 284        grammar_entry_create "l1_pattern_variable"
 285      and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e =
 286        grammar_entry_create "l1_simple_pattern"
 287      in
 288      [Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e),
 289       None,
 290       [None, None,
 291        [[Gramext.Snterm
 292            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 293          Gramext.Stoken ("EOI", "")],
 294         Gramext.action
 295           (fun _ (p : 'l1_pattern)
 296              (loc : Lexing.position * Lexing.position) ->
 297              (CicNotationUtil.boxify p : 'level1_pattern))]];
 298       Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
 299       [None, None,
 300        [[Gramext.Slist1
 301            (Gramext.Snterm
 302               (Grammar.Entry.obj
 303                  (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
 304         Gramext.action
 305           (fun (p : 'l1_simple_pattern list)
 306              (loc : Lexing.position * Lexing.position) ->
 307              (p : 'l1_pattern))]];
 308       Grammar.Entry.obj (literal : 'literal Grammar.Entry.e), None,
 309       [None, None,
 310        [[Gramext.Stoken ("NUMBER", "")],
 311         Gramext.action
 312           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
 313              (`Number n : 'literal));
 314         [Gramext.Stoken ("QKEYWORD", "")],
 315         Gramext.action
 316           (fun (k : string) (loc : Lexing.position * Lexing.position) ->
 317              (`Keyword k : 'literal));
 318         [Gramext.Stoken ("SYMBOL", "")],
 319         Gramext.action
 320           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
 321              (`Symbol s : 'literal))]];
 322       Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None,
 323       [None, None,
 324        [[Gramext.Stoken ("", "sep");
 325          Gramext.Snterm
 326            (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
 327         Gramext.action
 328           (fun (sep : 'literal) _ (loc : Lexing.position * Lexing.position) ->
 329              (sep : 'sep))]];
 330       Grammar.Entry.obj
 331         (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e),
 332       None,
 333       [None, None,
 334        [[Gramext.Stoken ("", "opt");
 335          Gramext.Snterm
 336            (Grammar.Entry.obj
 337               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
 338         Gramext.action
 339           (fun (p : 'l1_simple_pattern) _
 340              (loc : Lexing.position * Lexing.position) ->
 341              (Ast.Opt p : 'l1_magic_pattern));
 342         [Gramext.Stoken ("", "list1");
 343          Gramext.Snterm
 344            (Grammar.Entry.obj
 345               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
 346          Gramext.Sopt
 347            (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
 348         Gramext.action
 349           (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
 350              (loc : Lexing.position * Lexing.position) ->
 351              (Ast.List1 (p, sep) : 'l1_magic_pattern));
 352         [Gramext.Stoken ("", "list0");
 353          Gramext.Snterm
 354            (Grammar.Entry.obj
 355               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
 356          Gramext.Sopt
 357            (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
 358         Gramext.action
 359           (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
 360              (loc : Lexing.position * Lexing.position) ->
 361              (Ast.List0 (p, sep) : 'l1_magic_pattern))]];
 362       Grammar.Entry.obj
 363         (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e),
 364       None,
 365       [None, None,
 366        [[Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
 367         Gramext.action
 368           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 369              (Ast.IdentVar id : 'l1_pattern_variable));
 370         [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
 371         Gramext.action
 372           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 373              (Ast.NumVar id : 'l1_pattern_variable));
 374         [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
 375         Gramext.action
 376           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 377              (Ast.TermVar id : 'l1_pattern_variable))]];
 378       Grammar.Entry.obj
 379         (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
 380       None,
 381       [Some "layout", Some Gramext.LeftA,
 382        [[Gramext.Stoken ("LPAREN", "");
 383          Gramext.Snterm
 384            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 385          Gramext.Stoken ("RPAREN", "")],
 386         Gramext.action
 387           (fun _ (p : 'l1_pattern) _
 388              (loc : Lexing.position * Lexing.position) ->
 389              (return_term loc (CicNotationUtil.group p) :
 390               'l1_simple_pattern));
 391         [Gramext.Stoken ("", "break")],
 392         Gramext.action
 393           (fun _ (loc : Lexing.position * Lexing.position) ->
 394              (return_term loc (Ast.Layout Ast.Break) : 'l1_simple_pattern));
 395         [Gramext.Stoken ("", "hovbox"); Gramext.Stoken ("LPAREN", "");
 396          Gramext.Snterm
 397            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 398          Gramext.Stoken ("RPAREN", "")],
 399         Gramext.action
 400           (fun _ (p : 'l1_pattern) _ _
 401              (loc : Lexing.position * Lexing.position) ->
 402              (return_term loc
 403                 (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p))) :
 404               'l1_simple_pattern));
 405         [Gramext.Stoken ("", "hvbox"); Gramext.Stoken ("LPAREN", "");
 406          Gramext.Snterm
 407            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 408          Gramext.Stoken ("RPAREN", "")],
 409         Gramext.action
 410           (fun _ (p : 'l1_pattern) _ _
 411              (loc : Lexing.position * Lexing.position) ->
 412              (return_term loc
 413                 (Ast.Layout (Ast.Box ((Ast.HV, false, false), p))) :
 414               'l1_simple_pattern));
 415         [Gramext.Stoken ("", "vbox"); Gramext.Stoken ("LPAREN", "");
 416          Gramext.Snterm
 417            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 418          Gramext.Stoken ("RPAREN", "")],
 419         Gramext.action
 420           (fun _ (p : 'l1_pattern) _ _
 421              (loc : Lexing.position * Lexing.position) ->
 422              (return_term loc
 423                 (Ast.Layout (Ast.Box ((Ast.V, false, false), p))) :
 424               'l1_simple_pattern));
 425         [Gramext.Stoken ("", "hbox"); Gramext.Stoken ("LPAREN", "");
 426          Gramext.Snterm
 427            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 428          Gramext.Stoken ("RPAREN", "")],
 429         Gramext.action
 430           (fun _ (p : 'l1_pattern) _ _
 431              (loc : Lexing.position * Lexing.position) ->
 432              (return_term loc
 433                 (Ast.Layout (Ast.Box ((Ast.H, false, false), p))) :
 434               'l1_simple_pattern));
 435         [Gramext.Stoken ("SYMBOL", "\\root"); Gramext.Sself;
 436          Gramext.Stoken ("SYMBOL", "\\of"); Gramext.Sself],
 437         Gramext.action
 438           (fun (arg : 'l1_simple_pattern) _ (index : 'l1_simple_pattern) _
 439              (loc : Lexing.position * Lexing.position) ->
 440              (return_term loc (Ast.Layout (Ast.Root (arg, index))) :
 441               'l1_simple_pattern));
 442         [Gramext.Stoken ("SYMBOL", "\\sqrt"); Gramext.Sself],
 443         Gramext.action
 444           (fun (p : 'l1_simple_pattern) _
 445              (loc : Lexing.position * Lexing.position) ->
 446              (return_term loc (Ast.Layout (Ast.Sqrt p)) :
 447               'l1_simple_pattern));
 448         [Gramext.Stoken ("SYMBOL", "\\frac"); Gramext.Sself; Gramext.Sself],
 449         Gramext.action
 450           (fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _
 451              (loc : Lexing.position * Lexing.position) ->
 452              (return_term loc (Ast.Layout (Ast.Frac (p1, p2))) :
 453               'l1_simple_pattern));
 454         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\atop"); Gramext.Sself],
 455         Gramext.action
 456           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 457              (loc : Lexing.position * Lexing.position) ->
 458              (return_term loc (Ast.Layout (Ast.Atop (p1, p2))) :
 459               'l1_simple_pattern));
 460         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\over"); Gramext.Sself],
 461         Gramext.action
 462           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 463              (loc : Lexing.position * Lexing.position) ->
 464              (return_term loc (Ast.Layout (Ast.Over (p1, p2))) :
 465               'l1_simple_pattern));
 466         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\above"); Gramext.Sself],
 467         Gramext.action
 468           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 469              (loc : Lexing.position * Lexing.position) ->
 470              (return_term loc (Ast.Layout (Ast.Above (p1, p2))) :
 471               'l1_simple_pattern));
 472         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\below"); Gramext.Sself],
 473         Gramext.action
 474           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 475              (loc : Lexing.position * Lexing.position) ->
 476              (return_term loc (Ast.Layout (Ast.Below (p1, p2))) :
 477               'l1_simple_pattern));
 478         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\sup"); Gramext.Sself],
 479         Gramext.action
 480           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 481              (loc : Lexing.position * Lexing.position) ->
 482              (return_term loc (Ast.Layout (Ast.Sup (p1, p2))) :
 483               'l1_simple_pattern));
 484         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\sub"); Gramext.Sself],
 485         Gramext.action
 486           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 487              (loc : Lexing.position * Lexing.position) ->
 488              (return_term loc (Ast.Layout (Ast.Sub (p1, p2))) :
 489               'l1_simple_pattern))];
 490        Some "simple", Some Gramext.NonA,
 491        [[Gramext.Snterm
 492            (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
 493         Gramext.action
 494           (fun (l : 'literal) (loc : Lexing.position * Lexing.position) ->
 495              (return_term loc (Ast.Literal l) : 'l1_simple_pattern));
 496         [Gramext.Snterm
 497            (Grammar.Entry.obj
 498               (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e))],
 499         Gramext.action
 500           (fun (v : 'l1_pattern_variable)
 501              (loc : Lexing.position * Lexing.position) ->
 502              (return_term loc (Ast.Variable v) : 'l1_simple_pattern));
 503         [Gramext.Snterm
 504            (Grammar.Entry.obj
 505               (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e))],
 506         Gramext.action
 507           (fun (m : 'l1_magic_pattern)
 508              (loc : Lexing.position * Lexing.position) ->
 509              (return_term loc (Ast.Magic m) : 'l1_simple_pattern));
 510         [Gramext.Stoken ("IDENT", "")],
 511         Gramext.action
 512           (fun (i : string) (loc : Lexing.position * Lexing.position) ->
 513              (return_term loc (Ast.Variable (Ast.TermVar i)) :
 514               'l1_simple_pattern))]]])
 515 (* }}} *)
 516
 517 (* {{{ Grammar for ast magics, notation level 2 *)
 518 let _ =
 519   Grammar.extend
 520     (let _ = (level2_meta : 'level2_meta Grammar.Entry.e) in
 521      let grammar_entry_create s =
 522        Grammar.Entry.create (Grammar.of_entry level2_meta) s
 523      in
 524      let l2_variable : 'l2_variable Grammar.Entry.e =
 525        grammar_entry_create "l2_variable"
 526      and l2_magic : 'l2_magic Grammar.Entry.e =
 527        grammar_entry_create "l2_magic"
 528      in
 529      [Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e), None,
 530       [None, None,
 531        [[Gramext.Stoken ("IDENT", "")],
 532         Gramext.action
 533           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
 534              (Ast.TermVar id : 'l2_variable));
 535         [Gramext.Stoken ("", "anonymous")],
 536         Gramext.action
 537           (fun _ (loc : Lexing.position * Lexing.position) ->
 538              (Ast.TermVar "_" : 'l2_variable));
 539         [Gramext.Stoken ("", "fresh"); Gramext.Stoken ("IDENT", "")],
 540         Gramext.action
 541           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 542              (Ast.FreshVar id : 'l2_variable));
 543         [Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
 544         Gramext.action
 545           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 546              (Ast.IdentVar id : 'l2_variable));
 547         [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
 548         Gramext.action
 549           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 550              (Ast.NumVar id : 'l2_variable));
 551         [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
 552         Gramext.action
 553           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 554              (Ast.TermVar id : 'l2_variable))]];
 555       Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e), None,
 556       [None, None,
 557        [[Gramext.Stoken ("", "fail")],
 558         Gramext.action
 559           (fun _ (loc : Lexing.position * Lexing.position) ->
 560              (Ast.Fail : 'l2_magic));
 561         [Gramext.Stoken ("", "if");
 562          Gramext.Snterm
 563            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
 564          Gramext.Stoken ("", "then");
 565          Gramext.Snterm
 566            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
 567          Gramext.Stoken ("", "else");
 568          Gramext.Snterm
 569            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
 570         Gramext.action
 571           (fun (p_false : 'level2_meta) _ (p_true : 'level2_meta) _
 572              (p_test : 'level2_meta) _
 573              (loc : Lexing.position * Lexing.position) ->
 574              (Ast.If (p_test, p_true, p_false) : 'l2_magic));
 575         [Gramext.Stoken ("", "default");
 576          Gramext.Snterm
 577            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
 578          Gramext.Snterm
 579            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
 580         Gramext.action
 581           (fun (none : 'level2_meta) (some : 'level2_meta) _
 582              (loc : Lexing.position * Lexing.position) ->
 583              (Ast.Default (some, none) : 'l2_magic));
 584         [Gramext.Stoken ("", "fold");
 585          Gramext.srules
 586            [[Gramext.Stoken ("", "right")],
 587             Gramext.action
 588               (fun _ (loc : Lexing.position * Lexing.position) ->
 589                  (`Right : 'e__1));
 590             [Gramext.Stoken ("", "left")],
 591             Gramext.action
 592               (fun _ (loc : Lexing.position * Lexing.position) ->
 593                  (`Left : 'e__1))];
 594          Gramext.Snterm
 595            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
 596          Gramext.Stoken ("", "rec"); Gramext.Stoken ("IDENT", "");
 597          Gramext.Snterm
 598            (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
 599         Gramext.action
 600           (fun (recursive : 'level2_meta) (id : string) _
 601              (base : 'level2_meta) (kind : 'e__1) _
 602              (loc : Lexing.position * Lexing.position) ->
 603              (Ast.Fold (kind, base, [id], recursive) : 'l2_magic))]];
 604       Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e), None,
 605       [None, None,
 606        [[Gramext.Stoken ("UNPARSED_AST", "")],
 607         Gramext.action
 608           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
 609              (!parse_level2_ast_ref (Ulexing.from_utf8_string blob) :
 610               'level2_meta));
 611         [Gramext.Snterm
 612            (Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e))],
 613         Gramext.action
 614           (fun (var : 'l2_variable)
 615              (loc : Lexing.position * Lexing.position) ->
 616              (Ast.Variable var : 'level2_meta));
 617         [Gramext.Snterm
 618            (Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e))],
 619         Gramext.action
 620           (fun (magic : 'l2_magic)
 621              (loc : Lexing.position * Lexing.position) ->
 622              (Ast.Magic magic : 'level2_meta))]]])
 623 (* }}} *)
 624
 625 (* {{{ Grammar for ast patterns, notation level 2 *)
 626 let _ =
 627   Grammar.extend
 628     (let _ = (level2_ast : 'level2_ast Grammar.Entry.e)
 629      and _ = (term : 'term Grammar.Entry.e)
 630      and _ = (let_defs : 'let_defs Grammar.Entry.e) in
 631      let grammar_entry_create s =
 632        Grammar.Entry.create (Grammar.of_entry level2_ast) s
 633      in
 634      let sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
 635      and explicit_subst : 'explicit_subst Grammar.Entry.e =
 636        grammar_entry_create "explicit_subst"
 637      and meta_subst : 'meta_subst Grammar.Entry.e =
 638        grammar_entry_create "meta_subst"
 639      and meta_substs : 'meta_substs Grammar.Entry.e =
 640        grammar_entry_create "meta_substs"
 641      and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
 642        grammar_entry_create "possibly_typed_name"
 643      and match_pattern : 'match_pattern Grammar.Entry.e =
 644        grammar_entry_create "match_pattern"
 645      and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
 646      and arg : 'arg Grammar.Entry.e = grammar_entry_create "arg"
 647      and single_arg : 'single_arg Grammar.Entry.e =
 648        grammar_entry_create "single_arg"
 649      and induction_kind : 'induction_kind Grammar.Entry.e =
 650        grammar_entry_create "induction_kind"
 651      and binder_vars : 'binder_vars Grammar.Entry.e =
 652        grammar_entry_create "binder_vars"
 653      in
 654      [Grammar.Entry.obj (level2_ast : 'level2_ast Grammar.Entry.e), None,
 655       [None, None,
 656        [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
 657         Gramext.action
 658           (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
 659              (p : 'level2_ast))]];
 660       Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
 661       [None, None,
 662        [[Gramext.Stoken ("", "CProp")],
 663         Gramext.action
 664           (fun _ (loc : Lexing.position * Lexing.position) ->
 665              (`CProp : 'sort));
 666         [Gramext.Stoken ("", "Type")],
 667         Gramext.action
 668           (fun _ (loc : Lexing.position * Lexing.position) ->
 669              (`Type : 'sort));
 670         [Gramext.Stoken ("", "Set")],
 671         Gramext.action
 672           (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
 673         [Gramext.Stoken ("", "Prop")],
 674         Gramext.action
 675           (fun _ (loc : Lexing.position * Lexing.position) ->
 676              (`Prop : 'sort))]];
 677       Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
 678       None,
 679       [None, None,
 680        [[Gramext.Stoken ("SYMBOL", "\\subst"); Gramext.Stoken ("SYMBOL", "[");
 681          Gramext.Slist1sep
 682            (Gramext.srules
 683               [[Gramext.Stoken ("IDENT", "");
 684                 Gramext.Stoken ("SYMBOL", "≔");
 685                 Gramext.Snterm
 686                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
 687                Gramext.action
 688                  (fun (t : 'term) _ (i : string)
 689                     (loc : Lexing.position * Lexing.position) ->
 690                     (i, t : 'e__2))],
 691             Gramext.Stoken ("SYMBOL", ";"));
 692          Gramext.Stoken ("SYMBOL", "]")],
 693         Gramext.action
 694           (fun _ (substs : 'e__2 list) _ _
 695              (loc : Lexing.position * Lexing.position) ->
 696              (substs : 'explicit_subst))]];
 697       Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
 698       [None, None,
 699        [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
 700         Gramext.action
 701           (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
 702              (Some p : 'meta_subst));
 703         [Gramext.Stoken ("SYMBOL", "_")],
 704         Gramext.action
 705           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
 706              (None : 'meta_subst))]];
 707       Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e), None,
 708       [None, None,
 709        [[Gramext.Stoken ("SYMBOL", "[");
 710          Gramext.Slist0
 711            (Gramext.Snterm
 712               (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e)));
 713          Gramext.Stoken ("SYMBOL", "]")],
 714         Gramext.action
 715           (fun _ (substs : 'meta_subst list) _
 716              (loc : Lexing.position * Lexing.position) ->
 717              (substs : 'meta_substs))]];
 718       Grammar.Entry.obj
 719         (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
 720       None,
 721       [None, None,
 722        [[Gramext.Snterm
 723            (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e))],
 724         Gramext.action
 725           (fun (arg : 'single_arg)
 726              (loc : Lexing.position * Lexing.position) ->
 727              (arg, None : 'possibly_typed_name));
 728         [Gramext.Stoken ("LPAREN", "");
 729          Gramext.Snterm
 730            (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e));
 731          Gramext.Stoken ("SYMBOL", ":");
 732          Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
 733          Gramext.Stoken ("RPAREN", "")],
 734         Gramext.action
 735           (fun _ (typ : 'term) _ (id : 'single_arg) _
 736              (loc : Lexing.position * Lexing.position) ->
 737              (id, Some typ : 'possibly_typed_name))]];
 738       Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
 739       None,
 740       [None, None,
 741        [[Gramext.Stoken ("LPAREN", ""); Gramext.Stoken ("IDENT", "");
 742          Gramext.Slist1
 743            (Gramext.Snterm
 744               (Grammar.Entry.obj
 745                  (possibly_typed_name :
 746                   'possibly_typed_name Grammar.Entry.e)));
 747          Gramext.Stoken ("RPAREN", "")],
 748         Gramext.action
 749           (fun _ (vars : 'possibly_typed_name list) (id : string) _
 750              (loc : Lexing.position * Lexing.position) ->
 751              (id, None, vars : 'match_pattern));
 752         [Gramext.Stoken ("IDENT", "")],
 753         Gramext.action
 754           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
 755              (id, None, [] : 'match_pattern))]];
 756       Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None,
 757       [None, None,
 758        [[Gramext.Stoken ("SYMBOL", "λ")],
 759         Gramext.action
 760           (fun _ (loc : Lexing.position * Lexing.position) ->
 761              (`Lambda : 'binder));
 762         [Gramext.Stoken ("SYMBOL", "∀")],
 763         Gramext.action
 764           (fun _ (loc : Lexing.position * Lexing.position) ->
 765              (`Forall : 'binder));
 766         [Gramext.Stoken ("SYMBOL", "Π")],
 767         Gramext.action
 768           (fun _ (loc : Lexing.position * Lexing.position) ->
 769              (`Pi : 'binder))]];
 770       Grammar.Entry.obj (arg : 'arg Grammar.Entry.e), None,
 771       [None, None,
 772        [[Gramext.Stoken ("UNPARSED_META", "")],
 773         Gramext.action
 774           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
 775              (let meta =
 776                 !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
 777               in
 778               match meta with
 779                 Ast.Variable (Ast.FreshVar _) -> [meta], None
 780               | Ast.Variable (Ast.TermVar "_") ->
 781                   [Ast.Ident ("_", None)], None
 782               | _ -> failwith "Invalid bound name." :
 783               'arg));
 784         [Gramext.Stoken ("IDENT", "")],
 785         Gramext.action
 786           (fun (name : string) (loc : Lexing.position * Lexing.position) ->
 787              ([Ast.Ident (name, None)], None : 'arg));
 788         [Gramext.Stoken ("LPAREN", "");
 789          Gramext.Slist1sep
 790            (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
 791          Gramext.Stoken ("SYMBOL", ":");
 792          Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
 793          Gramext.Stoken ("RPAREN", "")],
 794         Gramext.action
 795           (fun _ (ty : 'term) _ (names : string list) _
 796              (loc : Lexing.position * Lexing.position) ->
 797              (List.map (fun n -> Ast.Ident (n, None)) names, Some ty :
 798               'arg))]];
 799       Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e), None,
 800       [None, None,
 801        [[Gramext.Stoken ("UNPARSED_META", "")],
 802         Gramext.action
 803           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
 804              (let meta =
 805                 !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
 806               in
 807               match meta with
 808                 Ast.Variable (Ast.FreshVar _) |
 809                 Ast.Variable (Ast.IdentVar _) ->
 810                   meta
 811               | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
 812               | _ -> failwith "Invalid index name." :
 813               'single_arg));
 814         [Gramext.Stoken ("IDENT", "")],
 815         Gramext.action
 816           (fun (name : string) (loc : Lexing.position * Lexing.position) ->
 817              (Ast.Ident (name, None) : 'single_arg))]];
 818       Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
 819       None,
 820       [None, None,
 821        [[Gramext.Stoken ("", "corec")],
 822         Gramext.action
 823           (fun _ (loc : Lexing.position * Lexing.position) ->
 824              (`CoInductive : 'induction_kind));
 825         [Gramext.Stoken ("", "rec")],
 826         Gramext.action
 827           (fun _ (loc : Lexing.position * Lexing.position) ->
 828              (`Inductive : 'induction_kind))]];
 829       Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e), None,
 830       [None, None,
 831        [[Gramext.Slist1sep
 832            (Gramext.srules
 833               [[Gramext.Snterm
 834                   (Grammar.Entry.obj
 835                      (single_arg : 'single_arg Grammar.Entry.e));
 836                 Gramext.Slist1
 837                   (Gramext.Snterm
 838                      (Grammar.Entry.obj (arg : 'arg Grammar.Entry.e)));
 839                 Gramext.Sopt
 840                   (Gramext.srules
 841                      [[Gramext.Stoken ("", "on");
 842                        Gramext.Snterm
 843                          (Grammar.Entry.obj
 844                             (single_arg : 'single_arg Grammar.Entry.e))],
 845                       Gramext.action
 846                         (fun (id : 'single_arg) _
 847                            (loc : Lexing.position * Lexing.position) ->
 848                            (id : 'e__3))]);
 849                 Gramext.Sopt
 850                   (Gramext.srules
 851                      [[Gramext.Stoken ("SYMBOL", ":");
 852                        Gramext.Snterm
 853                          (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
 854                       Gramext.action
 855                         (fun (p : 'term) _
 856                            (loc : Lexing.position * Lexing.position) ->
 857                            (p : 'e__4))]);
 858                 Gramext.Stoken ("SYMBOL", "≝");
 859                 Gramext.Snterm
 860                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
 861                Gramext.action
 862                  (fun (body : 'term) _ (ty : 'e__4 option)
 863                     (index_name : 'e__3 option) (args : 'arg list)
 864                     (name : 'single_arg)
 865                     (loc : Lexing.position * Lexing.position) ->
 866                     (let body = fold_binder `Lambda args body in
 867                      let ty =
 868                        match ty with
 869                          None -> None
 870                        | Some ty -> Some (fold_binder `Pi args ty)
 871                      in
 872                      let rec position_of name p =
 873                        function
 874                          [] -> None, p
 875                        | n :: _ when n = name -> Some p, p
 876                        | _ :: tl -> position_of name (p + 1) tl
 877                      in
 878                      let rec find_arg name n =
 879                        function
 880                          [] ->
 881                            Ast.fail loc
 882                              (sprintf "Argument %s not found"
 883                                 (CicNotationPp.pp_term name))
 884                        | (l, _) :: tl ->
 885                            match position_of name 0 l with
 886                              None, len -> find_arg name (n + len) tl
 887                            | Some where, len -> n + where
 888                      in
 889                      let index =
 890                        match index_name with
 891                          None -> 0
 892                        | Some index_name -> find_arg index_name 0 args
 893                      in
 894                      (name, ty), body, index :
 895                      'e__5))],
 896             Gramext.Stoken ("", "and"))],
 897         Gramext.action
 898           (fun (defs : 'e__5 list)
 899              (loc : Lexing.position * Lexing.position) ->
 900              (defs : 'let_defs))]];
 901       Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e), None,
 902       [None, None,
 903        [[Gramext.Stoken ("LPAREN", "");
 904          Gramext.srules
 905            [[Gramext.Stoken ("SYMBOL", "_")],
 906             Gramext.action
 907               (fun _ (loc : Lexing.position * Lexing.position) ->
 908                  ([Ast.Ident ("_", None)] : 'e__8));
 909             [Gramext.Slist1sep
 910                (Gramext.Snterm
 911                   (Grammar.Entry.obj
 912                      (single_arg : 'single_arg Grammar.Entry.e)),
 913                 Gramext.Stoken ("SYMBOL", ","))],
 914             Gramext.action
 915               (fun (l : 'single_arg list)
 916                  (loc : Lexing.position * Lexing.position) ->
 917                  (l : 'e__8))];
 918          Gramext.Sopt
 919            (Gramext.srules
 920               [[Gramext.Stoken ("SYMBOL", ":");
 921                 Gramext.Snterm
 922                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
 923                Gramext.action
 924                  (fun (t : 'term) _
 925                     (loc : Lexing.position * Lexing.position) ->
 926                     (t : 'e__9))]);
 927          Gramext.Stoken ("RPAREN", "")],
 928         Gramext.action
 929           (fun _ (typ : 'e__9 option) (vars : 'e__8) _
 930              (loc : Lexing.position * Lexing.position) ->
 931              (vars, typ : 'binder_vars));
 932         [Gramext.srules
 933            [[Gramext.Stoken ("SYMBOL", "_")],
 934             Gramext.action
 935               (fun _ (loc : Lexing.position * Lexing.position) ->
 936                  ([Ast.Ident ("_", None)] : 'e__6));
 937             [Gramext.Slist1sep
 938                (Gramext.Snterm
 939                   (Grammar.Entry.obj
 940                      (single_arg : 'single_arg Grammar.Entry.e)),
 941                 Gramext.Stoken ("SYMBOL", ","))],
 942             Gramext.action
 943               (fun (l : 'single_arg list)
 944                  (loc : Lexing.position * Lexing.position) ->
 945                  (l : 'e__6))];
 946          Gramext.Sopt
 947            (Gramext.srules
 948               [[Gramext.Stoken ("SYMBOL", ":");
 949                 Gramext.Snterm
 950                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
 951                Gramext.action
 952                  (fun (t : 'term) _
 953                     (loc : Lexing.position * Lexing.position) ->
 954                     (t : 'e__7))])],
 955         Gramext.action
 956           (fun (typ : 'e__7 option) (vars : 'e__6)
 957              (loc : Lexing.position * Lexing.position) ->
 958              (vars, typ : 'binder_vars))]];
 959       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
 960       Some (Gramext.Level "10N"),
 961       [None, None,
 962        [[Gramext.Stoken ("", "let");
 963          Gramext.Snterm
 964            (Grammar.Entry.obj
 965               (induction_kind : 'induction_kind Grammar.Entry.e));
 966          Gramext.Snterm
 967            (Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e));
 968          Gramext.Stoken ("", "in"); Gramext.Sself],
 969         Gramext.action
 970           (fun (body : 'term) _ (defs : 'let_defs) (k : 'induction_kind) _
 971              (loc : Lexing.position * Lexing.position) ->
 972              (return_term loc (Ast.LetRec (k, defs, body)) : 'term));
 973         [Gramext.Stoken ("", "let");
 974          Gramext.Snterm
 975            (Grammar.Entry.obj
 976               (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e));
 977          Gramext.Stoken ("SYMBOL", "≝"); Gramext.Sself;
 978          Gramext.Stoken ("", "in"); Gramext.Sself],
 979         Gramext.action
 980           (fun (p2 : 'term) _ (p1 : 'term) _ (var : 'possibly_typed_name) _
 981              (loc : Lexing.position * Lexing.position) ->
 982              (return_term loc (Ast.LetIn (var, p1, p2)) : 'term))]];
 983       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
 984       Some (Gramext.Level "20R"),
 985       [None, None,
 986        [[Gramext.Stoken ("SYMBOL", "∃");
 987          Gramext.Snterm
 988            (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
 989          Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
 990         Gramext.action
 991           (fun (body : 'term) _ (vars, typ : 'binder_vars) _
 992              (loc : Lexing.position * Lexing.position) ->
 993              (return_term loc (fold_exists vars typ body) : 'term));
 994         [Gramext.Snterm
 995            (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
 996          Gramext.Snterm
 997            (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
 998          Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
 999         Gramext.action
1000           (fun (body : 'term) _ (vars, typ : 'binder_vars) (b : 'binder)
1001              (loc : Lexing.position * Lexing.position) ->
1002              (return_term loc (fold_cluster b vars typ body) : 'term))]];
1003       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
1004       Some (Gramext.Level "70L"),
1005       [None, None,
1006        [[Gramext.Sself; Gramext.Sself],
1007         Gramext.action
1008           (fun (p2 : 'term) (p1 : 'term)
1009              (loc : Lexing.position * Lexing.position) ->
1010              (let rec aux =
1011                 function
1012                   Ast.Appl (hd :: tl) |
1013                   Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
1014                     aux hd @ tl
1015                 | term -> [term]
1016               in
1017               return_term loc (Ast.Appl (aux p1 @ [p2])) :
1018               'term))]];
1019       Grammar.Entry.obj (term : 'term Grammar.Entry.e),
1020       Some (Gramext.Level "90N"),
1021       [None, None,
1022        [[Gramext.Stoken ("UNPARSED_META", "")],
1023         Gramext.action
1024           (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
1025              (!parse_level2_meta_ref (Ulexing.from_utf8_string blob) :
1026               'term));
1027         [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
1028          Gramext.Stoken ("RPAREN", "")],
1029         Gramext.action
1030           (fun _ (p : 'term) _ (loc : Lexing.position * Lexing.position) ->
1031              (p : 'term));
1032         [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
1033          Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
1034          Gramext.Stoken ("RPAREN", "")],
1035         Gramext.action
1036           (fun _ (p2 : 'term) _ (p1 : 'term) _
1037              (loc : Lexing.position * Lexing.position) ->
1038              (return_term loc (Ast.Cast (p1, p2)) : 'term));
1039         [Gramext.Sopt
1040            (Gramext.srules
1041               [[Gramext.Stoken ("SYMBOL", "[");
1042                 Gramext.Snterm
1043                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
1044                 Gramext.Stoken ("SYMBOL", "]")],
1045                Gramext.action
1046                  (fun _ (ty : 'term) _
1047                     (loc : Lexing.position * Lexing.position) ->
1048                     (ty : 'e__10))]);
1049          Gramext.Stoken ("", "match"); Gramext.Sself;
1050          Gramext.Sopt
1051            (Gramext.srules
1052               [[Gramext.Stoken ("", "in"); Gramext.Stoken ("IDENT", "")],
1053                Gramext.action
1054                  (fun (id : string) _
1055                     (loc : Lexing.position * Lexing.position) ->
1056                     (id, None : 'e__11))]);
1057          Gramext.Stoken ("", "with"); Gramext.Stoken ("SYMBOL", "[");
1058          Gramext.Slist0sep
1059            (Gramext.srules
1060               [[Gramext.Snterm
1061                   (Grammar.Entry.obj
1062                      (match_pattern : 'match_pattern Grammar.Entry.e));
1063                 Gramext.Stoken ("SYMBOL", "⇒");
1064                 Gramext.Snterm
1065                   (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
1066                Gramext.action
1067                  (fun (rhs : 'term) _ (lhs : 'match_pattern)
1068                     (loc : Lexing.position * Lexing.position) ->
1069                     (lhs, rhs : 'e__12))],
1070             Gramext.Stoken ("SYMBOL", "|"));
1071          Gramext.Stoken ("SYMBOL", "]")],
1072         Gramext.action
1073           (fun _ (patterns : 'e__12 list) _ _ (indty_ident : 'e__11 option)
1074              (t : 'term) _ (outtyp : 'e__10 option)
1075              (loc : Lexing.position * Lexing.position) ->
1076              (return_term loc (Ast.Case (t, indty_ident, outtyp, patterns)) :
1077               'term));
1078         [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
1079         Gramext.action
1080           (fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
1081              (return_term loc (Ast.Sort s) : 'term));
1082         [Gramext.Stoken ("META", "");
1083          Gramext.Snterm
1084            (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
1085         Gramext.action
1086           (fun (s : 'meta_substs) (m : string)
1087              (loc : Lexing.position * Lexing.position) ->
1088              (return_term loc (Ast.Meta (int_of_string m, s)) : 'term));
1089         [Gramext.Stoken ("META", "")],
1090         Gramext.action
1091           (fun (m : string) (loc : Lexing.position * Lexing.position) ->
1092              (return_term loc (Ast.Meta (int_of_string m, [])) : 'term));
1093         [Gramext.Stoken ("PLACEHOLDER", "")],
1094         Gramext.action
1095           (fun _ (loc : Lexing.position * Lexing.position) ->
1096              (return_term loc Ast.UserInput : 'term));
1097         [Gramext.Stoken ("IMPLICIT", "")],
1098         Gramext.action
1099           (fun _ (loc : Lexing.position * Lexing.position) ->
1100              (return_term loc Ast.Implicit : 'term));
1101         [Gramext.Stoken ("NUMBER", "")],
1102         Gramext.action
1103           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
1104              (return_term loc (Ast.Num (n, 0)) : 'term));
1105         [Gramext.Stoken ("URI", "")],
1106         Gramext.action
1107           (fun (u : string) (loc : Lexing.position * Lexing.position) ->
1108              (return_term loc (Ast.Uri (u, None)) : 'term));
1109         [Gramext.Stoken ("CSYMBOL", "")],
1110         Gramext.action
1111           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
1112              (return_term loc (Ast.Symbol (s, 0)) : 'term));
1113         [Gramext.Stoken ("IDENT", "");
1114          Gramext.Snterm
1115            (Grammar.Entry.obj
1116               (explicit_subst : 'explicit_subst Grammar.Entry.e))],
1117         Gramext.action
1118           (fun (s : 'explicit_subst) (id : string)
1119              (loc : Lexing.position * Lexing.position) ->
1120              (return_term loc (Ast.Ident (id, Some s)) : 'term));
1121         [Gramext.Stoken ("IDENT", "")],
1122         Gramext.action
1123           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
1124              (return_term loc (Ast.Ident (id, None)) : 'term))]]])
1125 (* }}} *)
1126
1127 (** {2 API implementation} *)
1128
1129 let exc_located_wrapper f =
1130   try f () with
1131     Stdpp.Exc_located (floc, Stream.Error msg) ->
1132       raise (Parse_error (floc, msg))
1133   | Stdpp.Exc_located (floc, exn) ->
1134       raise (Parse_error (floc, Printexc.to_string exn))
1135
1136 let parse_level1_pattern lexbuf =
1137   CicNotationLexer.set_lexbuf lexbuf;
1138   exc_located_wrapper
1139     (fun () -> Grammar.Entry.parse level1_pattern Stream.sempty)
1140
1141 let parse_level2_ast lexbuf =
1142   CicNotationLexer.set_lexbuf lexbuf;
1143   exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast Stream.sempty)
1144
1145 let parse_level2_meta lexbuf =
1146   CicNotationLexer.set_lexbuf lexbuf;
1147   exc_located_wrapper
1148     (fun () -> Grammar.Entry.parse level2_meta Stream.sempty)
1149
1150 let _ =
1151   parse_level1_pattern_ref := parse_level1_pattern;
1152   parse_level2_ast_ref := parse_level2_ast;
1153   parse_level2_meta_ref := parse_level2_meta
1154
1155 (** {2 Debugging} *)
1156
1157 let print_l2_pattern () =
1158   Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term);
1159   Format.pp_print_flush Format.std_formatter ();
1160   flush stdout
1161
1162 (* vim:set encoding=utf8 foldmethod=marker: *)