X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.expanded.ml;h=5c73d2b4c4dec01a6808075289214cd6357d9834;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=69b51c398fa304da592702f9bcf71881f558498e;hpb=aca103d3c3d740efcc0bcc2932922cff77facb49;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
index 69b51c398..5c73d2b4c 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml
@@ -24,14 +24,14 @@
  *)
 
 oopen Printf
+oopen CicNotationEnvoopen CicNotationPt
 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 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)
@@ -39,27 +39,216 @@ 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 =
+(** {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 =
+  function
+    `Symbol s -> symbol s
+  | `Keyword s -> ident s
+  | `Number s -> number s
+ttype binding =
+    NoBinding
+  | Binding of string * value_type
+  | Env of (string * value_type) list
+llet make_action action bindings =
+  let rec aux (vl : env_type) =
+    function
+      [] -> Gramext.action (fun (loc : location) -> action vl loc)
+    | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
+    | Binding (name, TermType) :: tl ->
+        Gramext.action
+          (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl)
+    | Binding (name, StringType) :: tl ->
+        Gramext.action
+          (fun (v : string) ->
+             aux ((name, (StringType, StringValue v)) :: vl) tl)
+    | Binding (name, NumType) :: tl ->
+        Gramext.action
+          (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
+    | Binding (name, OptType t) :: tl ->
+        Gramext.action
+          (fun (v : 'a option) ->
+             aux ((name, (OptType t, OptValue v)) :: vl) tl)
+    | Binding (name, 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)
+  in
+  aux [] (List.rev bindings)
+llet flatten_opt =
+  let rec aux acc =
+    function
+      [] -> List.rev acc
+    | NoBinding :: tl -> aux acc tl
+    | Env names :: tl -> aux (List.rev names @ acc) tl
+    | 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 =
+  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
+  and aux_literal =
+    function
+      `Symbol s -> [NoBinding, symbol s]
+    | `Keyword s -> [NoBinding, ident s]
+    | `Number s -> [NoBinding, 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)
+  and aux_magic magic =
+    match magic with
+      Opt p ->
+        let (p_bindings, p_atoms, p_names, p_action) = inner_pattern p in
+        let action (env_opt : env_type option) (loc : location) =
+          match env_opt with
+            Some env -> List.map opt_binding_some env
+          | None -> List.map opt_binding_of_name p_names
+        in
+        [Env (List.map opt_declaration p_names),
+         Gramext.srules
+           [[Gramext.Sopt (Gramext.srules [p_atoms, p_action])],
+            Gramext.action action]]
+    | List0 (p, _) | 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
+        in
+        let action (env_list : env_type list) (loc : location) =
+          List.fold_right grow_env env_list env0
+        in
+        let g_symbol 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)
+          | _ -> assert false
+        in
+        [Env (List.map list_declaration p_names),
+         Gramext.srules
+           [[g_symbol (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
+  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)
+        p_bindings
+    in
+    p_bindings, p_atoms, p_names, action
+  in
+  aux pattern
+
+let level_of_int precedence =
+  if precedence < min_precedence || precedence > max_precedence then
+    raise (Level_not_found precedence);
+  string_of_int precedence
+
+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
+
+let delete atoms = Grammar.delete_rule l2_pattern atoms
+
+(** {2 Grammar} *)
+
+let 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
+
+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
-llet return_term loc term = AttributedTerm (`Loc loc, term)
-Elet _ =
+
+let return_term loc term = AttributedTerm (`Loc loc, term)
+
+let _ =
+  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)
+    in
+    aux [] last
+  in
+  Grammar.extend
+    [Grammar.Entry.obj (l2_pattern : 'a Grammar.Entry.e), None,
+     mk_level_list min_precedence max_precedence]
+
+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) in
+     and _ = (interpretation : 'interpretation Grammar.Entry.e)
+     and _ = (phrase : 'phrase Grammar.Entry.e) in
      let grammar_entry_create s =
        Grammar.Entry.create (Grammar.of_entry level1_pattern) s
      in
@@ -78,11 +267,15 @@ Elet _ =
        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 =
@@ -104,15 +297,15 @@ Elet _ =
       None,
       [None, None,
        [[Gramext.Snterm
-           (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
-         Gramext.Stoken ("EOI", "")],
+           (Grammar.Entry.obj
+              (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e))],
         Gramext.action
-          (fun _ (p : 'l1_pattern)
+          (fun (p : 'l1_simple_pattern)
              (loc : Lexing.position * Lexing.position) ->
-             (boxify p : 'level1_pattern))]];
+             (p : 'level1_pattern))]];
       Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Slist0
+       [[Gramext.Slist1
            (Gramext.Snterm
               (Grammar.Entry.obj
                  (l1_simple_pattern : 'l1_simple_pattern Grammar.Entry.e)))],
@@ -189,30 +382,22 @@ Elet _ =
         [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.Sself; Gramext.Stoken ("SYMBOL", "\\AS");
+         Gramext.Stoken ("IDENT", "")],
         Gramext.action
-          (fun _ (id : string) _ (p : 'l1_pattern) _
+          (fun (id : string) _ (p : 'l1_simple_pattern)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc
-                (Variable (Ascription (Layout (Box (H, p)), id))) :
+             (return_term loc (Variable (Ascription (p, id))) :
               'l1_simple_pattern));
-        [Gramext.Stoken ("SYMBOL", "[");
+        [Gramext.Stoken ("DELIM", "\\[");
          Gramext.Snterm
            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
-         Gramext.Stoken ("SYMBOL", "]")],
+         Gramext.Stoken ("DELIM", "\\]")],
         Gramext.action
           (fun _ (p : 'l1_pattern) _
              (loc : Lexing.position * Lexing.position) ->
@@ -221,30 +406,28 @@ Elet _ =
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
              (return_term loc (Layout Break) : 'l1_simple_pattern));
-        [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("SYMBOL", "[");
+        [Gramext.Stoken ("SYMBOL", "\\VBOX"); Gramext.Stoken ("DELIM", "\\[");
          Gramext.Snterm
            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
-         Gramext.Stoken ("SYMBOL", "]")],
+         Gramext.Stoken ("DELIM", "\\]")],
         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.Stoken ("SYMBOL", "\\HBOX"); Gramext.Stoken ("DELIM", "\\[");
          Gramext.Snterm
            (Grammar.Entry.obj (l1_pattern : 'l1_pattern Grammar.Entry.e));
-         Gramext.Stoken ("SYMBOL", "]")],
+         Gramext.Stoken ("DELIM", "\\]")],
         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", "\\ROOT"); Gramext.Sself;
          Gramext.Stoken ("SYMBOL", "\\OF"); Gramext.Sself],
         Gramext.action
-          (fun (arg : 'l1_simple_pattern) _ (index : 'l1_pattern) _
+          (fun (arg : 'l1_simple_pattern) _ (index : 'l1_simple_pattern) _
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout (Root (arg, Layout (Box (H, index))))) :
+             (return_term loc (Layout (Root (arg, index))) :
               'l1_simple_pattern));
         [Gramext.Stoken ("SYMBOL", "\\SQRT"); Gramext.Sself],
         Gramext.action
@@ -256,30 +439,16 @@ Elet _ =
           (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.Sself; Gramext.Stoken ("SYMBOL", "\\ATOP"); Gramext.Sself],
         Gramext.action
-          (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
+          (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_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", "]")],
+             (return_term loc (Layout (Atop (p1, p2))) : 'l1_simple_pattern));
+        [Gramext.Sself; Gramext.Stoken ("SYMBOL", "\\OVER"); Gramext.Sself],
         Gramext.action
-          (fun _ (p2 : 'l1_pattern) _ (p1 : 'l1_pattern) _
+          (fun (p2 : 'l1_simple_pattern) _ (p1 : 'l1_simple_pattern)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Layout (Over (boxify p1, boxify p2))) :
-              'l1_simple_pattern));
+             (return_term loc (Layout (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)
@@ -321,7 +490,11 @@ Elet _ =
         Gramext.action
           (fun (m : 'l1_magic_pattern)
              (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Magic m) : 'l1_simple_pattern))]];
+             (return_term loc (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,
       [None, None,
@@ -344,26 +517,68 @@ Elet _ =
           (fun _ (loc : Lexing.position * Lexing.position) ->
              (`Prop : 'sort))]];
       Grammar.Entry.obj (explicit_subst : 'explicit_subst Grammar.Entry.e),
-      None, [None, None, []];
+      None,
+      [None, None,
+       [[Gramext.Stoken ("SYMBOL", "\\subst"); Gramext.Stoken ("SYMBOL", "[");
+         Gramext.Slist1sep
+           (Gramext.srules
+              [[Gramext.Stoken ("IDENT", "");
+                Gramext.Stoken ("SYMBOL", "≔");
+                Gramext.Snterm
+                  (Grammar.Entry.obj
+                     (l2_pattern : 'l2_pattern Grammar.Entry.e))],
+               Gramext.action
+                 (fun (t : 'l2_pattern) _ (i : string)
+                    (loc : Lexing.position * Lexing.position) ->
+                    (i, t : 'e__1))],
+            Gramext.Stoken ("SYMBOL", ";"));
+         Gramext.Stoken ("SYMBOL", "]")],
+        Gramext.action
+          (fun _ (substs : 'e__1 list) _ _
+             (loc : Lexing.position * Lexing.position) ->
+             (substs : 'explicit_subst))]];
       Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e), None,
-      [None, 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) ->
+             (Some p : 'meta_subst));
+        [Gramext.Stoken ("SYMBOL", "_")],
+        Gramext.action
+          (fun (s : string) (loc : Lexing.position * Lexing.position) ->
+             (None : 'meta_subst))]];
+      Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e), None,
+      [None, None,
+       [[Gramext.Stoken ("SYMBOL", "[");
+         Gramext.Slist0
+           (Gramext.Snterm
+              (Grammar.Entry.obj (meta_subst : 'meta_subst Grammar.Entry.e)));
+         Gramext.Stoken ("SYMBOL", "]")],
+        Gramext.action
+          (fun _ (substs : 'meta_subst list) _
+             (loc : Lexing.position * Lexing.position) ->
+             (substs : 'meta_substs))]];
       Grammar.Entry.obj
         (possibly_typed_name : 'possibly_typed_name Grammar.Entry.e),
       None,
       [None, None,
-       [[Gramext.Stoken ("IDENT", "")],
+       [[Gramext.Snterm
+           (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e))],
         Gramext.action
-          (fun (id : string) (loc : Lexing.position * Lexing.position) ->
-             (Cic.Name id, None : 'possibly_typed_name));
-        [Gramext.Stoken ("SYMBOL", "("); Gramext.Stoken ("IDENT", "");
+          (fun (id : 'bound_name) (loc : Lexing.position * Lexing.position) ->
+             (id, None : 'possibly_typed_name));
+        [Gramext.Stoken ("SYMBOL", "(");
+         Gramext.Snterm
+           (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e));
          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) _
+          (fun _ (typ : 'l2_pattern) _ (id : 'bound_name) _
              (loc : Lexing.position * Lexing.position) ->
-             (Cic.Name id, Some typ : 'possibly_typed_name))]];
+             (id, Some typ : 'possibly_typed_name))]];
       Grammar.Entry.obj (match_pattern : 'match_pattern Grammar.Entry.e),
       None,
       [None, None,
@@ -400,13 +615,25 @@ Elet _ =
         Gramext.action
           (fun _ (loc : Lexing.position * Lexing.position) ->
              (`Pi : 'binder))]];
+      Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e), None,
+      [None, None,
+       [[Gramext.Stoken ("SYMBOL", "\\FRESH"); Gramext.Stoken ("IDENT", "")],
+        Gramext.action
+          (fun (i : string) _ (loc : Lexing.position * Lexing.position) ->
+             (Variable (FreshVar i) : 'bound_name));
+        [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.Stoken ("IDENT", ""),
+                  (Gramext.Snterm
+                     (Grammar.Entry.obj
+                        (bound_name : 'bound_name Grammar.Entry.e)),
                    Gramext.Stoken ("SYMBOL", ","));
                 Gramext.Sopt
                   (Gramext.srules
@@ -417,18 +644,20 @@ Elet _ =
                       Gramext.action
                         (fun (p : 'l2_pattern) _
                            (loc : Lexing.position * Lexing.position) ->
-                           (p : 'e__2))]);
+                           (p : 'e__3))]);
                 Gramext.Stoken ("SYMBOL", ")")],
                Gramext.action
-                 (fun _ (ty : 'e__2 option) (vars : string list) _
+                 (fun _ (ty : 'e__3 option) (vars : 'bound_name list) _
                     (loc : Lexing.position * Lexing.position) ->
-                    (vars, ty : 'e__3))])],
+                    (vars, ty : 'e__4))])],
         Gramext.action
-          (fun (clusters : 'e__3 list)
+          (fun (clusters : 'e__4 list)
              (loc : Lexing.position * Lexing.position) ->
              (clusters : 'bound_names));
         [Gramext.Slist1sep
-           (Gramext.Stoken ("IDENT", ""), Gramext.Stoken ("SYMBOL", ","));
+           (Gramext.Snterm
+              (Grammar.Entry.obj (bound_name : 'bound_name Grammar.Entry.e)),
+            Gramext.Stoken ("SYMBOL", ","));
          Gramext.Sopt
            (Gramext.srules
               [[Gramext.Stoken ("SYMBOL", ":");
@@ -438,9 +667,9 @@ Elet _ =
                Gramext.action
                  (fun (p : 'l2_pattern) _
                     (loc : Lexing.position * Lexing.position) ->
-                    (p : 'e__1))])],
+                    (p : 'e__2))])],
         Gramext.action
-          (fun (ty : 'e__1 option) (vars : string list)
+          (fun (ty : 'e__2 option) (vars : 'bound_name list)
              (loc : Lexing.position * Lexing.position) ->
              ([vars, ty] : 'bound_names))]];
       Grammar.Entry.obj (induction_kind : 'induction_kind Grammar.Entry.e),
@@ -458,18 +687,22 @@ Elet _ =
       [None, None,
        [[Gramext.Slist1sep
            (Gramext.srules
-              [[Gramext.Stoken ("IDENT", "");
+              [[Gramext.Snterm
+                  (Grammar.Entry.obj
+                     (bound_name : 'bound_name Grammar.Entry.e));
                 Gramext.Snterm
                   (Grammar.Entry.obj
                      (bound_names : 'bound_names Grammar.Entry.e));
                 Gramext.Sopt
                   (Gramext.srules
                      [[Gramext.Stoken ("IDENT", "on");
-                       Gramext.Stoken ("IDENT", "")],
+                       Gramext.Snterm
+                         (Grammar.Entry.obj
+                            (bound_name : 'bound_name Grammar.Entry.e))],
                       Gramext.action
-                        (fun (id : string) _
+                        (fun (id : 'bound_name) _
                            (loc : Lexing.position * Lexing.position) ->
-                           (id : 'e__4))]);
+                           (id : 'e__5))]);
                 Gramext.Sopt
                   (Gramext.srules
                      [[Gramext.Stoken ("SYMBOL", ":");
@@ -479,15 +712,15 @@ Elet _ =
                       Gramext.action
                         (fun (p : 'l2_pattern) _
                            (loc : Lexing.position * Lexing.position) ->
-                           (p : 'e__5))]);
+                           (p : 'e__6))]);
                 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)
+                 (fun (body : 'l2_pattern) _ (ty : 'e__6 option)
+                    (index_name : 'e__5 option) (args : 'bound_names)
+                    (name : 'bound_name)
                     (loc : Lexing.position * Lexing.position) ->
                     (let body = fold_binder `Lambda args body in
                      let ty =
@@ -503,7 +736,10 @@ Elet _ =
                      in
                      let rec find_arg name n =
                        function
-                         [] -> fail loc (sprintf "Argument %s not found" name)
+                         [] ->
+                           fail loc
+                             (sprintf "Argument %s not found"
+                                (CicNotationPp.pp_term name))
                        | (l, _) :: tl ->
                            match position_of name 0 l with
                              None, len -> find_arg name (n + len) tl
@@ -514,11 +750,11 @@ Elet _ =
                          None -> 0
                        | Some name -> find_arg name 0 args
                      in
-                     (Cic.Name name, ty), body, index :
-                     'e__6))],
+                     (name, ty), body, index :
+                     'e__7))],
             Gramext.Stoken ("IDENT", "and"))],
         Gramext.action
-          (fun (defs : 'e__6 list)
+          (fun (defs : 'e__7 list)
              (loc : Lexing.position * Lexing.position) ->
              (defs : 'let_defs))]];
       Grammar.Entry.obj
@@ -542,12 +778,15 @@ Elet _ =
       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))],
+           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
+         Gramext.Stoken ("DELIM", "\\]")],
         Gramext.action
-          (fun (none : 'l2_pattern) (some : 'l2_pattern) _
+          (fun _ (none : 'l2_pattern) _ _ (some : 'l2_pattern) _ _
              (loc : Lexing.position * Lexing.position) ->
              (Default (some, none) : 'l2_magic_pattern));
         [Gramext.Stoken ("SYMBOL", "\\FOLD");
@@ -555,23 +794,28 @@ Elet _ =
            [[Gramext.Stoken ("IDENT", "right")],
             Gramext.action
               (fun _ (loc : Lexing.position * Lexing.position) ->
-                 (`Right : 'e__7));
+                 (`Right : 'e__8));
             [Gramext.Stoken ("IDENT", "left")],
             Gramext.action
               (fun _ (loc : Lexing.position * Lexing.position) ->
-                 (`Left : 'e__7))];
+                 (`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))],
+           (Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e));
+         Gramext.Stoken ("DELIM", "\\]")],
         Gramext.action
-          (fun (recursive : 'l2_pattern) (id : string) _ (base : 'l2_pattern)
-             (kind : 'e__7) _ (loc : Lexing.position * Lexing.position) ->
+          (fun _ (recursive : 'l2_pattern) _ (id : string) _ _
+             (base : 'l2_pattern) _ (kind : 'e__8) _
+             (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,
+      Grammar.Entry.obj (l2_pattern : 'l2_pattern Grammar.Entry.e),
+      Some (Gramext.Level "10"),
+      [Some "10", Some Gramext.NonA,
        [[Gramext.Stoken ("IDENT", "let");
          Gramext.Snterm
            (Grammar.Entry.obj
@@ -593,8 +837,10 @@ Elet _ =
           (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,
+             (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
            (Grammar.Entry.obj (binder : 'binder Grammar.Entry.e));
          Gramext.Snterm
@@ -603,10 +849,10 @@ Elet _ =
         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,
+             (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,
        [[Gramext.Sself; Gramext.Sself],
         Gramext.action
           (fun (p2 : 'l2_pattern) (p1 : 'l2_pattern)
@@ -618,9 +864,10 @@ Elet _ =
                 | term -> [term]
               in
               return_term loc (Appl (aux p1 @ [p2])) :
-              'l2_pattern))];
-       Some "80", None, [];
-       Some "90", Some Gramext.NonA,
+              '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))],
@@ -659,7 +906,7 @@ Elet _ =
                Gramext.action
                  (fun _ (ty : 'l2_pattern) _
                     (loc : Lexing.position * Lexing.position) ->
-                    (ty : 'e__8))]);
+                    (ty : 'e__9))]);
          Gramext.Stoken ("IDENT", "match"); Gramext.Sself;
          Gramext.Sopt
            (Gramext.srules
@@ -667,7 +914,7 @@ Elet _ =
                Gramext.action
                  (fun (id : string) _
                     (loc : Lexing.position * Lexing.position) ->
-                    (id : 'e__9))]);
+                    (id : 'e__10))]);
          Gramext.Stoken ("IDENT", "with"); Gramext.Stoken ("SYMBOL", "[");
          Gramext.Slist0sep
            (Gramext.srules
@@ -681,28 +928,24 @@ Elet _ =
                Gramext.action
                  (fun (rhs : 'l2_pattern) _ (lhs : 'match_pattern)
                     (loc : Lexing.position * Lexing.position) ->
-                    (lhs, rhs : 'e__10))],
+                    (lhs, rhs : 'e__11))],
             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)
+          (fun _ (patterns : 'e__11 list) _ _ (indty_ident : 'e__10 option)
+             (t : 'l2_pattern) _ (outtyp : 'e__9 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))],
+           (Grammar.Entry.obj (meta_substs : 'meta_substs Grammar.Entry.e))],
         Gramext.action
-          (fun (s : 'meta_subst) (m : string)
+          (fun (s : 'meta_substs) (m : string)
              (loc : Lexing.position * Lexing.position) ->
              (return_term loc (Meta (int_of_string m, s)) : 'l2_pattern));
         [Gramext.Stoken ("META", "")],
@@ -716,8 +959,7 @@ Elet _ =
         [Gramext.Stoken ("NUMBER", "")],
         Gramext.action
           (fun (n : string) (loc : Lexing.position * Lexing.position) ->
-             (prerr_endline "number"; return_term loc (Num (n, 0)) :
-              'l2_pattern));
+             (return_term loc (Num (n, 0)) : 'l2_pattern));
         [Gramext.Stoken ("URI", "")],
         Gramext.action
           (fun (u : string) (loc : Lexing.position * Lexing.position) ->
@@ -733,8 +975,7 @@ Elet _ =
         [Gramext.Stoken ("IDENT", "")],
         Gramext.action
           (fun (id : string) (loc : Lexing.position * Lexing.position) ->
-             (return_term loc (Ident (id, None)) : 'l2_pattern))];
-       Some "100", None, []];
+             (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", "");
@@ -777,47 +1018,51 @@ Elet _ =
       Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e),
       None,
       [None, None,
-       [[Gramext.Stoken ("IDENT", "right");
+       [[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) ->
-             (`Right : 'associativity));
+             (Gramext.RightA : 'associativity));
         [Gramext.Stoken ("IDENT", "left");
          Gramext.Stoken ("IDENT", "associative")],
         Gramext.action
           (fun _ _ (loc : Lexing.position * Lexing.position) ->
-             (`Left : 'associativity))]];
+             (Gramext.LeftA : 'associativity))]];
       Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
       [None, None,
-       [[Gramext.Stoken ("IDENT", "at");
+       [[Gramext.Stoken ("IDENT", "with");
          Gramext.Stoken ("IDENT", "precedence");
          Gramext.Stoken ("NUMBER", "")],
         Gramext.action
           (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
-             (n : 'precedence))]];
+             (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.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)))],
+              (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 (prec : 'precedence option) (assoc : 'associativity option)
-             (p2 : 'level2_pattern) _ (p1 : 'level1_pattern) _
+          (fun (p2 : 'level2_pattern) _ (prec : 'precedence option)
+             (assoc : 'associativity option) (p1 : 'level1_pattern) _
              (loc : Lexing.position * Lexing.position) ->
-             (() : 'notation))]];
+             (p1, assoc, prec, p2 : 'notation))]];
       Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
       None,
       [None, None,
@@ -832,7 +1077,27 @@ Elet _ =
         Gramext.action
           (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
              (loc : Lexing.position * Lexing.position) ->
-             (() : 'interpretation))]]])
+             (() : '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))]]])
+
+(** {2 API implementation} *)
 
 let exc_located_wrapper f =
   try f () with
@@ -843,153 +1108,14 @@ let exc_located_wrapper f =
 
 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)
 
-(** {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
+(** {2 Debugging} *)
 
 let print_l2_pattern () =
   Grammar.print_entry Format.std_formatter (Grammar.Entry.obj l2_pattern);