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