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 eexception Parse_error of Token.flocation * string
  28 llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
  29 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 notation = Grammar.Entry.create grammar "notation"(* level1 <-> level 2 *)
  30 llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *)
  31
  32 llet return_term loc term = ()
  33 llet loc_of_floc ({Lexing.pos_cnum = loc_begin}, {Lexing.pos_cnum = loc_end}) =
  34   loc_begin, loc_end
  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 oopen CicNotationPt
  43 llet boxify =
  44   function
  45     [a] -> a
  46   | l -> Layout (Box (H, l))
  47 llet fold_binder binder pt_names body =
  48   let fold_cluster binder names ty body =
  49     List.fold_right
  50       (fun name body -> Binder (binder, (Cic.Name name, ty), body)) names body
  51   in
  52   List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
  53     pt_names body
  54 llet return_term loc term = AttributedTerm (`Loc loc, term)
  55 Elet _ =
  56   Grammar.extend
  57     (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e)
  58      and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e)
  59      and _ = (level3_term : 'level3_term Grammar.Entry.e)
  60      and _ = (notation : 'notation Grammar.Entry.e)
  61      and _ = (interpretation : 'interpretation Grammar.Entry.e) in
  62      let grammar_entry_create s =
  63        Grammar.Entry.create (Grammar.of_entry level1_pattern) s
  64      in
  65      let l1_pattern : 'l1_pattern Grammar.Entry.e =
  66        grammar_entry_create "l1_pattern"
  67      and literal : 'literal Grammar.Entry.e = grammar_entry_create "literal"
  68      and sep : 'sep Grammar.Entry.e = grammar_entry_create "sep"
  69      and l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e =
  70        grammar_entry_create "l1_magic_pattern"
  71      and l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e =
  72        grammar_entry_create "l1_pattern_variable"
  73      and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e =
  74        grammar_entry_create "l1_simple_pattern"
  75      and sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
  76      and explicit_subst : 'explicit_subst Grammar.Entry.e =
  77        grammar_entry_create "explicit_subst"
  78      and meta_subst : 'meta_subst Grammar.Entry.e =
  79        grammar_entry_create "meta_subst"
  80      and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
  81        grammar_entry_create "possibly_typed_name"
  82      and match_pattern : 'match_pattern Grammar.Entry.e =
  83        grammar_entry_create "match_pattern"
  84      and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
  85      and bound_names : 'bound_names Grammar.Entry.e =
  86        grammar_entry_create "bound_names"
  87      and induction_kind : 'induction_kind Grammar.Entry.e =
  88        grammar_entry_create "induction_kind"
  89      and let_defs : 'let_defs Grammar.Entry.e =
  90        grammar_entry_create "let_defs"
  91      and l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e =
  92        grammar_entry_create "l2_pattern_variable"
  93      and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e =
  94        grammar_entry_create "l2_magic_pattern"
  95      and l2_pattern : 'l2_pattern Grammar.Entry.e =
  96        grammar_entry_create "l2_pattern"
  97      and argument : 'argument Grammar.Entry.e =
  98        grammar_entry_create "argument"
  99      and associativity : 'associativity Grammar.Entry.e =
 100        grammar_entry_create "associativity"
 101      and precedence : 'precedence Grammar.Entry.e =
 102        grammar_entry_create "precedence"
 103      in
 104      [Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e),
 105       None,
 106       [None, None,
 107        [[Gramext.Snterm
 108            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 109          Gramext.Stoken ("EOI", "")],
 110         Gramext.action
 111           (fun _ (p : 'l1_pattern)
 112              (loc : Lexing.position * Lexing.position) ->
 113              (boxify p : 'level1_pattern))]];
 114       Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
 115       [None, None,
 116        [[Gramext.Slist0
 117            (Gramext.Snterm
 118               (Grammar.Entry.obj
 119                  (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
 120         Gramext.action
 121           (fun (p : 'l1_simple_pattern list)
 122              (loc : Lexing.position * Lexing.position) ->
 123              (p : 'l1_pattern))]];
 124       Grammar.Entry.obj (literal : 'literal Grammar.Entry.e), None,
 125       [None, None,
 126        [[Gramext.Stoken ("NUMBER", "")],
 127         Gramext.action
 128           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
 129              (`Number n : 'literal));
 130         [Gramext.Stoken ("KEYWORD", "")],
 131         Gramext.action
 132           (fun (k : string) (loc : Lexing.position * Lexing.position) ->
 133              (`Keyword k : 'literal));
 134         [Gramext.Stoken ("SYMBOL", "")],
 135         Gramext.action
 136           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
 137              (`Symbol s : 'literal))]];
 138       Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None,
 139       [None, None,
 140        [[Gramext.Stoken ("SYMBOL", "\\SEP");
 141          Gramext.Snterm
 142            (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
 143         Gramext.action
 144           (fun (sep : 'literal) _ (loc : Lexing.position * Lexing.position) ->
 145              (sep : 'sep))]];
 146       Grammar.Entry.obj
 147         (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e),
 148       None,
 149       [None, None,
 150        [[Gramext.Stoken ("SYMBOL", "\\OPT");
 151          Gramext.Snterm
 152            (Grammar.Entry.obj
 153               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
 154         Gramext.action
 155           (fun (p : 'l1_simple_pattern) _
 156              (loc : Lexing.position * Lexing.position) ->
 157              (Opt p : 'l1_magic_pattern));
 158         [Gramext.Stoken ("SYMBOL", "\\LIST1");
 159          Gramext.Snterm
 160            (Grammar.Entry.obj
 161               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
 162          Gramext.Sopt
 163            (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
 164         Gramext.action
 165           (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
 166              (loc : Lexing.position * Lexing.position) ->
 167              (List1 (p, sep) : 'l1_magic_pattern));
 168         [Gramext.Stoken ("SYMBOL", "\\LIST0");
 169          Gramext.Snterm
 170            (Grammar.Entry.obj
 171               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
 172          Gramext.Sopt
 173            (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
 174         Gramext.action
 175           (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
 176              (loc : Lexing.position * Lexing.position) ->
 177              (List0 (p, sep) : 'l1_magic_pattern))]];
 178       Grammar.Entry.obj
 179         (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e),
 180       None,
 181       [None, None,
 182        [[Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
 183         Gramext.action
 184           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 185              (IdentVar id : 'l1_pattern_variable));
 186         [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
 187         Gramext.action
 188           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 189              (NumVar id : 'l1_pattern_variable));
 190         [Gramext.Stoken ("SYMBOL", "\\TERM"); Gramext.Stoken ("IDENT", "")],
 191         Gramext.action
 192           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 193              (TermVar id : 'l1_pattern_variable));
 194         [Gramext.Stoken ("IDENT", "")],
 195         Gramext.action
 196           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
 197              (TermVar id : 'l1_pattern_variable))]];
 198       Grammar.Entry.obj
 199         (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
 200       None,
 201       [Some "layout", Some Gramext.LeftA,
 202        [[Gramext.Stoken ("SYMBOL", "[");
 203          Gramext.Snterm
 204            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 205          Gramext.Stoken ("SYMBOL", "\\AS"); Gramext.Stoken ("IDENT", "");
 206          Gramext.Stoken ("SYMBOL", "]")],
 207         Gramext.action
 208           (fun _ (id : string) _ (p : 'l1_pattern) _
 209              (loc : Lexing.position * Lexing.position) ->
 210              (return_term loc
 211                 (Variable (Ascription (Layout (Box (H, p)), id))) :
 212               'l1_simple_pattern));
 213         [Gramext.Stoken ("SYMBOL", "[");
 214          Gramext.Snterm
 215            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 216          Gramext.Stoken ("SYMBOL", "]")],
 217         Gramext.action
 218           (fun _ (p : 'l1_pattern) _
 219              (loc : Lexing.position * Lexing.position) ->
 220              (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
 221         [Gramext.Stoken ("SYMBOL", "\\BREAK")],
 222         Gramext.action
 223           (fun _ (loc : Lexing.position * Lexing.position) ->
 224              (return_term loc (Layout Break) : 'l1_simple_pattern));
 225         [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("SYMBOL", "[");
 226          Gramext.Snterm
 227            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 228          Gramext.Stoken ("SYMBOL", "]")],
 229         Gramext.action
 230           (fun _ (p : 'l1_pattern) _ _
 231              (loc : Lexing.position * Lexing.position) ->
 232              (return_term loc (Layout (Box (V, p))) : 'l1_simple_pattern));
 233         [Gramext.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("SYMBOL", "[");
 234          Gramext.Snterm
 235            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 236          Gramext.Stoken ("SYMBOL", "]")],
 237         Gramext.action
 238           (fun _ (p : 'l1_pattern) _ _
 239              (loc : Lexing.position * Lexing.position) ->
 240              (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
 241         [Gramext.Stoken ("SYMBOL", "\\ROOT");
 242          Gramext.Snterm
 243            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 244          Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself],
 245         Gramext.action
 246           (fun (arg : 'l1_simple_pattern) _ (index : 'l1_pattern) _
 247              (loc : Lexing.position * Lexing.position) ->
 248              (return_term loc (Layout (Root (arg, Layout (Box (H, index))))) :
 249               'l1_simple_pattern));
 250         [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
 251         Gramext.action
 252           (fun (p : 'l1_simple_pattern) _
 253              (loc : Lexing.position * Lexing.position) ->
 254              (return_term loc (Layout (Sqrt p)) : 'l1_simple_pattern));
 255         [Gramext.Stoken ("SYMBOL", "\\FRAC"); Gramext.Sself; Gramext.Sself],
 256         Gramext.action
 257           (fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _
 258              (loc : Lexing.position * Lexing.position) ->
 259              (return_term loc (Layout (Frac (p1, p2))) : 'l1_simple_pattern));
 260         [Gramext.Stoken ("SYMBOL", "[");
 261          Gramext.Snterm
 262            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 263          Gramext.Stoken ("SYMBOL", "\\ATOP");
 264          Gramext.Snterm
 265            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 266          Gramext.Stoken ("SYMBOL", "]")],
 267         Gramext.action
 268           (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
 269              (loc : Lexing.position * Lexing.position) ->
 270              (return_term loc (Layout (Atop (boxify p1, boxify p2))) :
 271               'l1_simple_pattern));
 272         [Gramext.Stoken ("SYMBOL", "[");
 273          Gramext.Snterm
 274            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 275          Gramext.Stoken ("SYMBOL", "\\OVER");
 276          Gramext.Snterm
 277            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
 278          Gramext.Stoken ("SYMBOL", "]")],
 279         Gramext.action
 280           (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
 281              (loc : Lexing.position * Lexing.position) ->
 282              (return_term loc (Layout (Frac (boxify p1, boxify p2))) :
 283               'l1_simple_pattern));
 284         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
 285         Gramext.action
 286           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 287              (loc : Lexing.position * Lexing.position) ->
 288              (return_term loc (Layout (Above (p1, p2))) :
 289               'l1_simple_pattern));
 290         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\BELOW"); Gramext.Sself],
 291         Gramext.action
 292           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 293              (loc : Lexing.position * Lexing.position) ->
 294              (return_term loc (Layout (Below (p1, p2))) :
 295               'l1_simple_pattern));
 296         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUP"); Gramext.Sself],
 297         Gramext.action
 298           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 299              (loc : Lexing.position * Lexing.position) ->
 300              (return_term loc (Layout (Sup (p1, p2))) : 'l1_simple_pattern));
 301         [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUB"); Gramext.Sself],
 302         Gramext.action
 303           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
 304              (loc : Lexing.position * Lexing.position) ->
 305              (return_term loc (Layout (Sub (p1, p2))) : 'l1_simple_pattern))];
 306        Some "simple", Some Gramext.NonA,
 307        [[Gramext.Snterm
 308            (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
 309         Gramext.action
 310           (fun (l : 'literal) (loc : Lexing.position * Lexing.position) ->
 311              (return_term loc (Literal l) : 'l1_simple_pattern));
 312         [Gramext.Snterm
 313            (Grammar.Entry.obj
 314               (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e))],
 315         Gramext.action
 316           (fun (v : 'l1_pattern_variable)
 317              (loc : Lexing.position * Lexing.position) ->
 318              (return_term loc (Variable v) : 'l1_simple_pattern));
 319         [Gramext.Snterm
 320            (Grammar.Entry.obj
 321               (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e))],
 322         Gramext.action
 323           (fun (m : 'l1_magic_pattern)
 324              (loc : Lexing.position * Lexing.position) ->
 325              (return_term loc (Magic m) : 'l1_simple_pattern))]];
 326       Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e),
 327       None,
 328       [None, None,
 329        [[Gramext.Snterm
 330            (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 331         Gramext.action
 332           (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
 333              (p : 'level2_pattern))]];
 334       Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
 335       [None, None,
 336        [[Gramext.Stoken ("SYMBOL", "\\TYPE")],
 337         Gramext.action
 338           (fun _ (loc : Lexing.position * Lexing.position) ->
 339              (`Type : 'sort));
 340         [Gramext.Stoken ("SYMBOL", "\\SET")],
 341         Gramext.action
 342           (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
 343         [Gramext.Stoken ("SYMBOL", "\\PROP")],
 344         Gramext.action
 345           (fun _ (loc : Lexing.position * Lexing.position) ->
 346              (`Prop : 'sort))]];
 347       Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
 348       None, [None, None, []];
 349       Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
 350       [None, None, []];
 351       Grammar.Entry.obj
 352         (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
 353       None,
 354       [None, None,
 355        [[Gramext.Stoken ("IDENT", "")],
 356         Gramext.action
 357           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
 358              (Cic.Name id, None : 'possibly_typed_name));
 359         [Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
 360          Gramext.Stoken ("SYMBOL", ":");
 361          Gramext.Snterm
 362            (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
 363          Gramext.Stoken ("SYMBOL", ")")],
 364         Gramext.action
 365           (fun _ (typ : 'l2_pattern) _ (id : string) _
 366              (loc : Lexing.position * Lexing.position) ->
 367              (Cic.Name id, Some typ : 'possibly_typed_name))]];
 368       Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
 369       None,
 370       [None, None,
 371        [[Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
 372          Gramext.Slist1
 373            (Gramext.Snterm
 374               (Grammar.Entry.obj
 375                  (possibly_typed_name :
 376                   'possibly_typed_name Grammar.Entry.e)));
 377          Gramext.Stoken ("SYMBOL", ")")],
 378         Gramext.action
 379           (fun _ (vars : 'possibly_typed_name list) (id : string) _
 380              (loc : Lexing.position * Lexing.position) ->
 381              (id, vars : 'match_pattern));
 382         [Gramext.Stoken ("IDENT", "")],
 383         Gramext.action
 384           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
 385              (id, [] : 'match_pattern))]];
 386       Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None,
 387       [None, None,
 388        [[Gramext.Stoken ("SYMBOL", "λ")],
 389         Gramext.action
 390           (fun _ (loc : Lexing.position * Lexing.position) ->
 391              (`Lambda : 'binder));
 392         [Gramext.Stoken ("SYMBOL", "∀")],
 393         Gramext.action
 394           (fun _ (loc : Lexing.position * Lexing.position) ->
 395              (`Forall : 'binder));
 396         [Gramext.Stoken ("SYMBOL", "∃")],
 397         Gramext.action
 398           (fun _ (loc : Lexing.position * Lexing.position) ->
 399              (`Exists : 'binder));
 400         [Gramext.Stoken ("SYMBOL", "Π")],
 401         Gramext.action
 402           (fun _ (loc : Lexing.position * Lexing.position) ->
 403              (`Pi : 'binder))]];
 404       Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None,
 405       [None, None,
 406        [[Gramext.Slist1
 407            (Gramext.srules
 408               [[Gramext.Stoken ("SYMBOL", "(");
 409                 Gramext.Slist1sep
 410                   (Gramext.Stoken ("IDENT", ""),
 411                    Gramext.Stoken ("SYMBOL", ","));
 412                 Gramext.Sopt
 413                   (Gramext.srules
 414                      [[Gramext.Stoken ("SYMBOL", ":");
 415                        Gramext.Snterm
 416                          (Grammar.Entry.obj
 417                             (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 418                       Gramext.action
 419                         (fun (p : 'l2_pattern) _
 420                            (loc : Lexing.position * Lexing.position) ->
 421                            (p : 'e__2))]);
 422                 Gramext.Stoken ("SYMBOL", ")")],
 423                Gramext.action
 424                  (fun _ (ty : 'e__2 option) (vars : string list) _
 425                     (loc : Lexing.position * Lexing.position) ->
 426                     (vars, ty : 'e__3))])],
 427         Gramext.action
 428           (fun (clusters : 'e__3 list)
 429              (loc : Lexing.position * Lexing.position) ->
 430              (clusters : 'bound_names));
 431         [Gramext.Slist1sep
 432            (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
 433          Gramext.Sopt
 434            (Gramext.srules
 435               [[Gramext.Stoken ("SYMBOL", ":");
 436                 Gramext.Snterm
 437                   (Grammar.Entry.obj
 438                      (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 439                Gramext.action
 440                  (fun (p : 'l2_pattern) _
 441                     (loc : Lexing.position * Lexing.position) ->
 442                     (p : 'e__1))])],
 443         Gramext.action
 444           (fun (ty : 'e__1 option) (vars : string list)
 445              (loc : Lexing.position * Lexing.position) ->
 446              ([vars, ty] : 'bound_names))]];
 447       Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
 448       None,
 449       [None, None,
 450        [[Gramext.Stoken ("IDENT", "corec")],
 451         Gramext.action
 452           (fun _ (loc : Lexing.position * Lexing.position) ->
 453              (`CoInductive : 'induction_kind));
 454         [Gramext.Stoken ("IDENT", "rec")],
 455         Gramext.action
 456           (fun _ (loc : Lexing.position * Lexing.position) ->
 457              (`Inductive : 'induction_kind))]];
 458       Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e), None,
 459       [None, None,
 460        [[Gramext.Slist1sep
 461            (Gramext.srules
 462               [[Gramext.Stoken ("IDENT", "");
 463                 Gramext.Snterm
 464                   (Grammar.Entry.obj
 465                      (bound_names : 'bound_names Grammar.Entry.e));
 466                 Gramext.Sopt
 467                   (Gramext.srules
 468                      [[Gramext.Stoken ("IDENT", "on");
 469                        Gramext.Stoken ("IDENT", "")],
 470                       Gramext.action
 471                         (fun (id : string) _
 472                            (loc : Lexing.position * Lexing.position) ->
 473                            (id : 'e__4))]);
 474                 Gramext.Sopt
 475                   (Gramext.srules
 476                      [[Gramext.Stoken ("SYMBOL", ":");
 477                        Gramext.Snterm
 478                          (Grammar.Entry.obj
 479                             (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 480                       Gramext.action
 481                         (fun (p : 'l2_pattern) _
 482                            (loc : Lexing.position * Lexing.position) ->
 483                            (p : 'e__5))]);
 484                 Gramext.Stoken ("SYMBOL", "≝");
 485                 Gramext.Snterm
 486                   (Grammar.Entry.obj
 487                      (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 488                Gramext.action
 489                  (fun (body : 'l2_pattern) _ (ty : 'e__5 option)
 490                     (index_name : 'e__4 option) (args : 'bound_names)
 491                     (name : string)
 492                     (loc : Lexing.position * Lexing.position) ->
 493                     (let body = fold_binder `Lambda args body in
 494                      let ty =
 495                        match ty with
 496                          None -> None
 497                        | Some ty -> Some (fold_binder `Pi args ty)
 498                      in
 499                      let rec position_of name p =
 500                        function
 501                          [] -> None, p
 502                        | n :: _ when n = name -> Some p, p
 503                        | _ :: tl -> position_of name (p + 1) tl
 504                      in
 505                      let rec find_arg name n =
 506                        function
 507                          [] -> fail loc (sprintf "Argument %s not found" name)
 508                        | (l, _) :: tl ->
 509                            match position_of name 0 l with
 510                              None, len -> find_arg name (n + len) tl
 511                            | Some where, len -> n + where
 512                      in
 513                      let index =
 514                        match index_name with
 515                          None -> 0
 516                        | Some name -> find_arg name 0 args
 517                      in
 518                      (Cic.Name name, ty), body, index :
 519                      'e__6))],
 520             Gramext.Stoken ("IDENT", "and"))],
 521         Gramext.action
 522           (fun (defs : 'e__6 list)
 523              (loc : Lexing.position * Lexing.position) ->
 524              (defs : 'let_defs))]];
 525       Grammar.Entry.obj
 526         (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e),
 527       None,
 528       [None, None,
 529        [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
 530         Gramext.action
 531           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 532              (FreshVar id : 'l2_pattern_variable));
 533         [Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
 534         Gramext.action
 535           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 536              (IdentVar id : 'l2_pattern_variable));
 537         [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
 538         Gramext.action
 539           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
 540              (NumVar id : 'l2_pattern_variable))]];
 541       Grammar.Entry.obj
 542         (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e),
 543       None,
 544       [None, None,
 545        [[Gramext.Stoken ("SYMBOL", "\\DEFAULT");
 546          Gramext.Snterm
 547            (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
 548          Gramext.Snterm
 549            (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 550         Gramext.action
 551           (fun (none : 'l2_pattern) (some : 'l2_pattern) _
 552              (loc : Lexing.position * Lexing.position) ->
 553              (Default (some, none) : 'l2_magic_pattern));
 554         [Gramext.Stoken ("SYMBOL", "\\FOLD");
 555          Gramext.srules
 556            [[Gramext.Stoken ("IDENT", "right")],
 557             Gramext.action
 558               (fun _ (loc : Lexing.position * Lexing.position) ->
 559                  (`Right : 'e__7));
 560             [Gramext.Stoken ("IDENT", "left")],
 561             Gramext.action
 562               (fun _ (loc : Lexing.position * Lexing.position) ->
 563                  (`Left : 'e__7))];
 564          Gramext.Snterm
 565            (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
 566          Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", "");
 567          Gramext.Snterm
 568            (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 569         Gramext.action
 570           (fun (recursive : 'l2_pattern) (id : string) _ (base : 'l2_pattern)
 571              (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) ->
 572              (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
 573       Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), None,
 574       [Some "letin", Some Gramext.NonA,
 575        [[Gramext.Stoken ("IDENT", "let");
 576          Gramext.Snterm
 577            (Grammar.Entry.obj
 578               (induction_kind : 'induction_kind Grammar.Entry.e));
 579          Gramext.Snterm
 580            (Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e));
 581          Gramext.Stoken ("IDENT", "in"); Gramext.Sself],
 582         Gramext.action
 583           (fun (body : 'l2_pattern) _ (defs : 'let_defs) (k : 'induction_kind)
 584              _ (loc : Lexing.position * Lexing.position) ->
 585              (return_term loc (LetRec (k, defs, body)) : 'l2_pattern));
 586         [Gramext.Stoken ("IDENT", "let");
 587          Gramext.Snterm
 588            (Grammar.Entry.obj
 589               (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e));
 590          Gramext.Stoken ("SYMBOL", "≝"); Gramext.Sself;
 591          Gramext.Stoken ("", "in"); Gramext.Sself],
 592         Gramext.action
 593           (fun (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
 594              (var : 'possibly_typed_name) _
 595              (loc : Lexing.position * Lexing.position) ->
 596              (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))];
 597        Some "binder", Some Gramext.RightA,
 598        [[Gramext.Snterm
 599            (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
 600          Gramext.Snterm
 601            (Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e));
 602          Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
 603         Gramext.action
 604           (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder)
 605              (loc : Lexing.position * Lexing.position) ->
 606              (return_term loc (fold_binder b names body) : 'l2_pattern))];
 607        Some "extension", None, [];
 608        Some "apply", Some Gramext.LeftA,
 609        [[Gramext.Sself; Gramext.Sself],
 610         Gramext.action
 611           (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
 612              (loc : Lexing.position * Lexing.position) ->
 613              (let rec aux =
 614                 function
 615                   Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) ->
 616                     aux hd @ tl
 617                 | term -> [term]
 618               in
 619               return_term loc (Appl (aux p1 @ [p2])) :
 620               'l2_pattern))];
 621        Some "simple", Some Gramext.NonA,
 622        [[Gramext.Snterm
 623            (Grammar.Entry.obj
 624               (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))],
 625         Gramext.action
 626           (fun (m : 'l2_magic_pattern)
 627              (loc : Lexing.position * Lexing.position) ->
 628              (return_term loc (Magic m) : 'l2_pattern));
 629         [Gramext.Snterm
 630            (Grammar.Entry.obj
 631               (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e))],
 632         Gramext.action
 633           (fun (v : 'l2_pattern_variable)
 634              (loc : Lexing.position * Lexing.position) ->
 635              (return_term loc (Variable v) : 'l2_pattern));
 636         [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
 637          Gramext.Stoken ("SYMBOL", ")")],
 638         Gramext.action
 639           (fun _ (p : 'l2_pattern) _
 640              (loc : Lexing.position * Lexing.position) ->
 641              (p : 'l2_pattern));
 642         [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
 643          Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
 644          Gramext.Stoken ("SYMBOL", ")")],
 645         Gramext.action
 646           (fun _ (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
 647              (loc : Lexing.position * Lexing.position) ->
 648              (return_term loc (Appl [Symbol ("cast", 0); p1; p2]) :
 649               'l2_pattern));
 650         [Gramext.Sopt
 651            (Gramext.srules
 652               [[Gramext.Stoken ("SYMBOL", "[");
 653                 Gramext.Snterm
 654                   (Grammar.Entry.obj
 655                      (l2_pattern : 'l2_pattern Grammar.Entry.e));
 656                 Gramext.Stoken ("SYMBOL", "]")],
 657                Gramext.action
 658                  (fun _ (ty : 'l2_pattern) _
 659                     (loc : Lexing.position * Lexing.position) ->
 660                     (ty : 'e__8))]);
 661          Gramext.Stoken ("IDENT", "match"); Gramext.Sself;
 662          Gramext.Sopt
 663            (Gramext.srules
 664               [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Stoken ("IDENT", "")],
 665                Gramext.action
 666                  (fun (id : string) _
 667                     (loc : Lexing.position * Lexing.position) ->
 668                     (id : 'e__9))]);
 669          Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
 670          Gramext.Slist0sep
 671            (Gramext.srules
 672               [[Gramext.Snterm
 673                   (Grammar.Entry.obj
 674                      (match_pattern : 'match_pattern Grammar.Entry.e));
 675                 Gramext.Stoken ("SYMBOL", "⇒");
 676                 Gramext.Snterm
 677                   (Grammar.Entry.obj
 678                      (l2_pattern : 'l2_pattern Grammar.Entry.e))],
 679                Gramext.action
 680                  (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern)
 681                     (loc : Lexing.position * Lexing.position) ->
 682                     (lhs, rhs : 'e__10))],
 683             Gramext.Stoken ("SYMBOL", "|"));
 684          Gramext.Stoken ("SYMBOL", "]")],
 685         Gramext.action
 686           (fun _ (patterns : 'e__10 list) _ _ (indty_ident : 'e__9 option)
 687              (t : 'l2_pattern) _ (outtyp : 'e__8 option)
 688              (loc : Lexing.position * Lexing.position) ->
 689              (return_term loc (Case (t, indty_ident, outtyp, patterns)) :
 690               'l2_pattern));
 691         [Gramext.Stoken ("SYMBOL", "")],
 692         Gramext.action
 693           (fun (s : string) (loc : Lexing.position * Lexing.position) ->
 694              (return_term loc (Symbol (s, 0)) : 'l2_pattern));
 695         [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
 696         Gramext.action
 697           (fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
 698              (return_term loc (Sort s) : 'l2_pattern));
 699         [Gramext.Stoken ("META", "");
 700          Gramext.Snterm
 701            (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e))],
 702         Gramext.action
 703           (fun (s : 'meta_subst) (m : string)
 704              (loc : Lexing.position * Lexing.position) ->
 705              (return_term loc (Meta (int_of_string m, s)) : 'l2_pattern));
 706         [Gramext.Stoken ("META", "")],
 707         Gramext.action
 708           (fun (m : string) (loc : Lexing.position * Lexing.position) ->
 709              (return_term loc (Meta (int_of_string m, [])) : 'l2_pattern));
 710         [Gramext.Stoken ("IMPLICIT", "")],
 711         Gramext.action
 712           (fun _ (loc : Lexing.position * Lexing.position) ->
 713              (return_term loc Implicit : 'l2_pattern));
 714         [Gramext.Stoken ("NUMBER", "")],
 715         Gramext.action
 716           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
 717              (return_term loc (Num (n, 0)) : 'l2_pattern));
 718         [Gramext.Stoken ("URI", "")],
 719         Gramext.action
 720           (fun (u : string) (loc : Lexing.position * Lexing.position) ->
 721              (return_term loc (Uri (u, None)) : 'l2_pattern));
 722         [Gramext.Stoken ("IDENT", "");
 723          Gramext.Snterm
 724            (Grammar.Entry.obj
 725               (explicit_subst : 'explicit_subst Grammar.Entry.e))],
 726         Gramext.action
 727           (fun (s : 'explicit_subst) (id : string)
 728              (loc : Lexing.position * Lexing.position) ->
 729              (return_term loc (Ident (id, Some s)) : 'l2_pattern));
 730         [Gramext.Stoken ("IDENT", "")],
 731         Gramext.action
 732           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
 733              (return_term loc (Ident (id, None)) : 'l2_pattern))]];
 734       Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None,
 735       [None, None,
 736        [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", "");
 737          Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
 738         Gramext.action
 739           (fun (a : 'argument) _ (id : string) _
 740              (loc : Lexing.position * Lexing.position) ->
 741              (EtaArg (Some id, a) : 'argument));
 742         [Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("SYMBOL", ".");
 743          Gramext.Sself],
 744         Gramext.action
 745           (fun (a : 'argument) _ _
 746              (loc : Lexing.position * Lexing.position) ->
 747              (EtaArg (None, a) : 'argument));
 748         [Gramext.Stoken ("IDENT", "")],
 749         Gramext.action
 750           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
 751              (IdentArg id : 'argument))]];
 752       Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e), None,
 753       [None, None,
 754        [[Gramext.Stoken ("SYMBOL", "("); Gramext.Slist1 Gramext.Sself;
 755          Gramext.Stoken ("SYMBOL", ")")],
 756         Gramext.action
 757           (fun _ (terms : 'level3_term list) _
 758              (loc : Lexing.position * Lexing.position) ->
 759              (match terms with
 760                 [] -> assert false
 761               | [term] -> term
 762               | terms -> ApplPattern terms :
 763               'level3_term));
 764         [Gramext.Snterm
 765            (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e))],
 766         Gramext.action
 767           (fun (a : 'argument) (loc : Lexing.position * Lexing.position) ->
 768              (ArgPattern a : 'level3_term));
 769         [Gramext.Stoken ("URI", "")],
 770         Gramext.action
 771           (fun (u : string) (loc : Lexing.position * Lexing.position) ->
 772              (UriPattern u : 'level3_term))]];
 773       Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e),
 774       None,
 775       [None, None,
 776        [[Gramext.Stoken ("IDENT", "right");
 777          Gramext.Stoken ("IDENT", "associative")],
 778         Gramext.action
 779           (fun _ _ (loc : Lexing.position * Lexing.position) ->
 780              (`Right : 'associativity));
 781         [Gramext.Stoken ("IDENT", "left");
 782          Gramext.Stoken ("IDENT", "associative")],
 783         Gramext.action
 784           (fun _ _ (loc : Lexing.position * Lexing.position) ->
 785              (`Left : 'associativity))]];
 786       Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
 787       [None, None,
 788        [[Gramext.Stoken ("IDENT", "at");
 789          Gramext.Stoken ("IDENT", "precedence");
 790          Gramext.Stoken ("NUMBER", "")],
 791         Gramext.action
 792           (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
 793              (n : 'precedence))]];
 794       Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None,
 795       [None, None,
 796        [[Gramext.Stoken ("IDENT", "notation");
 797          Gramext.Snterm
 798            (Grammar.Entry.obj
 799               (level1_pattern : 'level1_pattern Grammar.Entry.e));
 800          Gramext.Stoken ("IDENT", "for");
 801          Gramext.Snterm
 802            (Grammar.Entry.obj
 803               (level2_pattern : 'level2_pattern Grammar.Entry.e));
 804          Gramext.Sopt
 805            (Gramext.Snterm
 806               (Grammar.Entry.obj
 807                  (associativity : 'associativity Grammar.Entry.e)));
 808          Gramext.Sopt
 809            (Gramext.Snterm
 810               (Grammar.Entry.obj
 811                  (precedence : 'precedence Grammar.Entry.e)))],
 812         Gramext.action
 813           (fun (prec : 'precedence option) (assoc : 'associativity option)
 814              (p2 : 'level2_pattern) _ (p1 : 'level1_pattern) _
 815              (loc : Lexing.position * Lexing.position) ->
 816              (() : 'notation))]];
 817       Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
 818       None,
 819       [None, None,
 820        [[Gramext.Stoken ("IDENT", "interpretation");
 821          Gramext.Stoken ("SYMBOL", "");
 822          Gramext.Slist1
 823            (Gramext.Snterm
 824               (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e)));
 825          Gramext.Stoken ("IDENT", "as");
 826          Gramext.Snterm
 827            (Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e))],
 828         Gramext.action
 829           (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
 830              (loc : Lexing.position * Lexing.position) ->
 831              (() : 'interpretation))]]])
 832
 833 let exc_located_wrapper f =
 834   try f () with
 835     Stdpp.Exc_located (floc, Stream.Error msg) ->
 836       raise (Parse_error (floc, msg))
 837   | Stdpp.Exc_located (floc, exn) ->
 838       raise (Parse_error (floc, Printexc.to_string exn))
 839
 840 let parse_syntax_pattern stream =
 841   exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
 842
 843 let parse_ast_pattern stream =
 844   exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
 845
 846 let parse_interpretation stream =
 847   exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
 848
 849 (* vim:set encoding=utf8 foldmethod=marker: *)