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