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