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