X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.expanded.ml;h=9d0b579401d0f4ee11cfc1436db02fc88458ba09;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=5c73d2b4c4dec01a6808075289214cd6357d9834;hpb=915c3e1993cad4dcadefe7e6886e6cb8feefae8b;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
index 5c73d2b4c..9d0b57940 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
@@ -24,57 +24,57 @@
  *)
 
 oopen Printf
-oopen CicNotationEnvoopen CicNotationPt
+mmodule Ast = CicNotationPtmmodule Env = CicNotationEnv
 eexception Parse_error of Token.flocation * stringeexception Level_not_found of int
-llet grammar = Grammar.gcreate CicNotationLexer.notation_lexer
-llet min_precedence = 0llet max_precedence = 100llet default_precedence = 50
-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 phrase = Grammar.Entry.create grammar "phrase"
+llet level1_pattern_grammar =
+  Grammar.gcreate CicNotationLexer.level1_pattern_lexerllet level2_ast_grammar = Grammar.gcreate CicNotationLexer.level2_ast_lexerllet level2_meta_grammar = Grammar.gcreate CicNotationLexer.level2_meta_lexer
+llet min_precedence = 0llet max_precedence = 100
+llet level1_pattern =
+  Grammar.Entry.create level1_pattern_grammar "level1_pattern"llet level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"llet term = Grammar.Entry.create level2_ast_grammar "term"llet let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"llet level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
 llet return_term loc term = ()
-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)
 (** {2 Grammar extension} *)
 
-llet symbol s = Gramext.Stoken ("SYMBOL", s)llet ident s = Gramext.Stoken ("IDENT", s)llet number s = Gramext.Stoken ("NUMBER", s)llet term = Gramext.Sself
-llet g_symbol_of_literal =
+llet gram_symbol s = Gramext.Stoken ("SYMBOL", s)llet gram_ident s = Gramext.Stoken ("IDENT", s)llet gram_number s = Gramext.Stoken ("NUMBER", s)llet gram_keyword s = Gramext.Stoken ("", s)llet gram_term = Gramext.Sself
+llet gram_of_literal =
   function
-    `Symbol s -> symbol s
-  | `Keyword s -> ident s
-  | `Number s -> number s
+    `Symbol s -> gram_symbol s
+  | `Keyword s -> gram_keyword s
+  | `Number s -> gram_number s
 ttype binding =
     NoBinding
-  | Binding of string * value_type
-  | Env of (string * value_type) list
+  | Binding of string * Env.value_type
+  | Env of (string * Env.value_type) list
 llet make_action action bindings =
-  let rec aux (vl : env_type) =
+  let rec aux (vl : CicNotationEnv.t) =
     function
-      [] -> Gramext.action (fun (loc : location) -> action vl loc)
+      [] -> Gramext.action (fun (loc : Ast.location) -> action vl loc)
     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
-    | Binding (name, TermType) :: tl ->
+    | Binding (name, Env.TermType) :: tl ->
         Gramext.action
