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