(* *)(* Copyright (C) 2005, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://helm.cs.unibo.it/
 *)

oopen Printf
eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
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 *)
llet interpretation = Grammar.Entry.create grammar "interpretation"(* level2 <-> level 3 *)

llet return_term loc term = ()
llet loc_of_floc ({Lexing.pos_cnum = loc_begin}, {Lexing.pos_cnum = loc_end}) =
  loc_begin, loc_end
llet fail floc msg =
  let (x, y) = loc_of_floc floc in
  failwith (sprintf "Error at characters %d - %d: %s" x y msg)
llet int_of_string s =
  try Pervasives.int_of_string s with
    Failure _ ->
      failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
oopen CicNotationPt
llet boxify =
  function
    [a] -> a
  | l -> Layout (Box (H, l))
llet fold_binder binder pt_names body =
  let fold_cluster binder names ty body =
    List.fold_right
      (fun name body -> Binder (binder, (Cic.Name name, ty), body)) names body
  in
  List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
    pt_names body
llet return_term loc term = AttributedTerm (`Loc loc, term)
Elet _ =
  Grammar.extend
    (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e)
     and _ = (level2_pattern : 'level2_pattern Grammar.Entry.e)
     and _ = (level3_term : 'level3_term Grammar.Entry.e)
     and _ = (l2_pattern : 'l2_pattern Grammar.Entry.e)
     and _ = (notation : 'notation Grammar.Entry.e)
     and _ = (interpretation : 'interpretation Grammar.Entry.e) in
     let grammar_entry_create s =
       Grammar.Entry.create (Grammar.of_entry level1_pattern) s
     in
     let l1_pattern : 'l1_pattern Grammar.Entry.e =
       grammar_entry_create "l1_pattern"
     and literal : 'literal Grammar.Entry.e = grammar_entry_create "literal"
     and sep : 'sep Grammar.Entry.e = grammar_entry_create "sep"
     and l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e =
       grammar_entry_create "l1_magic_pattern"
     and l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e =
       grammar_entry_create "l1_pattern_variable"
     and l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e =
       grammar_entry_create "l1_simple_pattern"
     and sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
     and explicit_subst : 'explicit_subst Grammar.Entry.e =
       grammar_entry_create "explicit_subst"
     and meta_subst : 'meta_subst Grammar.Entry.e =
       grammar_entry_create "meta_subst"
     and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
       grammar_entry_create "possibly_typed_name"
     and match_pattern : 'match_pattern Grammar.Entry.e =
       grammar_entry_create "match_pattern"
     and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
     and bound_names : 'bound_names Grammar.Entry.e =
       grammar_entry_create "bound_names"
     and induction_kind : 'induction_kind Grammar.Entry.e =
       grammar_entry_create "induction_kind"
     and let_defs : 'let_defs Grammar.Entry.e =
       grammar_entry_create "let_defs"
     and l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e =
       grammar_entry_create "l2_pattern_variable"
     and l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e =
       grammar_entry_create "l2_magic_pattern"
     and argument : 'argument Grammar.Entry.e =
       grammar_entry_create "argument"
     and associativity : 'associativity Grammar.Entry.e =
       grammar_entry_create "associativity"
     and precedence : 'precedence Grammar.Entry.e =
       grammar_entry_create "precedence"
     in
     [Grammar.Entry.obj (level1_pattern : 'level1_pattern Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("EOI", "")],
        Gramext.action
          (fun _ (p : 'l1_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (boxify p : 'level1_pattern))]];
      Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Slist0
           (Gramext.Snterm
              (Grammar.Entry.obj
                 (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
        Gramext.action
          (fun (p : 'l1_simple_pattern list)
             (loc : Lexing.position * Lexing.position) ->
             (p : 'l1_pattern))]];
      Grammar.Entry.obj (literal : 'literal Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("NUMBER", "")],
        Gramext.action
          (fun (n : string) (loc : Lexing.position * Lexing.position) ->
             (`Number n : 'literal));
        [Gramext.Stoken ("KEYWORD", "")],
        Gramext.action
          (fun (k : string) (loc : Lexing.position * Lexing.position) ->
             (`Keyword k : 'literal));
        [Gramext.Stoken ("SYMBOL", "")],
        Gramext.action
          (fun (s : string) (loc : Lexing.position * Lexing.position) ->
             (`Symbol s : 'literal))]];
      Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "\\SEP");
         Gramext.Snterm
           (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
        Gramext.action
          (fun (sep : 'literal) _ (loc : Lexing.position * Lexing.position) ->
             (sep : 'sep))]];
      Grammar.Entry.obj
        (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "\\OPT");
         Gramext.Snterm
           (Grammar.Entry.obj
              (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
        Gramext.action
          (fun (p : 'l1_simple_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (Opt p : 'l1_magic_pattern));
        [Gramext.Stoken ("SYMBOL", "\\LIST1");
         Gramext.Snterm
           (Grammar.Entry.obj
              (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
         Gramext.Sopt
           (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
        Gramext.action
          (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (List1 (p, sep) : 'l1_magic_pattern));
        [Gramext.Stoken ("SYMBOL", "\\LIST0");
         Gramext.Snterm
           (Grammar.Entry.obj
              (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
         Gramext.Sopt
           (Gramext.Snterm (Grammar.Entry.obj (sep : 'sep Grammar.Entry.e)))],
        Gramext.action
          (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (List0 (p, sep) : 'l1_magic_pattern))]];
      Grammar.Entry.obj
        (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
             (IdentVar id : 'l1_pattern_variable));
        [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
             (NumVar id : 'l1_pattern_variable));
        [Gramext.Stoken ("SYMBOL", "\\TERM"); Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
             (TermVar id : 'l1_pattern_variable));
        [Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) (loc : Lexing.position * Lexing.position) ->
             (TermVar id : 'l1_pattern_variable))]];
      Grammar.Entry.obj
        (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
      None,
      [Some "layout", Some Gramext.LeftA,
       [[Gramext.Stoken ("SYMBOL", "[");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "\\AS"); Gramext.Stoken ("IDENT", "");
         Gramext.Stoken ("SYMBOL", "]")],
        Gramext.action
          (fun _ (id : string) _ (p : 'l1_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc
                (Variable (Ascription (Layout (Box (H, p)), id))) :
              'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "[");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "]")],
        Gramext.action
          (fun _ (p : 'l1_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (boxify p) : 'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "\\BREAK")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout Break) : 'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("SYMBOL", "[");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "]")],
        Gramext.action
          (fun _ (p : 'l1_pattern) _ _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Box (V, p))) : 'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("SYMBOL", "[");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "]")],
        Gramext.action
          (fun _ (p : 'l1_pattern) _ _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Box (H, p))) : 'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "\\ROOT");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself],
        Gramext.action
          (fun (arg : 'l1_simple_pattern) _ (index : 'l1_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Root (arg, Layout (Box (H, index))))) :
              'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
        Gramext.action
          (fun (p : 'l1_simple_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Sqrt p)) : 'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "\\FRAC"); Gramext.Sself; Gramext.Sself],
        Gramext.action
          (fun (p2 : 'l1_simple_pattern) (p1 : 'l1_simple_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Frac (p1, p2))) : 'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "[");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "\\ATOP");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "]")],
        Gramext.action
          (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Atop (boxify p1, boxify p2))) :
              'l1_simple_pattern));
        [Gramext.Stoken ("SYMBOL", "[");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "\\OVER");
         Gramext.Snterm
           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "]")],
        Gramext.action
          (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Over (boxify p1, boxify p2))) :
              'l1_simple_pattern));
        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
        Gramext.action
          (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Above (p1, p2))) :
              'l1_simple_pattern));
        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\BELOW"); Gramext.Sself],
        Gramext.action
          (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Below (p1, p2))) :
              'l1_simple_pattern));
        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUP"); Gramext.Sself],
        Gramext.action
          (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Sup (p1, p2))) : 'l1_simple_pattern));
        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUB"); Gramext.Sself],
        Gramext.action
          (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Layout (Sub (p1, p2))) : 'l1_simple_pattern))];
       Some "simple", Some Gramext.NonA,
       [[Gramext.Snterm
           (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
        Gramext.action
          (fun (l : 'literal) (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Literal l) : 'l1_simple_pattern));
        [Gramext.Snterm
           (Grammar.Entry.obj
              (l1_pattern_variable : 'l1_pattern_variable Grammar.Entry.e))],
        Gramext.action
          (fun (v : 'l1_pattern_variable)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Variable v) : 'l1_simple_pattern));
        [Gramext.Snterm
           (Grammar.Entry.obj
              (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e))],
        Gramext.action
          (fun (m : 'l1_magic_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Magic m) : 'l1_simple_pattern))]];
      Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Snterm
           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
        Gramext.action
          (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
             (p : 'level2_pattern))]];
      Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "\\TYPE")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`Type : 'sort));
        [Gramext.Stoken ("SYMBOL", "\\SET")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
        [Gramext.Stoken ("SYMBOL", "\\PROP")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`Prop : 'sort))]];
      Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
      None, [None, None, []];
      Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
      [None, None, []];
      Grammar.Entry.obj
        (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) (loc : Lexing.position * Lexing.position) ->
             (Cic.Name id, None : 'possibly_typed_name));
        [Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
         Gramext.Stoken ("SYMBOL", ":");
         Gramext.Snterm
           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", ")")],
        Gramext.action
          (fun _ (typ : 'l2_pattern) _ (id : string) _
             (loc : Lexing.position * Lexing.position) ->
             (Cic.Name id, Some typ : 'possibly_typed_name))]];
      Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
         Gramext.Slist1
           (Gramext.Snterm
              (Grammar.Entry.obj
                 (possibly_typed_name :
                  'possibly_typed_name Grammar.Entry.e)));
         Gramext.Stoken ("SYMBOL", ")")],
        Gramext.action
          (fun _ (vars : 'possibly_typed_name list) (id : string) _
             (loc : Lexing.position * Lexing.position) ->
             (id, vars : 'match_pattern));
        [Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) (loc : Lexing.position * Lexing.position) ->
             (id, [] : 'match_pattern))]];
      Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "λ")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`Lambda : 'binder));
        [Gramext.Stoken ("SYMBOL", "∀")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`Forall : 'binder));
        [Gramext.Stoken ("SYMBOL", "∃")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`Exists : 'binder));
        [Gramext.Stoken ("SYMBOL", "Π")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`Pi : 'binder))]];
      Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Slist1
           (Gramext.srules
              [[Gramext.Stoken ("SYMBOL", "(");
                Gramext.Slist1sep
                  (Gramext.Stoken ("IDENT", ""),
                   Gramext.Stoken ("SYMBOL", ","));
                Gramext.Sopt
                  (Gramext.srules
                     [[Gramext.Stoken ("SYMBOL", ":");
                       Gramext.Snterm
                         (Grammar.Entry.obj
                            (l2_pattern : 'l2_pattern Grammar.Entry.e))],
                      Gramext.action
                        (fun (p : 'l2_pattern) _
                           (loc : Lexing.position * Lexing.position) ->
                           (p : 'e__2))]);
                Gramext.Stoken ("SYMBOL", ")")],
               Gramext.action
                 (fun _ (ty : 'e__2 option) (vars : string list) _
                    (loc : Lexing.position * Lexing.position) ->
                    (vars, ty : 'e__3))])],
        Gramext.action
          (fun (clusters : 'e__3 list)
             (loc : Lexing.position * Lexing.position) ->
             (clusters : 'bound_names));
        [Gramext.Slist1sep
           (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
         Gramext.Sopt
           (Gramext.srules
              [[Gramext.Stoken ("SYMBOL", ":");
                Gramext.Snterm
                  (Grammar.Entry.obj
                     (l2_pattern : 'l2_pattern Grammar.Entry.e))],
               Gramext.action
                 (fun (p : 'l2_pattern) _
                    (loc : Lexing.position * Lexing.position) ->
                    (p : 'e__1))])],
        Gramext.action
          (fun (ty : 'e__1 option) (vars : string list)
             (loc : Lexing.position * Lexing.position) ->
             ([vars, ty] : 'bound_names))]];
      Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("IDENT", "corec")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`CoInductive : 'induction_kind));
        [Gramext.Stoken ("IDENT", "rec")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (`Inductive : 'induction_kind))]];
      Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Slist1sep
           (Gramext.srules
              [[Gramext.Stoken ("IDENT", "");
                Gramext.Snterm
                  (Grammar.Entry.obj
                     (bound_names : 'bound_names Grammar.Entry.e));
                Gramext.Sopt
                  (Gramext.srules
                     [[Gramext.Stoken ("IDENT", "on");
                       Gramext.Stoken ("IDENT", "")],
                      Gramext.action
                        (fun (id : string) _
                           (loc : Lexing.position * Lexing.position) ->
                           (id : 'e__4))]);
                Gramext.Sopt
                  (Gramext.srules
                     [[Gramext.Stoken ("SYMBOL", ":");
                       Gramext.Snterm
                         (Grammar.Entry.obj
                            (l2_pattern : 'l2_pattern Grammar.Entry.e))],
                      Gramext.action
                        (fun (p : 'l2_pattern) _
                           (loc : Lexing.position * Lexing.position) ->
                           (p : 'e__5))]);
                Gramext.Stoken ("SYMBOL", "≝");
                Gramext.Snterm
                  (Grammar.Entry.obj
                     (l2_pattern : 'l2_pattern Grammar.Entry.e))],
               Gramext.action
                 (fun (body : 'l2_pattern) _ (ty : 'e__5 option)
                    (index_name : 'e__4 option) (args : 'bound_names)
                    (name : string)
                    (loc : Lexing.position * Lexing.position) ->
                    (let body = fold_binder `Lambda args body in
                     let ty =
                       match ty with
                         None -> None
                       | Some ty -> Some (fold_binder `Pi args ty)
                     in
                     let rec position_of name p =
                       function
                         [] -> None, p
                       | n :: _ when n = name -> Some p, p
                       | _ :: tl -> position_of name (p + 1) tl
                     in
                     let rec find_arg name n =
                       function
                         [] -> fail loc (sprintf "Argument %s not found" name)
                       | (l, _) :: tl ->
                           match position_of name 0 l with
                             None, len -> find_arg name (n + len) tl
                           | Some where, len -> n + where
                     in
                     let index =
                       match index_name with
                         None -> 0
                       | Some name -> find_arg name 0 args
                     in
                     (Cic.Name name, ty), body, index :
                     'e__6))],
            Gramext.Stoken ("IDENT", "and"))],
        Gramext.action
          (fun (defs : 'e__6 list)
             (loc : Lexing.position * Lexing.position) ->
             (defs : 'let_defs))]];
      Grammar.Entry.obj
        (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
             (FreshVar id : 'l2_pattern_variable));
        [Gramext.Stoken ("SYMBOL", "\\IDENT"); Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
             (IdentVar id : 'l2_pattern_variable));
        [Gramext.Stoken ("SYMBOL", "\\NUM"); Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
             (NumVar id : 'l2_pattern_variable))]];
      Grammar.Entry.obj
        (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "\\DEFAULT");
         Gramext.Snterm
           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
         Gramext.Snterm
           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
        Gramext.action
          (fun (none : 'l2_pattern) (some : 'l2_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (Default (some, none) : 'l2_magic_pattern));
        [Gramext.Stoken ("SYMBOL", "\\FOLD");
         Gramext.srules
           [[Gramext.Stoken ("IDENT", "right")],
            Gramext.action
              (fun _ (loc : Lexing.position * Lexing.position) ->
                 (`Right : 'e__7));
            [Gramext.Stoken ("IDENT", "left")],
            Gramext.action
              (fun _ (loc : Lexing.position * Lexing.position) ->
                 (`Left : 'e__7))];
         Gramext.Snterm
           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", "");
         Gramext.Snterm
           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
        Gramext.action
          (fun (recursive : 'l2_pattern) (id : string) _ (base : 'l2_pattern)
             (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) ->
             (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
      Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e), None,
      [Some "0", None, [];
       Some "10", Some Gramext.NonA,
       [[Gramext.Stoken ("IDENT", "let");
         Gramext.Snterm
           (Grammar.Entry.obj
              (induction_kind : 'induction_kind Grammar.Entry.e));
         Gramext.Snterm
           (Grammar.Entry.obj (let_defs : 'let_defs Grammar.Entry.e));
         Gramext.Stoken ("IDENT", "in"); Gramext.Sself],
        Gramext.action
          (fun (body : 'l2_pattern) _ (defs : 'let_defs) (k : 'induction_kind)
             _ (loc : Lexing.position * Lexing.position) ->
             (return_term loc (LetRec (k, defs, body)) : 'l2_pattern));
        [Gramext.Stoken ("IDENT", "let");
         Gramext.Snterm
           (Grammar.Entry.obj
              (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "≝"); Gramext.Sself;
         Gramext.Stoken ("", "in"); Gramext.Sself],
        Gramext.action
          (fun (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
             (var : 'possibly_typed_name) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))];
       Some "20", Some Gramext.RightA,
       [[Gramext.Snterm
           (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
         Gramext.Snterm
           (Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e));
         Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
        Gramext.action
          (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (fold_binder b names body) : 'l2_pattern))];
       Some "30", None, []; Some "40", None, []; Some "50", None, [];
       Some "60", None, [];
       Some "70", Some Gramext.LeftA,
       [[Gramext.Sself; Gramext.Sself],
        Gramext.action
          (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (let rec aux =
                function
                  Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) ->
                    aux hd @ tl
                | term -> [term]
              in
              return_term loc (Appl (aux p1 @ [p2])) :
              'l2_pattern))];
       Some "80", None, [];
       Some "90", Some Gramext.NonA,
       [[Gramext.Snterm
           (Grammar.Entry.obj
              (l2_magic_pattern : 'l2_magic_pattern Grammar.Entry.e))],
        Gramext.action
          (fun (m : 'l2_magic_pattern)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Magic m) : 'l2_pattern));
        [Gramext.Snterm
           (Grammar.Entry.obj
              (l2_pattern_variable : 'l2_pattern_variable Grammar.Entry.e))],
        Gramext.action
          (fun (v : 'l2_pattern_variable)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Variable v) : 'l2_pattern));
        [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
         Gramext.Stoken ("SYMBOL", ")")],
        Gramext.action
          (fun _ (p : 'l2_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (p : 'l2_pattern));
        [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
         Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
         Gramext.Stoken ("SYMBOL", ")")],
        Gramext.action
          (fun _ (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Appl [Symbol ("cast", 0); p1; p2]) :
              'l2_pattern));
        [Gramext.Sopt
           (Gramext.srules
              [[Gramext.Stoken ("SYMBOL", "[");
                Gramext.Snterm
                  (Grammar.Entry.obj
                     (l2_pattern : 'l2_pattern Grammar.Entry.e));
                Gramext.Stoken ("SYMBOL", "]")],
               Gramext.action
                 (fun _ (ty : 'l2_pattern) _
                    (loc : Lexing.position * Lexing.position) ->
                    (ty : 'e__8))]);
         Gramext.Stoken ("IDENT", "match"); Gramext.Sself;
         Gramext.Sopt
           (Gramext.srules
              [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Stoken ("IDENT", "")],
               Gramext.action
                 (fun (id : string) _
                    (loc : Lexing.position * Lexing.position) ->
                    (id : 'e__9))]);
         Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
         Gramext.Slist0sep
           (Gramext.srules
              [[Gramext.Snterm
                  (Grammar.Entry.obj
                     (match_pattern : 'match_pattern Grammar.Entry.e));
                Gramext.Stoken ("SYMBOL", "⇒");
                Gramext.Snterm
                  (Grammar.Entry.obj
                     (l2_pattern : 'l2_pattern Grammar.Entry.e))],
               Gramext.action
                 (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern)
                    (loc : Lexing.position * Lexing.position) ->
                    (lhs, rhs : 'e__10))],
            Gramext.Stoken ("SYMBOL", "|"));
         Gramext.Stoken ("SYMBOL", "]")],
        Gramext.action
          (fun _ (patterns : 'e__10 list) _ _ (indty_ident : 'e__9 option)
             (t : 'l2_pattern) _ (outtyp : 'e__8 option)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Case (t, indty_ident, outtyp, patterns)) :
              'l2_pattern));
        [Gramext.Stoken ("SYMBOL", "")],
        Gramext.action
          (fun (s : string) (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Symbol (s, 0)) : 'l2_pattern));
        [Gramext.Snterm (Grammar.Entry.obj (sort : 'sort Grammar.Entry.e))],
        Gramext.action
          (fun (s : 'sort) (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Sort s) : 'l2_pattern));
        [Gramext.Stoken ("META", "");
         Gramext.Snterm
           (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e))],
        Gramext.action
          (fun (s : 'meta_subst) (m : string)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Meta (int_of_string m, s)) : 'l2_pattern));
        [Gramext.Stoken ("META", "")],
        Gramext.action
          (fun (m : string) (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Meta (int_of_string m, [])) : 'l2_pattern));
        [Gramext.Stoken ("IMPLICIT", "")],
        Gramext.action
          (fun _ (loc : Lexing.position * Lexing.position) ->
             (return_term loc Implicit : 'l2_pattern));
        [Gramext.Stoken ("NUMBER", "")],
        Gramext.action
          (fun (n : string) (loc : Lexing.position * Lexing.position) ->
             (prerr_endline "number"; return_term loc (Num (n, 0)) :
              'l2_pattern));
        [Gramext.Stoken ("URI", "")],
        Gramext.action
          (fun (u : string) (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Uri (u, None)) : 'l2_pattern));
        [Gramext.Stoken ("IDENT", "");
         Gramext.Snterm
           (Grammar.Entry.obj
              (explicit_subst : 'explicit_subst Grammar.Entry.e))],
        Gramext.action
          (fun (s : 'explicit_subst) (id : string)
             (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Ident (id, Some s)) : 'l2_pattern));
        [Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) (loc : Lexing.position * Lexing.position) ->
             (return_term loc (Ident (id, None)) : 'l2_pattern))];
       Some "100", None, []];
      Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", "");
         Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
        Gramext.action
          (fun (a : 'argument) _ (id : string) _
             (loc : Lexing.position * Lexing.position) ->
             (EtaArg (Some id, a) : 'argument));
        [Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("SYMBOL", ".");
         Gramext.Sself],
        Gramext.action
          (fun (a : 'argument) _ _
             (loc : Lexing.position * Lexing.position) ->
             (EtaArg (None, a) : 'argument));
        [Gramext.Stoken ("IDENT", "")],
        Gramext.action
          (fun (id : string) (loc : Lexing.position * Lexing.position) ->
             (IdentArg id : 'argument))]];
      Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("SYMBOL", "("); Gramext.Slist1 Gramext.Sself;
         Gramext.Stoken ("SYMBOL", ")")],
        Gramext.action
          (fun _ (terms : 'level3_term list) _
             (loc : Lexing.position * Lexing.position) ->
             (match terms with
                [] -> assert false
              | [term] -> term
              | terms -> ApplPattern terms :
              'level3_term));
        [Gramext.Snterm
           (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e))],
        Gramext.action
          (fun (a : 'argument) (loc : Lexing.position * Lexing.position) ->
             (ArgPattern a : 'level3_term));
        [Gramext.Stoken ("URI", "")],
        Gramext.action
          (fun (u : string) (loc : Lexing.position * Lexing.position) ->
             (UriPattern u : 'level3_term))]];
      Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("IDENT", "right");
         Gramext.Stoken ("IDENT", "associative")],
        Gramext.action
          (fun _ _ (loc : Lexing.position * Lexing.position) ->
             (`Right : 'associativity));
        [Gramext.Stoken ("IDENT", "left");
         Gramext.Stoken ("IDENT", "associative")],
        Gramext.action
          (fun _ _ (loc : Lexing.position * Lexing.position) ->
             (`Left : 'associativity))]];
      Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("IDENT", "at");
         Gramext.Stoken ("IDENT", "precedence");
         Gramext.Stoken ("NUMBER", "")],
        Gramext.action
          (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
             (n : 'precedence))]];
      Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None,
      [None, None,
       [[Gramext.Stoken ("IDENT", "notation");
         Gramext.Snterm
           (Grammar.Entry.obj
              (level1_pattern : 'level1_pattern Grammar.Entry.e));
         Gramext.Stoken ("IDENT", "for");
         Gramext.Snterm
           (Grammar.Entry.obj
              (level2_pattern : 'level2_pattern Grammar.Entry.e));
         Gramext.Sopt
           (Gramext.Snterm
              (Grammar.Entry.obj
                 (associativity : 'associativity Grammar.Entry.e)));
         Gramext.Sopt
           (Gramext.Snterm
              (Grammar.Entry.obj
                 (precedence : 'precedence Grammar.Entry.e)))],
        Gramext.action
          (fun (prec : 'precedence option) (assoc : 'associativity option)
             (p2 : 'level2_pattern) _ (p1 : 'level1_pattern) _
             (loc : Lexing.position * Lexing.position) ->
             (() : 'notation))]];
      Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
      None,
      [None, None,
       [[Gramext.Stoken ("IDENT", "interpretation");
         Gramext.Stoken ("SYMBOL", "");
         Gramext.Slist1
           (Gramext.Snterm
              (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e)));
         Gramext.Stoken ("IDENT", "as");
         Gramext.Snterm
           (Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e))],
        Gramext.action
          (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
             (loc : Lexing.position * Lexing.position) ->
             (() : 'interpretation))]]])

let exc_located_wrapper f =
  try f () with
    Stdpp.Exc_located (floc, Stream.Error msg) ->
      raise (Parse_error (floc, msg))
  | Stdpp.Exc_located (floc, exn) ->
      raise (Parse_error (floc, Printexc.to_string exn))

let parse_syntax_pattern stream =
  exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)

let parse_ast_pattern stream =
  exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)

let parse_interpretation stream =
  exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)

(** {2 Grammar extension} *)

type associativity_kind = [ `Left | `Right | `None ]

let symbol s = Gramext.Stoken ("SYMBOL", s)
let ident s = Gramext.Stoken ("IDENT", s)
let number s = Gramext.Stoken ("NUMBER", s)
let term = Gramext.Sself

type env_type = (string * (value_type * value)) list

let make_action action =
  let rec aux (vl : env_type) =
    prerr_endline "aux";
    function
      [] ->
        prerr_endline "make_action";
        Gramext.action (fun (loc : location) -> action vl loc)
    | None :: tl -> Gramext.action (fun _ -> aux vl tl)
    | Some (name, TermType) :: tl ->
        Gramext.action
          (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
    | Some (name, StringType) :: tl ->
        Gramext.action
          (fun (v : string) ->
             aux ((name, (StringType, StringValue v)) :: vl) tl)
    | Some (name, NumType) :: tl ->
        Gramext.action
          (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
    | Some (name, OptType t) :: tl ->
        Gramext.action
          (fun (v : 'a option) ->
             aux ((name, (OptType t, OptValue v)) :: vl) tl)
    | Some (name, ListType t) :: tl ->
        Gramext.action
          (fun (v : 'a list) ->
             aux ((name, (ListType t, ListValue v)) :: vl) tl)
  in
  aux []

let flatten_opt =
  let rec aux acc =
    function
      [] -> List.rev acc
    | None :: tl -> aux acc tl
    | Some hd :: tl -> aux (hd :: acc) tl
  in
  aux []

  (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
let extract_term_production pattern =
  let rec aux =
    function
      Literal l -> aux_literal l
    | Layout l -> aux_layout l
    | Magic m -> aux_magic m
    | Variable v -> aux_variable v
    | _ -> assert false
  and aux_literal =
    function
      `Symbol s -> [None, symbol s]
    | `Keyword s -> [None, ident s]
    | `Number s -> [None, number s]
  and aux_layout =
    function
      Sub (p1, p2) -> aux p1 @ [None, symbol "\\SUB"] @ aux p2
    | Sup (p1, p2) -> aux p1 @ [None, symbol "\\SUP"] @ aux p2
    | Below (p1, p2) -> aux p1 @ [None, symbol "\\BELOW"] @ aux p2
    | Above (p1, p2) -> aux p1 @ [None, symbol "\\ABOVE"] @ aux p2
    | Frac (p1, p2) -> aux p1 @ [None, symbol "\\FRAC"] @ aux p2
    | Atop (p1, p2) -> aux p1 @ [None, symbol "\\ATOP"] @ aux p2
    | Over (p1, p2) -> aux p1 @ [None, symbol "\\OVER"] @ aux p2
    | Root (p1, p2) ->
        [None, symbol "\\ROOT"] @ aux p2 @ [None, symbol "\\OF"] @ aux p1
    | Sqrt p -> [None, symbol "\\SQRT"] @ aux p
    | Break -> []
    | Box (_, pl) -> List.flatten (List.map aux pl)
  and aux_magic =
    function
      Opt p ->
        let (p_bindings, p_atoms) = List.split (aux p) in
        let p_names = flatten_opt p_bindings in
        [None,
         Gramext.srules
           [[Gramext.Sopt
               (Gramext.srules
                  [p_atoms,
                   make_action (fun (env : env_type) (loc : location) -> env)
                     p_bindings])],
            Gramext.action
              (fun (env_opt : env_type option) (loc : location) ->
                 match env_opt with
                   Some env ->
                     List.map
                       (fun (name, (typ, v)) ->
                          name, (OptType typ, OptValue (Some v)))
                       env
                 | None ->
                     List.map
                       (fun (name, typ) -> name, (OptType typ, OptValue None))
                       p_names)]]
    | _ -> assert false
  and aux_variable =
    function
      NumVar s -> [Some (s, NumType), number ""]
    | TermVar s -> [Some (s, TermType), term]
    | IdentVar s -> [Some (s, StringType), ident ""]
    | Ascription (p, s) -> assert false
    | FreshVar _ -> assert false
  in
  aux pattern

let level_of_int precedence =
  if precedence mod 10 <> 0 || precedence < 0 || precedence > 100 then
    raise (Level_not_found precedence);
  string_of_int precedence

type rule_id = Token.t Gramext.g_symbol list

let extend level1_pattern ?(precedence = 0) =
  fun ?associativity action ->
    let (p_bindings, p_atoms) =
      List.split (extract_term_production level1_pattern)
    in
    let level = level_of_int precedence in
    let p_names = flatten_opt p_bindings in
    let entry = Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e) in
    let _ =
      prerr_endline (string_of_int (List.length p_bindings));
      Grammar.extend
        [entry, Some (Gramext.Level level),
         [Some level, associativity,
          [p_atoms,
           make_action
             (fun (env : env_type) (loc : location) -> action env loc)
             p_bindings]]]
    in
    p_atoms

let delete atoms = Grammar.delete_rule l2_pattern atoms

let print_l2_pattern () =
  Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);
  Format.pp_print_flush Format.std_formatter ();
  flush stdout

(* vim:set encoding=utf8 foldmethod=marker: *)