-          (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
-    | Binding (name, StringType) :: tl ->
+          (fun (v : Ast.term) ->
+             aux ((name, (Env.TermType, Env.TermValue v)) :: vl) tl)
+    | Binding (name, Env.StringType) :: tl ->
         Gramext.action
           (fun (v : string) ->
-             aux ((name, (StringType, StringValue v)) :: vl) tl)
-    | Binding (name, NumType) :: tl ->
+             aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
+    | Binding (name, Env.NumType) :: tl ->
         Gramext.action
-          (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
-    | Binding (name, OptType t) :: tl ->
+          (fun (v : string) ->
+             aux ((name, (Env.NumType, Env.NumValue v)) :: vl) tl)
+    | Binding (name, Env.OptType t) :: tl ->
         Gramext.action
           (fun (v : 'a option) ->
-             aux ((name, (OptType t, OptValue v)) :: vl) tl)
-    | Binding (name, ListType t) :: tl ->
+             aux ((name, (Env.OptType t, Env.OptValue v)) :: vl) tl)
+    | Binding (name, Env.ListType t) :: tl ->
         Gramext.action
           (fun (v : 'a list) ->
-             aux ((name, (ListType t, ListValue v)) :: vl) tl)
-    | Env _ :: tl -> Gramext.action (fun (v : env_type) -> aux (v @ vl) tl)
+             aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
+    | Env _ :: tl ->
+        Gramext.action (fun (v : CicNotationEnv.t) -> aux (v @ vl) tl)
   in
   aux [] (List.rev bindings)
 llet flatten_opt =
@@ -86,169 +86,191 @@ llet flatten_opt =
     | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
   in
   aux []
-
   (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
-let extract_term_production pattern =
+llet extract_term_production pattern =
   let rec aux =
     function
-      AttributedTerm (_, t) -> aux t
-    | Literal l -> aux_literal l
-    | Layout l -> aux_layout l
-    | Magic m -> aux_magic m
-    | Variable v -> aux_variable v
-    | t ->
-        prerr_endline (CicNotationPp.pp_term t);
-        assert false
+      Ast.AttributedTerm (_, t) -> aux t
+    | Ast.Literal l -> aux_literal l
+    | Ast.Layout l -> aux_layout l
+    | Ast.Magic m -> aux_magic m
+    | Ast.Variable v -> aux_variable v
+    | t -> prerr_endline (CicNotationPp.pp_term t); assert false
   and aux_literal =
     function
-      `Symbol s -> [NoBinding, symbol s]
-    | `Keyword s -> [NoBinding, ident s]
-    | `Number s -> [NoBinding, number s]
+      `Symbol s -> [NoBinding, gram_symbol s]
+    | `Keyword s -> [NoBinding, gram_keyword s]
+    | `Number s -> [NoBinding, gram_number s]
   and aux_layout =
     function
-      Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2
-    | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2
-    | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2
-    | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2
-    | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2
-    | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2
-    | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2
-    | Root (p1, p2) ->
-        [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"] @
-          aux p1
-    | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
-(*     | Break -> [] *)
-    | Box (_, pl) -> List.flatten (List.map aux pl)
+      Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2
+    | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2
+    | Ast.Below (p1, p2) ->
+        aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
+    | Ast.Above (p1, p2) ->
+        aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
+    | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
+    | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
+    | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
+    | Ast.Root (p1, p2) ->
+        [NoBinding, gram_symbol "\\root"] @ aux p2 @
+          [NoBinding, gram_symbol "\\of"] @ aux p1
+    | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
+    | Ast.Break -> []
+    | Ast.Box (_, pl) -> List.flatten (List.map aux pl)
+    | Ast.Group pl -> List.flatten (List.map aux pl)
   and aux_magic magic =
     match magic with
-      Opt p ->
+      Ast.Opt p ->
         let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
-        let action (env_opt : env_type option) (loc : location) =
+        let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) =
           match env_opt with
-            Some env -> List.map opt_binding_some env
-          | None -> List.map opt_binding_of_name p_names
+            Some env -> List.map Env.opt_binding_some env
+          | None -> List.map Env.opt_binding_of_name p_names
         in
-        [Env (List.map opt_declaration p_names),
+        [Env (List.map Env.opt_declaration p_names),
          Gramext.srules
            [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])],
             Gramext.action action]]
-    | List0 (p, _) | List1 (p, _) ->
+    | Ast.List0 (p, _) | Ast.List1 (p, _) ->
         let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
-        let env0 = List.map list_binding_of_name p_names in
-        let grow_env_entry env n v =
-          List.map
-            (function
-               n', (ty, ListValue vl) as entry ->
-                 if n' = n then n', (ty, ListValue (v :: vl)) else entry
-             | _ -> assert false)
-            env
-        in
-        let grow_env env_i env =
-          List.fold_left (fun env (n, (_, v)) -> grow_env_entry env n v) env
-            env_i
+        let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
+          CicNotationEnv.coalesce_env p_names env_list
         in
-        let action (env_list : env_type list) (loc : location) =
-          List.fold_right grow_env env_list env0
-        in
-        let g_symbol s =
+        let gram_of_list s =
           match magic with
-            List0 (_, None) -> Gramext.Slist0 s
-          | List1 (_, None) -> Gramext.Slist1 s
-          | List0 (_, Some l) -> Gramext.Slist0sep (s, g_symbol_of_literal l)
-          | List1 (_, Some l) -> Gramext.Slist1sep (s, g_symbol_of_literal l)
+            Ast.List0 (_, None) -> Gramext.Slist0 s
+          | Ast.List1 (_, None) -> Gramext.Slist1 s
+          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
           | _ -> assert false
         in
-        [Env (List.map list_declaration p_names),
+        [Env (List.map Env.list_declaration p_names),
          Gramext.srules
-           [[g_symbol (Gramext.srules [p_atoms, p_action])],
+           [[gram_of_list (Gramext.srules [p_atoms, p_action])],
             Gramext.action action]]
     | _ -> assert false
   and aux_variable =
     function
-      NumVar s -> [Binding (s, NumType), number ""]
-    | TermVar s -> [Binding (s, TermType), term]
-    | IdentVar s -> [Binding (s, StringType), ident ""]
-    | Ascription (p, s) -> assert false
-    | FreshVar _ -> assert false
+      Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
+    | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+    | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
+    | Ast.Ascription (p, s) -> assert false
+    | Ast.FreshVar _ -> assert false
   and inner_pattern p =
     let (p_bindings, p_atoms) = List.split (aux p) in
     let p_names = flatten_opt p_bindings in
     let action =
-      make_action
-        (fun (env : env_type) (loc : location) -> env)
+      make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env)
         p_bindings
     in
     p_bindings, p_atoms, p_names, action
   in
   aux pattern
 
-let level_of_int precedence =
+let level_of precedence associativity =
   if precedence < min_precedence || precedence > max_precedence then
     raise (Level_not_found precedence);
-  string_of_int precedence
+  let assoc_string =
+    match associativity with
+      Gramext.NonA -> "N"
+    | Gramext.LeftA -> "L"
+    | Gramext.RightA -> "R"
+  in
+  string_of_int precedence ^ assoc_string
 
 type rule_id = Token.t Gramext.g_symbol list
 
-let extend level1_pattern ?(precedence = default_precedence) =
-  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 _ =
-      Grammar.extend
-        [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e),
-         Some (Gramext.Level level),
-         [None, associativity,
-          [p_atoms,
-           make_action
-             (fun (env : env_type) (loc : location) -> action env loc)
-             p_bindings]]]
-    in
-    p_atoms
+  (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
+let owned_keywords = Hashtbl.create 23
+
+let extend level1_pattern ~precedence ~associativity action =
+  let (p_bindings, p_atoms) =
+    List.split (extract_term_production level1_pattern)
+  in
+  let level = level_of precedence associativity in
+  let p_names = flatten_opt p_bindings in
+  let _ =
+    Grammar.extend
+      [Grammar.Entry.obj (term : 'a Grammar.Entry.e),
+       Some (Gramext.Level level),
+       [None, Some associativity,
+        [p_atoms,
+         make_action
+           (fun (env : CicNotationEnv.t) (loc : Ast.location) ->
+              action env loc)
+           p_bindings]]]
+  in
+  let keywords = CicNotationUtil.keywords_of_term level1_pattern in
+  let rule_id = p_atoms in
+  List.iter CicNotationLexer.add_level2_ast_keyword keywords;
+  Hashtbl.add owned_keywords rule_id keywords;
+  rule_id
 
-let delete atoms = Grammar.delete_rule l2_pattern atoms
+let delete rule_id =
+  let atoms = rule_id in
+  begin try
+    let keywords = Hashtbl.find owned_keywords rule_id in
+    List.iter CicNotationLexer.remove_level2_ast_keyword keywords
+  with
+    Not_found -> assert false
+  end;
+  Grammar.delete_rule term atoms
 
 (** {2 Grammar} *)
 
-let boxify =
-  function
-    [a] -> a
-  | l -> Layout (Box (H, l))
+let parse_level1_pattern_ref = ref (fun _ -> assert false)
+let parse_level2_ast_ref = ref (fun _ -> assert false)
+let parse_level2_meta_ref = ref (fun _ -> assert false)
+
+let fold_cluster binder terms ty body =
+  List.fold_right (fun term body -> Ast.Binder (binder, (term, ty), body))
+    terms body  (* terms are names: either Ident or FreshVar *)
+
+let fold_exists terms ty body =
+  List.fold_right
+    (fun term body ->
+       let lambda = Ast.Binder (`Lambda, (term, ty), body) in
+       Ast.Appl [Ast.Symbol ("exists", 0); lambda])
+    terms body
 
 let fold_binder binder pt_names body =
-  let fold_cluster binder terms ty body =
-    List.fold_right (fun term body -> Binder (binder, (term, ty), body)) terms
-      body
-  in
   List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body)
     pt_names body
 
-let return_term loc term = AttributedTerm (`Loc loc, term)
+let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
 
+  (* create empty precedence level for "term" *)
 let _ =
+  let dummy_action =
+    Gramext.action
+      (fun _ -> failwith "internal error, lexer generated a dummy token")
+  in
+  let dummy_prod = [[Gramext.Stoken ("DUMMY", "")], dummy_action] in
   let mk_level_list first last =
     let rec aux acc =
       function
         i when i < first -> acc
-      | i -> aux ((Some (string_of_int i), None, []) :: acc) (i - 1)
+      | i ->
+          aux
+            ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod) ::
+               (Some (string_of_int i ^ "L"), Some Gramext.LeftA,
+                dummy_prod) ::
+               (Some (string_of_int i ^ "R"), Some Gramext.RightA,
+                dummy_prod) ::
+               acc)
+            (i - 1)
     in
     aux [] last
   in
   Grammar.extend
-    [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e), None,
+    [Grammar.Entry.obj (term : 'a Grammar.Entry.e), None,
      mk_level_list min_precedence max_precedence]
 
+(* {{{ Grammar for concrete syntax patterns, notation level 1 *)
 let _ =
   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)
-     and _ = (phrase : 'phrase Grammar.Entry.e) in
+    (let _ = (level1_pattern : 'level1_pattern Grammar.Entry.e) in
      let grammar_entry_create s =
        Grammar.Entry.create (Grammar.of_entry level1_pattern) s
      in
@@ -262,47 +284,17 @@ let _ =
        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 meta_substs : 'meta_substs Grammar.Entry.e =
-       grammar_entry_create "meta_substs"
-     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_name : 'bound_name Grammar.Entry.e =
-       grammar_entry_create "bound_name"
-     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_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
+           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
+         Gramext.Stoken ("EOI", "")],
         Gramext.action
-          (fun (p : 'l1_simple_pattern)
+          (fun _ (p : 'l1_pattern)
              (loc : Lexing.position * Lexing.position) ->
-             (p : 'level1_pattern))]];
+             (CicNotationUtil.boxify p : 'level1_pattern))]];
       Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
       [None, None,
        [[Gramext.Slist1
@@ -319,7 +311,7 @@ let _ =
         Gramext.action
           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
              (`Number n : 'literal));
-        [Gramext.Stoken ("KEYWORD", "")],
+        [Gramext.Stoken ("QKEYWORD", "")],
         Gramext.action
           (fun (k : string) (loc : Lexing.position * Lexing.position) ->
              (`Keyword k : 'literal));
@@ -329,7 +321,7 @@ let _ =
              (`Symbol s : 'literal))]];
       Grammar.Entry.obj (sep : 'sep Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Stoken ("SYMBOL", "\\SEP");
+       [[Gramext.Stoken ("", "sep");
          Gramext.Snterm
            (Grammar.Entry.obj (literal : 'literal Grammar.Entry.e))],
         Gramext.action
@@ -339,15 +331,15 @@ let _ =
         (l1_magic_pattern : 'l1_magic_pattern Grammar.Entry.e),
       None,
       [None, None,
-       [[Gramext.Stoken ("SYMBOL", "\\OPT");
+       [[Gramext.Stoken ("", "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");
+             (Ast.Opt p : 'l1_magic_pattern));
+        [Gramext.Stoken ("", "list1");
          Gramext.Snterm
            (Grammar.Entry.obj
               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
@@ -356,8 +348,8 @@ let _ =
         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");
+             (Ast.List1 (p, sep) : 'l1_magic_pattern));
+        [Gramext.Stoken ("", "list0");
          Gramext.Snterm
            (Grammar.Entry.obj
               (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e));
@@ -366,153 +358,319 @@ let _ =
         Gramext.action
           (fun (sep : 'sep option) (p : 'l1_simple_pattern) _
              (loc : Lexing.position * Lexing.position) ->
-             (List0 (p, sep) : 'l1_magic_pattern))]];
+             (Ast.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.Stoken ("", "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", "")],
+             (Ast.IdentVar id : 'l1_pattern_variable));
+        [Gramext.Stoken ("", "number"); 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", "")],
+             (Ast.NumVar id : 'l1_pattern_variable));
+        [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
         Gramext.action
           (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
-             (TermVar id : 'l1_pattern_variable))]];
+             (Ast.TermVar id : 'l1_pattern_variable))]];
       Grammar.Entry.obj
         (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e),
       None,
       [Some "layout", Some Gramext.LeftA,
-       [[Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\AS");
-         Gramext.Stoken ("IDENT", "")],
+       [[Gramext.Stoken ("LPAREN", "");
+         Gramext.Snterm
+           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
-          (fun (id : string) _ (p : 'l1_simple_pattern)
+          (fun _ (p : 'l1_pattern) _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Variable (Ascription (p, id))) :
+             (return_term loc (CicNotationUtil.group p) :
               'l1_simple_pattern));
-        [Gramext.Stoken ("DELIM", "\\[");
+        [Gramext.Stoken ("", "break")],
+        Gramext.action
+          (fun _ (loc : Lexing.position * Lexing.position) ->
+             (return_term loc (Ast.Layout Ast.Break) : 'l1_simple_pattern));
+        [Gramext.Stoken ("", "hovbox"); Gramext.Stoken ("LPAREN", "");
          Gramext.Snterm
            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
-         Gramext.Stoken ("DELIM", "\\]")],
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
-          (fun _ (p : 'l1_pattern) _
+          (fun _ (p : 'l1_pattern) _ _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (boxify p) : 'l1_simple_pattern));
-        [Gramext.Stoken ("SYMBOL", "\\BREAK")],
+             (return_term loc
+                (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p))) :
+              'l1_simple_pattern));
+        [Gramext.Stoken ("", "hvbox"); Gramext.Stoken ("LPAREN", "");
+         Gramext.Snterm
+           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
-          (fun _ (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout Break) : 'l1_simple_pattern));
-        [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("DELIM", "\\[");
+          (fun _ (p : 'l1_pattern) _ _
+             (loc : Lexing.position * Lexing.position) ->
+             (return_term loc
+                (Ast.Layout (Ast.Box ((Ast.HV, false, false), p))) :
+              'l1_simple_pattern));
+        [Gramext.Stoken ("", "vbox"); Gramext.Stoken ("LPAREN", "");
          Gramext.Snterm
            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
-         Gramext.Stoken ("DELIM", "\\]")],
+         Gramext.Stoken ("RPAREN", "")],
         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 ("DELIM", "\\[");
+             (return_term loc
+                (Ast.Layout (Ast.Box ((Ast.V, false, false), p))) :
+              'l1_simple_pattern));
+        [Gramext.Stoken ("", "hbox"); Gramext.Stoken ("LPAREN", "");
          Gramext.Snterm
            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
-         Gramext.Stoken ("DELIM", "\\]")],
+         Gramext.Stoken ("RPAREN", "")],
         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.Sself;
-         Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself],
+             (return_term loc
+                (Ast.Layout (Ast.Box ((Ast.H, false, false), p))) :
+              'l1_simple_pattern));
+        [Gramext.Stoken ("SYMBOL", "\\root"); Gramext.Sself;
+         Gramext.Stoken ("SYMBOL", "\\of"); Gramext.Sself],
         Gramext.action
           (fun (arg : 'l1_simple_pattern) _ (index : 'l1_simple_pattern) _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout (Root (arg, index))) :
+             (return_term loc (Ast.Layout (Ast.Root (arg, index))) :
               'l1_simple_pattern));
-        [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
+        [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],
+             (return_term loc (Ast.Layout (Ast.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.Sself; Gramext.Stoken ("SYMBOL", "\\ATOP"); Gramext.Sself],
+             (return_term loc (Ast.Layout (Ast.Frac (p1, p2))) :
+              'l1_simple_pattern));
+        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\atop"); Gramext.Sself],
         Gramext.action
           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout (Atop (p1, p2))) : 'l1_simple_pattern));
-        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\OVER"); Gramext.Sself],
+             (return_term loc (Ast.Layout (Ast.Atop (p1, p2))) :
+              'l1_simple_pattern));
+        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\over"); Gramext.Sself],
         Gramext.action
           (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout (Over (p1, p2))) : 'l1_simple_pattern));
-        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\ABOVE"); Gramext.Sself],
+             (return_term loc (Ast.Layout (Ast.Over (p1, 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))) :
+             (return_term loc (Ast.Layout (Ast.Above (p1, p2))) :
               'l1_simple_pattern));
-        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\BELOW"); Gramext.Sself],
+        [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))) :
+             (return_term loc (Ast.Layout (Ast.Below (p1, p2))) :
               'l1_simple_pattern));
-        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\SUP"); Gramext.Sself],
+        [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],
+             (return_term loc (Ast.Layout (Ast.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))];
+             (return_term loc (Ast.Layout (Ast.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));
+             (return_term loc (Ast.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));
+             (return_term loc (Ast.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));
+             (return_term loc (Ast.Magic m) : 'l1_simple_pattern));
         [Gramext.Stoken ("IDENT", "")],
         Gramext.action
           (fun (i : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Ident (i, None)) : 'l1_simple_pattern))]];
-      Grammar.Entry.obj (level2_pattern : 'level2_pattern Grammar.Entry.e),
-      None,
+             (return_term loc (Ast.Variable (Ast.TermVar i)) :
+              'l1_simple_pattern))]]])
+(* }}} *)
+
+(* {{{ Grammar for ast magics, notation level 2 *)
+let _ =
+  Grammar.extend
+    (let _ = (level2_meta : 'level2_meta Grammar.Entry.e) in
+     let grammar_entry_create s =
+       Grammar.Entry.create (Grammar.of_entry level2_meta) s
+     in
+     let l2_variable : 'l2_variable Grammar.Entry.e =
+       grammar_entry_create "l2_variable"
+     and l2_magic : 'l2_magic Grammar.Entry.e =
+       grammar_entry_create "l2_magic"
+     in
+     [Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Snterm
-           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+       [[Gramext.Stoken ("IDENT", "")],
         Gramext.action
-          (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
-             (p : 'level2_pattern))]];
+          (fun (id : string) (loc : Lexing.position * Lexing.position) ->
+             (Ast.TermVar id : 'l2_variable));
+        [Gramext.Stoken ("", "anonymous")],
+        Gramext.action
+          (fun _ (loc : Lexing.position * Lexing.position) ->
+             (Ast.TermVar "_" : 'l2_variable));
+        [Gramext.Stoken ("", "fresh"); Gramext.Stoken ("IDENT", "")],
+        Gramext.action
+          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+             (Ast.FreshVar id : 'l2_variable));
+        [Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
+        Gramext.action
+          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+             (Ast.IdentVar id : 'l2_variable));
+        [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
+        Gramext.action
+          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+             (Ast.NumVar id : 'l2_variable));
+        [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
+        Gramext.action
+          (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+             (Ast.TermVar id : 'l2_variable))]];
+      Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e), None,
+      [None, None,
+       [[Gramext.Stoken ("", "fail")],
+        Gramext.action
+          (fun _ (loc : Lexing.position * Lexing.position) ->
+             (Ast.Fail : 'l2_magic));
+        [Gramext.Stoken ("", "if");
+         Gramext.Snterm
+           (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+         Gramext.Stoken ("", "then");
+         Gramext.Snterm
+           (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+         Gramext.Stoken ("", "else");
+         Gramext.Snterm
+           (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
+        Gramext.action
+          (fun (p_false : 'level2_meta) _ (p_true : 'level2_meta) _
+             (p_test : 'level2_meta) _
+             (loc : Lexing.position * Lexing.position) ->
+             (Ast.If (p_test, p_true, p_false) : 'l2_magic));
+        [Gramext.Stoken ("", "default");
+         Gramext.Snterm
+           (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+         Gramext.Snterm
+           (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
+        Gramext.action
+          (fun (none : 'level2_meta) (some : 'level2_meta) _
+             (loc : Lexing.position * Lexing.position) ->
+             (Ast.Default (some, none) : 'l2_magic));
+        [Gramext.Stoken ("", "fold");
+         Gramext.srules
+           [[Gramext.Stoken ("", "right")],
+            Gramext.action
+              (fun _ (loc : Lexing.position * Lexing.position) ->
+                 (`Right : 'e__1));
+            [Gramext.Stoken ("", "left")],
+            Gramext.action
+              (fun _ (loc : Lexing.position * Lexing.position) ->
+                 (`Left : 'e__1))];
+         Gramext.Snterm
+           (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+         Gramext.Stoken ("", "rec"); Gramext.Stoken ("IDENT", "");
+         Gramext.Snterm
+           (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
+        Gramext.action
+          (fun (recursive : 'level2_meta) (id : string) _
+             (base : 'level2_meta) (kind : 'e__1) _
+             (loc : Lexing.position * Lexing.position) ->
+             (Ast.Fold (kind, base, [id], recursive) : 'l2_magic))]];
+      Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e), None,
+      [None, None,
+       [[Gramext.Stoken ("UNPARSED_AST", "")],
+        Gramext.action
+          (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
+             (!parse_level2_ast_ref (Ulexing.from_utf8_string blob) :
+              'level2_meta));
+        [Gramext.Snterm
+           (Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e))],
+        Gramext.action
+          (fun (var : 'l2_variable)
+             (loc : Lexing.position * Lexing.position) ->
+             (Ast.Variable var : 'level2_meta));
+        [Gramext.Snterm
+           (Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e))],
+        Gramext.action
+          (fun (magic : 'l2_magic)
+             (loc : Lexing.position * Lexing.position) ->
+             (Ast.Magic magic : 'level2_meta))]]])
+(* }}} *)
+
+(* {{{ Grammar for ast patterns, notation level 2 *)
+let _ =
+  Grammar.extend
+    (let _ = (level2_ast : 'level2_ast Grammar.Entry.e)
+     and _ = (term : 'term Grammar.Entry.e)
+     and _ = (let_defs : 'let_defs Grammar.Entry.e) in
+     let grammar_entry_create s =
+       Grammar.Entry.create (Grammar.of_entry level2_ast) s
+     in
+     let 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 meta_substs : 'meta_substs Grammar.Entry.e =
+       grammar_entry_create "meta_substs"
+     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 arg : 'arg Grammar.Entry.e = grammar_entry_create "arg"
+     and single_arg : 'single_arg Grammar.Entry.e =
+       grammar_entry_create "single_arg"
+     and induction_kind : 'induction_kind Grammar.Entry.e =
+       grammar_entry_create "induction_kind"
+     and binder_vars : 'binder_vars Grammar.Entry.e =
+       grammar_entry_create "binder_vars"
+     in
+     [Grammar.Entry.obj (level2_ast : 'level2_ast Grammar.Entry.e), None,
+      [None, None,
+       [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
+        Gramext.action
+          (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
+             (p : 'level2_ast))]];
       Grammar.Entry.obj (sort : 'sort Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Stoken ("SYMBOL", "\\TYPE")],
+       [[Gramext.Stoken ("", "CProp")],
+        Gramext.action
+          (fun _ (loc : Lexing.position * Lexing.position) ->
+             (`CProp : 'sort));
+        [Gramext.Stoken ("", "Type")],
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
              (`Type : 'sort));
-        [Gramext.Stoken ("SYMBOL", "\\SET")],
+        [Gramext.Stoken ("", "Set")],
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) -> (`Set : 'sort));
-        [Gramext.Stoken ("SYMBOL", "\\PROP")],
+        [Gramext.Stoken ("", "Prop")],
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
              (`Prop : 'sort))]];
@@ -525,24 +683,22 @@ let _ =
               [[Gramext.Stoken ("IDENT", "");
                 Gramext.Stoken ("SYMBOL", "≔");
                 Gramext.Snterm
-                  (Grammar.Entry.obj
-                     (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+                  (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
                Gramext.action
-                 (fun (t : 'l2_pattern) _ (i : string)
+                 (fun (t : 'term) _ (i : string)
                     (loc : Lexing.position * Lexing.position) ->
-                    (i, t : 'e__1))],
+                    (i, t : 'e__2))],
             Gramext.Stoken ("SYMBOL", ";"));
          Gramext.Stoken ("SYMBOL", "]")],
         Gramext.action
-          (fun _ (substs : 'e__1 list) _ _
+          (fun _ (substs : 'e__2 list) _ _
              (loc : Lexing.position * Lexing.position) ->
              (substs : 'explicit_subst))]];
       Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Snterm
-           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+       [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
         Gramext.action
-          (fun (p : 'l2_pattern) (loc : Lexing.position * Lexing.position) ->
+          (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
              (Some p : 'meta_subst));
         [Gramext.Stoken ("SYMBOL", "_")],
         Gramext.action
@@ -564,39 +720,39 @@ let _ =
       None,
       [None, None,
        [[Gramext.Snterm
-           (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e))],
+           (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e))],
         Gramext.action
-          (fun (id : 'bound_name) (loc : Lexing.position * Lexing.position) ->
-             (id, None : 'possibly_typed_name));
-        [Gramext.Stoken ("SYMBOL", "(");
+          (fun (arg : 'single_arg)
+             (loc : Lexing.position * Lexing.position) ->
+             (arg, None : 'possibly_typed_name));
+        [Gramext.Stoken ("LPAREN", "");
          Gramext.Snterm
-           (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e));
+           (Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e));
          Gramext.Stoken ("SYMBOL", ":");
-         Gramext.Snterm
-           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
-         Gramext.Stoken ("SYMBOL", ")")],
+         Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
-          (fun _ (typ : 'l2_pattern) _ (id : 'bound_name) _
+          (fun _ (typ : 'term) _ (id : 'single_arg) _
              (loc : Lexing.position * Lexing.position) ->
              (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.Stoken ("LPAREN", ""); Gramext.Stoken ("IDENT", "");
          Gramext.Slist1
            (Gramext.Snterm
               (Grammar.Entry.obj
                  (possibly_typed_name :
                   'possibly_typed_name Grammar.Entry.e)));
-         Gramext.Stoken ("SYMBOL", ")")],
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
           (fun _ (vars : 'possibly_typed_name list) (id : string) _
              (loc : Lexing.position * Lexing.position) ->
-             (id, vars : 'match_pattern));
+             (id, None, vars : 'match_pattern));
         [Gramext.Stoken ("IDENT", "")],
         Gramext.action
           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
-             (id, [] : 'match_pattern))]];
+             (id, None, [] : 'match_pattern))]];
       Grammar.Entry.obj (binder : 'binder Grammar.Entry.e), None,
       [None, None,
        [[Gramext.Stoken ("SYMBOL", "λ")],
@@ -607,79 +763,66 @@ let _ =
         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_name : 'bound_name Grammar.Entry.e), None,
+      Grammar.Entry.obj (arg : 'arg Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
+       [[Gramext.Stoken ("UNPARSED_META", "")],
         Gramext.action
-          (fun (i : string) _ (loc : Lexing.position * Lexing.position) ->
-             (Variable (FreshVar i) : 'bound_name));
+          (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
+             (let meta =
+                !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
+              in
+              match meta with
+                Ast.Variable (Ast.FreshVar _) -> [meta], None
+              | Ast.Variable (Ast.TermVar "_") ->
+                  [Ast.Ident ("_", None)], None
+              | _ -> failwith "Invalid bound name." :
+              'arg));
         [Gramext.Stoken ("IDENT", "")],
         Gramext.action
-          (fun (i : string) (loc : Lexing.position * Lexing.position) ->
-             (Ident (i, None) : 'bound_name))]];
-      Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e), None,
-      [None, None,
-       [[Gramext.Slist1
-           (Gramext.srules
-              [[Gramext.Stoken ("SYMBOL", "(");
-                Gramext.Slist1sep
-                  (Gramext.Snterm
-                     (Grammar.Entry.obj
-                        (bound_name : 'bound_name Grammar.Entry.e)),
-                   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__3))]);
-                Gramext.Stoken ("SYMBOL", ")")],
-               Gramext.action
-                 (fun _ (ty : 'e__3 option) (vars : 'bound_name list) _
-                    (loc : Lexing.position * Lexing.position) ->
-                    (vars, ty : 'e__4))])],
+          (fun (name : string) (loc : Lexing.position * Lexing.position) ->
+             ([Ast.Ident (name, None)], None : 'arg));
+        [Gramext.Stoken ("LPAREN", "");
+         Gramext.Slist1sep
+           (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
+         Gramext.Stoken ("SYMBOL", ":");
+         Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
-          (fun (clusters : 'e__4 list)
+          (fun _ (ty : 'term) _ (names : string list) _
              (loc : Lexing.position * Lexing.position) ->
-             (clusters : 'bound_names));
-        [Gramext.Slist1sep
-           (Gramext.Snterm
-              (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e)),
-            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))])],
+             (List.map (fun n -> Ast.Ident (n, None)) names, Some ty :
+              'arg))]];
+      Grammar.Entry.obj (single_arg : 'single_arg Grammar.Entry.e), None,
+      [None, None,
+       [[Gramext.Stoken ("UNPARSED_META", "")],
         Gramext.action
-          (fun (ty : 'e__2 option) (vars : 'bound_name list)
-             (loc : Lexing.position * Lexing.position) ->
-             ([vars, ty] : 'bound_names))]];
+          (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
+             (let meta =
+                !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
+              in
+              match meta with
+                Ast.Variable (Ast.FreshVar _) |
+                Ast.Variable (Ast.IdentVar _) ->
+                  meta
+              | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
+              | _ -> failwith "Invalid index name." :
+              'single_arg));
+        [Gramext.Stoken ("IDENT", "")],
+        Gramext.action
+          (fun (name : string) (loc : Lexing.position * Lexing.position) ->
+             (Ast.Ident (name, None) : 'single_arg))]];
       Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
       None,
       [None, None,
-       [[Gramext.Stoken ("IDENT", "corec")],
+       [[Gramext.Stoken ("", "corec")],
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
              (`CoInductive : 'induction_kind));
-        [Gramext.Stoken ("IDENT", "rec")],
+        [Gramext.Stoken ("", "rec")],
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
              (`Inductive : 'induction_kind))]];
@@ -689,38 +832,36 @@ let _ =
            (Gramext.srules
               [[Gramext.Snterm
                   (Grammar.Entry.obj
-                     (bound_name : 'bound_name Grammar.Entry.e));
-                Gramext.Snterm
-                  (Grammar.Entry.obj
-                     (bound_names : 'bound_names Grammar.Entry.e));
+                     (single_arg : 'single_arg Grammar.Entry.e));
+                Gramext.Slist1
+                  (Gramext.Snterm
+                     (Grammar.Entry.obj (arg : 'arg Grammar.Entry.e)));
                 Gramext.Sopt
                   (Gramext.srules
-                     [[Gramext.Stoken ("IDENT", "on");
+                     [[Gramext.Stoken ("", "on");
                        Gramext.Snterm
                          (Grammar.Entry.obj
-                            (bound_name : 'bound_name Grammar.Entry.e))],
+                            (single_arg : 'single_arg Grammar.Entry.e))],
                       Gramext.action
-                        (fun (id : 'bound_name) _
+                        (fun (id : 'single_arg) _
                            (loc : Lexing.position * Lexing.position) ->
-                           (id : 'e__5))]);
+                           (id : 'e__3))]);
                 Gramext.Sopt
                   (Gramext.srules
                      [[Gramext.Stoken ("SYMBOL", ":");
                        Gramext.Snterm
-                         (Grammar.Entry.obj
-                            (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+                         (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
                       Gramext.action
-                        (fun (p : 'l2_pattern) _
+                        (fun (p : 'term) _
                            (loc : Lexing.position * Lexing.position) ->
-                           (p : 'e__6))]);
+                           (p : 'e__4))]);
                 Gramext.Stoken ("SYMBOL", "≝");
                 Gramext.Snterm
-                  (Grammar.Entry.obj
-                     (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+                  (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
                Gramext.action
-                 (fun (body : 'l2_pattern) _ (ty : 'e__6 option)
-                    (index_name : 'e__5 option) (args : 'bound_names)
-                    (name : 'bound_name)
+                 (fun (body : 'term) _ (ty : 'e__4 option)
+                    (index_name : 'e__3 option) (args : 'arg list)
+                    (name : 'single_arg)
                     (loc : Lexing.position * Lexing.position) ->
                     (let body = fold_binder `Lambda args body in
                      let ty =
@@ -737,7 +878,7 @@ let _ =
                      let rec find_arg name n =
                        function
                          [] ->
-                           fail loc
+                           Ast.fail loc
                              (sprintf "Argument %s not found"
                                 (CicNotationPp.pp_term name))
                        | (l, _) :: tl ->
@@ -748,174 +889,172 @@ let _ =
                      let index =
                        match index_name with
                          None -> 0
-                       | Some name -> find_arg name 0 args
+                       | Some index_name -> find_arg index_name 0 args
                      in
                      (name, ty), body, index :
-                     'e__7))],
-            Gramext.Stoken ("IDENT", "and"))],
+                     'e__5))],
+            Gramext.Stoken ("", "and"))],
         Gramext.action
-          (fun (defs : 'e__7 list)
+          (fun (defs : 'e__5 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,
+      Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Stoken ("SYMBOL", "\\DEFAULT");
-         Gramext.Stoken ("DELIM", "\\[");
-         Gramext.Snterm
-           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
-         Gramext.Stoken ("DELIM", "\\]"); Gramext.Stoken ("DELIM", "\\[");
-         Gramext.Snterm
-           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
-         Gramext.Stoken ("DELIM", "\\]")],
-        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.Stoken ("LPAREN", "");
          Gramext.srules
-           [[Gramext.Stoken ("IDENT", "right")],
+           [[Gramext.Stoken ("SYMBOL", "_")],
             Gramext.action
               (fun _ (loc : Lexing.position * Lexing.position) ->
-                 (`Right : 'e__8));
-            [Gramext.Stoken ("IDENT", "left")],
+                 ([Ast.Ident ("_", None)] : 'e__8));
+            [Gramext.Slist1sep
+               (Gramext.Snterm
+                  (Grammar.Entry.obj
+                     (single_arg : 'single_arg Grammar.Entry.e)),
+                Gramext.Stoken ("SYMBOL", ","))],
+            Gramext.action
+              (fun (l : 'single_arg list)
+                 (loc : Lexing.position * Lexing.position) ->
+                 (l : 'e__8))];
+         Gramext.Sopt
+           (Gramext.srules
+              [[Gramext.Stoken ("SYMBOL", ":");
+                Gramext.Snterm
+                  (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
+               Gramext.action
+                 (fun (t : 'term) _
+                    (loc : Lexing.position * Lexing.position) ->
+                    (t : 'e__9))]);
+         Gramext.Stoken ("RPAREN", "")],
+        Gramext.action
+          (fun _ (typ : 'e__9 option) (vars : 'e__8) _
+             (loc : Lexing.position * Lexing.position) ->
+             (vars, typ : 'binder_vars));
+        [Gramext.srules
+           [[Gramext.Stoken ("SYMBOL", "_")],
             Gramext.action
               (fun _ (loc : Lexing.position * Lexing.position) ->
-                 (`Left : 'e__8))];
-         Gramext.Stoken ("DELIM", "\\[");
-         Gramext.Snterm
-           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
-         Gramext.Stoken ("DELIM", "\\]");
-         Gramext.Stoken ("SYMBOL", "\\LAMBDA"); Gramext.Stoken ("IDENT", "");
-         Gramext.Stoken ("DELIM", "\\[");
-         Gramext.Snterm
-           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
-         Gramext.Stoken ("DELIM", "\\]")],
+                 ([Ast.Ident ("_", None)] : 'e__6));
+            [Gramext.Slist1sep
+               (Gramext.Snterm
+                  (Grammar.Entry.obj
+                     (single_arg : 'single_arg Grammar.Entry.e)),
+                Gramext.Stoken ("SYMBOL", ","))],
+            Gramext.action
+              (fun (l : 'single_arg list)
+                 (loc : Lexing.position * Lexing.position) ->
+                 (l : 'e__6))];
+         Gramext.Sopt
+           (Gramext.srules
+              [[Gramext.Stoken ("SYMBOL", ":");
+                Gramext.Snterm
+                  (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
+               Gramext.action
+                 (fun (t : 'term) _
+                    (loc : Lexing.position * Lexing.position) ->
+                    (t : 'e__7))])],
         Gramext.action
-          (fun _ (recursive : 'l2_pattern) _ (id : string) _ _
-             (base : 'l2_pattern) _ (kind : 'e__8) _
+          (fun (typ : 'e__7 option) (vars : 'e__6)
              (loc : Lexing.position * Lexing.position) ->
-             (Fold (kind, base, [id], recursive) : 'l2_magic_pattern))]];
-      Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
-      Some (Gramext.Level "10"),
-      [Some "10", Some Gramext.NonA,
-       [[Gramext.Stoken ("IDENT", "let");
+             (vars, typ : 'binder_vars))]];
+      Grammar.Entry.obj (term : 'term Grammar.Entry.e),
+      Some (Gramext.Level "10N"),
+      [None, None,
+       [[Gramext.Stoken ("", "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.Stoken ("", "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");
+          (fun (body : 'term) _ (defs : 'let_defs) (k : 'induction_kind) _
+             (loc : Lexing.position * Lexing.position) ->
+             (return_term loc (Ast.LetRec (k, defs, body)) : 'term));
+        [Gramext.Stoken ("", "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) _
+          (fun (p2 : 'term) _ (p1 : 'term) _ (var : 'possibly_typed_name) _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (LetIn (var, p1, p2)) : 'l2_pattern))]];
-      Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
-      Some (Gramext.Level "20"),
-      [Some "20", Some Gramext.RightA,
-       [[Gramext.Snterm
+             (return_term loc (Ast.LetIn (var, p1, p2)) : 'term))]];
+      Grammar.Entry.obj (term : 'term Grammar.Entry.e),
+      Some (Gramext.Level "20R"),
+      [None, None,
+       [[Gramext.Stoken ("SYMBOL", "∃");
+         Gramext.Snterm
+           (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
+         Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
+        Gramext.action
+          (fun (body : 'term) _ (vars, typ : 'binder_vars) _
+             (loc : Lexing.position * Lexing.position) ->
+             (return_term loc (fold_exists vars typ body) : 'term));
+        [Gramext.Snterm
            (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
          Gramext.Snterm
-           (Grammar.Entry.obj (bound_names : 'bound_names Grammar.Entry.e));
+           (Grammar.Entry.obj (binder_vars : 'binder_vars Grammar.Entry.e));
          Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
         Gramext.action
-          (fun (body : 'l2_pattern) _ (names : 'bound_names) (b : 'binder)
+          (fun (body : 'term) _ (vars, typ : 'binder_vars) (b : 'binder)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (fold_binder b names body) : 'l2_pattern))]];
-      Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
-      Some (Gramext.Level "70"),
-      [Some "70", Some Gramext.LeftA,
+             (return_term loc (fold_cluster b vars typ body) : 'term))]];
+      Grammar.Entry.obj (term : 'term Grammar.Entry.e),
+      Some (Gramext.Level "70L"),
+      [None, None,
        [[Gramext.Sself; Gramext.Sself],
         Gramext.action
-          (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
+          (fun (p2 : 'term) (p1 : 'term)
              (loc : Lexing.position * Lexing.position) ->
              (let rec aux =
                 function
-                  Appl (hd :: tl) | AttributedTerm (_, Appl (hd :: tl)) ->
+                  Ast.Appl (hd :: tl) |
+                  Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
                     aux hd @ tl
                 | term -> [term]
               in
-              return_term loc (Appl (aux p1 @ [p2])) :
-              'l2_pattern))]];
-      Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
-      Some (Gramext.Level "90"),
-      [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))],
+              return_term loc (Ast.Appl (aux p1 @ [p2])) :
+              'term))]];
+      Grammar.Entry.obj (term : 'term Grammar.Entry.e),
+      Some (Gramext.Level "90N"),
+      [None, None,
+       [[Gramext.Stoken ("UNPARSED_META", "")],
         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", ")")],
+          (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
+             (!parse_level2_meta_ref (Ulexing.from_utf8_string blob) :
+              'term));
+        [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
-          (fun _ (p : 'l2_pattern) _
-             (loc : Lexing.position * Lexing.position) ->
-             (p : 'l2_pattern));
-        [Gramext.Stoken ("SYMBOL", "("); Gramext.Sself;
+          (fun _ (p : 'term) _ (loc : Lexing.position * Lexing.position) ->
+             (p : 'term));
+        [Gramext.Stoken ("LPAREN", ""); Gramext.Sself;
          Gramext.Stoken ("SYMBOL", ":"); Gramext.Sself;
-         Gramext.Stoken ("SYMBOL", ")")],
+         Gramext.Stoken ("RPAREN", "")],
         Gramext.action
-          (fun _ (p2 : 'l2_pattern) _ (p1 : 'l2_pattern) _
+          (fun _ (p2 : 'term) _ (p1 : 'term) _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Appl [Symbol ("cast", 0); p1; p2]) :
-              'l2_pattern));
+             (return_term loc (Ast.Cast (p1, p2)) : 'term));
         [Gramext.Sopt
            (Gramext.srules
               [[Gramext.Stoken ("SYMBOL", "[");
                 Gramext.Snterm
-                  (Grammar.Entry.obj
-                     (l2_pattern : 'l2_pattern Grammar.Entry.e));
+                  (Grammar.Entry.obj (term : 'term Grammar.Entry.e));
                 Gramext.Stoken ("SYMBOL", "]")],
                Gramext.action
-                 (fun _ (ty : 'l2_pattern) _
+                 (fun _ (ty : 'term) _
                     (loc : Lexing.position * Lexing.position) ->
-                    (ty : 'e__9))]);
-         Gramext.Stoken ("IDENT", "match"); Gramext.Sself;
+                    (ty : 'e__10))]);
+         Gramext.Stoken ("", "match"); Gramext.Sself;
          Gramext.Sopt
            (Gramext.srules
-              [[Gramext.Stoken ("SYMBOL", ":"); Gramext.Stoken ("IDENT", "")],
+              [[Gramext.Stoken ("", "in"); Gramext.Stoken ("IDENT", "")],
                Gramext.action
                  (fun (id : string) _
                     (loc : Lexing.position * Lexing.position) ->
-                    (id : 'e__10))]);
-         Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
+                    (id, None : 'e__11))]);
+         Gramext.Stoken ("", "with"); Gramext.Stoken ("SYMBOL", "[");
          Gramext.Slist0sep
            (Gramext.srules
               [[Gramext.Snterm
@@ -923,47 +1062,54 @@ let _ =
                      (match_pattern : 'match_pattern Grammar.Entry.e));
                 Gramext.Stoken ("SYMBOL", "⇒");
                 Gramext.Snterm
-                  (Grammar.Entry.obj
-                     (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+                  (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
                Gramext.action
-                 (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern)
+                 (fun (rhs : 'term) _ (lhs : 'match_pattern)
                     (loc : Lexing.position * Lexing.position) ->
-                    (lhs, rhs : 'e__11))],
+                    (lhs, rhs : 'e__12))],
             Gramext.Stoken ("SYMBOL", "|"));
          Gramext.Stoken ("SYMBOL", "]")],
         Gramext.action
-          (fun _ (patterns : 'e__11 list) _ _ (indty_ident : 'e__10 option)
-             (t : 'l2_pattern) _ (outtyp : 'e__9 option)
+          (fun _ (patterns : 'e__12 list) _ _ (indty_ident : 'e__11 option)
+             (t : 'term) _ (outtyp : 'e__10 option)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Case (t, indty_ident, outtyp, patterns)) :
-              'l2_pattern));
+             (return_term loc (Ast.Case (t, indty_ident, outtyp, patterns)) :
+              'term));
         [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));
+             (return_term loc (Ast.Sort s) : 'term));
         [Gramext.Stoken ("META", "");
          Gramext.Snterm
            (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
         Gramext.action
           (fun (s : 'meta_substs) (m : string)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Meta (int_of_string m, s)) : 'l2_pattern));
+             (return_term loc (Ast.Meta (int_of_string m, s)) : 'term));
         [Gramext.Stoken ("META", "")],
         Gramext.action
           (fun (m : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Meta (int_of_string m, [])) : 'l2_pattern));
+             (return_term loc (Ast.Meta (int_of_string m, [])) : 'term));
+        [Gramext.Stoken ("PLACEHOLDER", "")],
+        Gramext.action
+          (fun _ (loc : Lexing.position * Lexing.position) ->
+             (return_term loc Ast.UserInput : 'term));
         [Gramext.Stoken ("IMPLICIT", "")],
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
-             (return_term loc Implicit : 'l2_pattern));
+             (return_term loc Ast.Implicit : 'term));
         [Gramext.Stoken ("NUMBER", "")],
         Gramext.action
           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Num (n, 0)) : 'l2_pattern));
+             (return_term loc (Ast.Num (n, 0)) : 'term));
         [Gramext.Stoken ("URI", "")],
         Gramext.action
           (fun (u : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Uri (u, None)) : 'l2_pattern));
+             (return_term loc (Ast.Uri (u, None)) : 'term));
+        [Gramext.Stoken ("CSYMBOL", "")],
+        Gramext.action
+          (fun (s : string) (loc : Lexing.position * Lexing.position) ->
+             (return_term loc (Ast.Symbol (s, 0)) : 'term));
         [Gramext.Stoken ("IDENT", "");
          Gramext.Snterm
            (Grammar.Entry.obj
@@ -971,131 +1117,12 @@ let _ =
         Gramext.action
           (fun (s : 'explicit_subst) (id : string)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Ident (id, Some s)) : 'l2_pattern));
+             (return_term loc (Ast.Ident (id, Some s)) : 'term));
         [Gramext.Stoken ("IDENT", "")],
         Gramext.action
           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Ident (id, None)) : 'l2_pattern))]];
-      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", "non");
-         Gramext.Stoken ("IDENT", "associative")],
-        Gramext.action
-          (fun _ _ (loc : Lexing.position * Lexing.position) ->
-             (Gramext.NonA : 'associativity));
-        [Gramext.Stoken ("IDENT", "right");
-         Gramext.Stoken ("IDENT", "associative")],
-        Gramext.action
-          (fun _ _ (loc : Lexing.position * Lexing.position) ->
-             (Gramext.RightA : 'associativity));
-        [Gramext.Stoken ("IDENT", "left");
-         Gramext.Stoken ("IDENT", "associative")],
-        Gramext.action
-          (fun _ _ (loc : Lexing.position * Lexing.position) ->
-             (Gramext.LeftA : 'associativity))]];
-      Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
-      [None, None,
-       [[Gramext.Stoken ("IDENT", "with");
-         Gramext.Stoken ("IDENT", "precedence");
-         Gramext.Stoken ("NUMBER", "")],
-        Gramext.action
-          (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
-             (int_of_string 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.Sopt
-           (Gramext.Snterm
-              (Grammar.Entry.obj
-                 (associativity : 'associativity Grammar.Entry.e)));
-         Gramext.Sopt
-           (Gramext.Snterm
-              (Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e)));
-         Gramext.Stoken ("IDENT", "for");
-         Gramext.Snterm
-           (Grammar.Entry.obj
-              (level2_pattern : 'level2_pattern Grammar.Entry.e))],
-        Gramext.action
-          (fun (p2 : 'level2_pattern) _ (prec : 'precedence option)
-             (assoc : 'associativity option) (p1 : 'level1_pattern) _
-             (loc : Lexing.position * Lexing.position) ->
-             (p1, assoc, prec, p2 : '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))]];
-      Grammar.Entry.obj (phrase : 'phrase Grammar.Entry.e), None,
-      [None, None,
-       [[Gramext.Snterm
-           (Grammar.Entry.obj (notation : 'notation Grammar.Entry.e));
-         Gramext.Stoken ("SYMBOL", ".")],
-        Gramext.action
-          (fun _ (l1, assoc, prec, l2 : 'notation)
-             (loc : Lexing.position * Lexing.position) ->
-             (Notation (l1, assoc, prec, l2) : 'phrase));
-        [Gramext.Stoken ("IDENT", "print");
-         Gramext.Snterm
-           (Grammar.Entry.obj
-              (level2_pattern : 'level2_pattern Grammar.Entry.e));
-         Gramext.Stoken ("SYMBOL", ".")],
-        Gramext.action
-          (fun _ (p2 : 'level2_pattern) _
-             (loc : Lexing.position * Lexing.position) ->
-             (Print p2 : 'phrase))]]])
+             (return_term loc (Ast.Ident (id, None)) : 'term))]]])
+(* }}} *)
 
 (** {2 API implementation} *)
 
@@ -1106,19 +1133,29 @@ let exc_located_wrapper f =
   | 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)
-let parse_phrase stream =
-  exc_located_wrapper (fun () -> Grammar.Entry.parse phrase stream)
+let parse_level1_pattern lexbuf =
+  CicNotationLexer.set_lexbuf lexbuf;
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level1_pattern Stream.sempty)
+
+let parse_level2_ast lexbuf =
+  CicNotationLexer.set_lexbuf lexbuf;
+  exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast Stream.sempty)
+
+let parse_level2_meta lexbuf =
+  CicNotationLexer.set_lexbuf lexbuf;
+  exc_located_wrapper
+    (fun () -> Grammar.Entry.parse level2_meta Stream.sempty)
+
+let _ =
+  parse_level1_pattern_ref := parse_level1_pattern;
+  parse_level2_ast_ref := parse_level2_ast;
+  parse_level2_meta_ref := parse_level2_meta
 
 (** {2 Debugging} *)
 
 let print_l2_pattern () =
-  Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);
+  Grammar.print_entry Format.std_formatter (Grammar.Entry.obj term);
   Format.pp_print_flush Format.std_formatter ();
   flush stdout