Thorough rewriting of the Pcoq API towards safety and static invariants.

Amongst other things:

1. No more unsafe grammar extensions, except when going through the CAMLPX-based
Pcoq.Gram module. This is mostly safe because CAMLPX adds casts to ensure that
parsing rules are well-typed. In particular, constr notation is now based on
GADTs ensuring well-typedness.

2. Less reliance on unsafe coq inside Pcoq, and exposing a self-contained API.
The Entry module was also removed as it now results useless.

3. Purely functional API for synchronized grammar extension. This gets rid of
quite buggy code maintaining a table of empty entries to work around CAMLPX bugs.
The state modification is now explicit and grammar extensions synchronized with
the summary must provide the rules they want to perform instead of doing so
imperatively.

1 files changed, 160 insertions, 379 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6dcf76da8c..efb89cd6e1 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -19,10 +19,19 @@ module G = GrammarMake (CLexer)
 
 let warning_verbose = Compat.warning_verbose
 
-module Symbols = GramextMake(G)
+let of_coq_assoc = function
+| Extend.RightA -> CompatGramext.RightA
+| Extend.LeftA -> CompatGramext.LeftA
+| Extend.NonA -> CompatGramext.NonA
+
+let of_coq_position = function
+| Extend.First -> CompatGramext.First
+| Extend.Last -> CompatGramext.Last
+| Extend.Before s -> CompatGramext.Before s
+| Extend.After s -> CompatGramext.After s
+| Extend.Level s -> CompatGramext.Level s
 
-let gram_token_of_token = Symbols.stoken
-let gram_token_of_string s = gram_token_of_token (CLexer.terminal s)
+module Symbols = GramextMake(G)
 
 let camlp4_verbosity silent f x =
   let a = !warning_verbose in
@@ -32,26 +41,6 @@ let camlp4_verbosity silent f x =
 
 let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
 
-
-(** [grammar_object] is the superclass of all grammar entries *)
-
-module type Gramobj =
-sig
-  type grammar_object
-  val weaken_entry : 'a G.entry -> grammar_object G.entry
-end
-
-module Gramobj : Gramobj =
-struct
-  type grammar_object = Obj.t
-  let weaken_entry e = Obj.magic e
-end
-
-(** Grammar entries with associated types *)
-
-type grammar_object = Gramobj.grammar_object
-let weaken_entry x = Gramobj.weaken_entry x
-
 (** Grammar extensions *)
 
 (** NB: [extend_statment =
@@ -63,14 +52,57 @@ let weaken_entry x = Gramobj.weaken_entry x
     In [single_extend_statement], first two parameters are name and
     assoc iff a level is created *)
 
+(** Binding general entry keys to symbol *)
+
+let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function
+| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc))
+| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x))
+
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
+  | Atoken t -> Symbols.stoken t
+  | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
+  | Alist1sep (s,sep) ->
+      Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
+  | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
+  | Alist0sep (s,sep) ->
+      Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep)
+  | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
+  | Aself -> Symbols.sself
+  | Anext -> Symbols.snext
+  | Aentry e ->
+    Symbols.snterm (G.Entry.obj e)
+  | Aentryl (e, n) ->
+    Symbols.snterml (G.Entry.obj e, string_of_int n)
+  | Arules rs ->
+    G.srules' (List.map symbol_of_rules rs)
+
+and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
+| Stop -> fun accu -> accu
+| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
+
+and symbol_of_rules : type a. a Extend.rules -> _ = function
+| Rules (r, act) ->
+  let symb = symbol_of_rule r.norec_rule [] in
+  let act = of_coq_action r.norec_rule act in
+  (symb, act)
+
+let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
+| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
+
+let of_coq_single_extend_statement (lvl, assoc, rule) =
+  (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
+
+let of_coq_extend_statement (pos, st) =
+  (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
+
 (** Type of reinitialization data *)
 type gram_reinit = gram_assoc * gram_position
 
+type extend_rule =
+| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule
+
 type ext_kind =
-  | ByGrammar of
-      grammar_object G.entry
-      * gram_reinit option (** for reinitialization if ever needed *)
-      * G.extend_statment
+  | ByGrammar of extend_rule
   | ByEXTEND of (unit -> unit) * (unit -> unit)
 
 (** The list of extensions *)
@@ -86,13 +118,28 @@ let grammar_delete e reinit (pos,rls) =
     (List.rev rls);
   match reinit with
   | Some (a,ext) ->
-    let lev = match Option.map Compat.to_coq_position pos with
-    | Some (Level n) -> n
+    let a = of_coq_assoc a in
+    let ext = of_coq_position ext in
+    let lev = match pos with
+    | Some (CompatGramext.Level n) -> n
     | _ -> assert false
     in
     maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]])
   | None -> ()
 
+(** Extension *)
+
+let grammar_extend e reinit ext =
+  let ext = of_coq_extend_statement ext in
+  let undo () = grammar_delete e reinit ext in
+  let redo () = camlp4_verbose (maybe_uncurry (G.extend e)) ext in
+  camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state;
+  redo ()
+
+let grammar_extend_sync e reinit ext =
+  camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
+  camlp4_verbose (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext)
+
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
 
@@ -119,12 +166,6 @@ module Gram =
       G.delete_rule e pil
   end
 
-(** This extension command is used by the Grammar constr *)
-
-let unsafe_grammar_extend e reinit ext =
-  camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
-  camlp4_verbose (maybe_uncurry (G.extend e)) ext
-
 (** Remove extensions
 
    [n] is the number of extended entries (not the number of Grammar commands!)
@@ -134,9 +175,8 @@ let rec remove_grammars n =
   if n>0 then
     (match !camlp4_state with
        | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove")
-       | ByGrammar(g,reinit,ext)::t ->
-           let f (a,b) = (of_coq_assoc a, of_coq_position b) in
-           grammar_delete g (Option.map f reinit) ext;
+       | ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
+           grammar_delete g reinit (of_coq_extend_statement ext);
            camlp4_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
@@ -188,21 +228,9 @@ let get_univ u =
   if Hashtbl.mem utables u then u
   else raise Not_found
 
-(** A table associating grammar to entries *)
-let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
-
-let get_grammar (e : 'a Entry.t) : 'a Gram.entry =
-  Obj.magic (String.Map.find (Entry.repr e) !gtable)
-
-let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) =
-  assert (not (String.Map.mem (Entry.repr e) !gtable));
-  gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable
-
 let new_entry u s =
   let ename = u ^ ":" ^ s in
-  let entry = Entry.create ename in
   let e = Gram.entry_create ename in
-  let () = set_grammar entry e in
   e
 
 let make_gen_entry u s = new_entry u s
@@ -374,344 +402,97 @@ let main_entry = Vernac_.main_entry
 let set_command_entry e = Vernac_.command_entry_ref := e
 let get_command_entry () = !Vernac_.command_entry_ref
 
-(**********************************************************************)
-(* This determines (depending on the associativity of the current
-   level and on the expected associativity) if a reference to constr_n is
-   a reference to the current level (to be translated into "SELF" on the
-   left border and into "constr LEVEL n" elsewhere), to the level below
-   (to be translated into "NEXT") or to an below wrt associativity (to be
-   translated in camlp4 into "constr" without level) or to another level
-   (to be translated into "constr LEVEL n")
-
-   The boolean is true if the entry was existing _and_ empty; this to
-   circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the
-   converse of the extension mechanism *)
-
-let constr_level = string_of_int
-
-let default_levels =
-  [200,Extend.RightA,false;
-   100,Extend.RightA,false;
-   99,Extend.RightA,true;
-   10,Extend.RightA,false;
-   9,Extend.RightA,false;
-   8,Extend.RightA,true;
-   1,Extend.LeftA,false;
-   0,Extend.RightA,false]
-
-let default_pattern_levels =
-  [200,Extend.RightA,true;
-   100,Extend.RightA,false;
-   99,Extend.RightA,true;
-   11,Extend.LeftA,false;
-   10,Extend.RightA,false;
-   1,Extend.LeftA,false;
-   0,Extend.RightA,false]
-
-let level_stack =
-  ref [(default_levels, default_pattern_levels)]
-
-(* At a same level, LeftA takes precedence over RightA and NoneA *)
-(* In case, several associativity exists for a level, we make two levels, *)
-(* first LeftA, then RightA and NoneA together *)
-
-let admissible_assoc = function
-  | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false
-  | Extend.RightA, Some Extend.LeftA -> false
-  | _ -> true
-
-let create_assoc = function
-  | None -> Extend.RightA
-  | Some a -> a
-
-let error_level_assoc p current expected =
-  let pr_assoc = function
-    | Extend.LeftA -> str "left"
-    | Extend.RightA -> str "right"
-    | Extend.NonA -> str "non" in
-  errorlabstrm ""
-    (str "Level " ++ int p ++ str " is already declared " ++
-     pr_assoc current ++ str " associative while it is now expected to be " ++
-     pr_assoc expected ++ str " associative.")
-
-let create_pos = function
-  | None -> Extend.First
-  | Some lev -> Extend.After (constr_level lev)
-
-let find_position_gen forpat ensure assoc lev =
-  let ccurrent,pcurrent as current = List.hd !level_stack in
-  match lev with
-  | None ->
-      level_stack := current :: !level_stack;
-      None, None, None, None
-  | Some n ->
-      let after = ref None in
-      let init = ref None in
-      let rec add_level q = function
-        | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
-        | (p,a,reinit)::l when Int.equal p n ->
-            if reinit then
-	      let a' = create_assoc assoc in
-              (init := Some (a',create_pos q); (p,a',false)::l)
-	    else if admissible_assoc (a,assoc) then
-	      raise Exit
-            else
-	      error_level_assoc p a (Option.get assoc)
-	| l -> after := q; (n,create_assoc assoc,ensure)::l
-      in
-      try
-	let updated =
-	  if forpat then (ccurrent, add_level None pcurrent)
-	  else (add_level None ccurrent, pcurrent) in
-        level_stack := updated:: !level_stack;
-	let assoc = create_assoc assoc in
-        begin match !init with
-        | None ->
-	  (* Create the entry *)
-	   Some (create_pos !after), Some assoc, Some (constr_level n), None
-        | _ ->
-	  (* The reinit flag has been updated *)
-	   Some (Extend.Level (constr_level n)), None, None, !init
-        end
-      with
-	  (* Nothing has changed *)
-          Exit ->
-            level_stack := current :: !level_stack;
-	    (* Just inherit the existing associativity and name (None) *)
-	    Some (Extend.Level (constr_level n)), None, None, None
-
-let remove_levels n =
-  level_stack := List.skipn n !level_stack
-
-let rec list_mem_assoc_triple x = function
-  | [] -> false
-  | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l
-
-let register_empty_levels forpat levels =
-  let filter n =
-    try
-      let levels = (if forpat then snd else fst) (List.hd !level_stack) in
-      if not (list_mem_assoc_triple n levels) then
-        Some (find_position_gen forpat true None (Some n))
-      else None
-    with Failure _ -> None
-  in
-  List.map_filter filter levels
-
-let find_position forpat assoc level =
-  find_position_gen forpat false assoc level
-
-(* Synchronise the stack of level updates *)
-let synchronize_level_positions () =
-  let _ = find_position true None None in ()
-
-(**********************************************************************)
-(* Binding constr entry keys to entries                               *)
-
-(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
-let camlp4_assoc = function
-  | Some Extend.NonA | Some Extend.RightA -> Extend.RightA
-  | None | Some Extend.LeftA -> Extend.LeftA
-
-let assoc_eq al ar = match al, ar with
-| Extend.NonA, Extend.NonA
-| Extend.RightA, Extend.RightA
-| Extend.LeftA, Extend.LeftA -> true
-| _, _ -> false
-
-(* [adjust_level assoc from prod] where [assoc] and [from] are the name
-   and associativity of the level where to add the rule; the meaning of
-   the result is
-
-     None = SELF
-     Some None = NEXT
-     Some (Some (n,cur)) = constr LEVEL n
-         s.t. if [cur] is set then [n] is the same as the [from] level *)
-let adjust_level assoc from = function
-(* Associativity is None means force the level *)
-  | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
-(* Compute production name on the right side *)
-  (* If NonA or LeftA on the right-hand side, set to NEXT *)
-  | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) ->
-      Some None
-  (* If RightA on the right-hand side, set to the explicit (current) level *)
-  | (NumLevel n,BorderProd (Right,Some Extend.RightA)) ->
-      Some (Some (n,true))
-(* Compute production name on the left side *)
-  (* If NonA on the left-hand side, adopt the current assoc ?? *)
-  | (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None
-  (* If the expected assoc is the current one, set to SELF *)
-  | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) ->
-      None
-  (* Otherwise, force the level, n or n-1, according to expected assoc *)
-  | (NumLevel n,BorderProd (Left,Some a)) ->
-    begin match a with
-    | Extend.LeftA -> Some (Some (n, true))
-    | _ -> Some None
-    end
-  (* None means NEXT *)
-  | (NextLevel,_) -> Some None
-(* Compute production name elsewhere *)
-  | (NumLevel n,InternalProd) ->
-      match from with
-	| ETConstr (p,()) when Int.equal p (n + 1) -> Some None
-	| ETConstr (p,()) -> Some (Some (n, Int.equal n p))
-	| _ -> Some (Some (n,false))
-
-let compute_entry adjust forpat = function
-  | ETConstr (n,q) ->
-      (if forpat then weaken_entry Constr.pattern
-       else weaken_entry Constr.operconstr),
-      adjust (n,q), false
-  | ETName -> weaken_entry Prim.name, None, false
-  | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList")
-  | ETBinder false -> weaken_entry Constr.binder, None, false
-  | ETBinderList (true,tkl) ->
-    let () = match tkl with [] -> () | _ -> assert false in
-    weaken_entry Constr.open_binders, None, false
-  | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.")
-  | ETBigint -> weaken_entry Prim.bigint, None, false
-  | ETReference -> weaken_entry Constr.global, None, false
-  | ETPattern -> weaken_entry Constr.pattern, None, false
-  | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
-  | ETOther (u,n) -> assert false
-
-(* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key forpat level =
-  if level = 200 && not forpat then weaken_entry Constr.binder_constr, None
-  else if forpat then weaken_entry Constr.pattern, Some level
-  else weaken_entry Constr.operconstr, Some level
-
-(* This computes the name to give to a production knowing the name and
-   associativity of the level where it must be added *)
-let interp_constr_prod_entry_key ass from forpat en =
-  compute_entry (adjust_level ass from) forpat en
-
-(**********************************************************************)
-(* Binding constr entry keys to symbols                               *)
-
-let is_self from e =
-  match from, e with
-      ETConstr(n,()), ETConstr(NumLevel n',
-        BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false
-    | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n'
-    | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint
-      | ETPattern, ETPattern) -> true
-    | ETOther(s1,s2), ETOther(s1',s2') ->
-      String.equal s1 s1' && String.equal s2 s2'
-    | _ -> false
-
-let is_binder_level from e =
-  match from, e with
-      ETConstr(200,()),
-      ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true
-    | _ -> false
-
-let make_sep_rules tkl =
-  Gram.srules'
-    [List.map gram_token_of_token tkl,
-     List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
-       (Gram.action (fun loc -> ()))]
-
-let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
-  if is_binder_level from typ then
-    if forpat then
-      Symbols.snterml (Gram.Entry.obj Constr.pattern,"200")
-    else
-      Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200")
-  else if is_self from typ then
-      Symbols.sself
-  else
-    match typ with
-    | ETConstrList (typ',[]) ->
-        Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
-    | ETConstrList (typ',tkl) ->
-        Symbols.slist1sep
-          (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
-          make_sep_rules tkl)
-    | ETBinderList (false,[]) ->
-        Symbols.slist1
-	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
-    | ETBinderList (false,tkl) ->
-        Symbols.slist1sep
-          (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
-          make_sep_rules tkl)
-
-    | _ ->
-    match interp_constr_prod_entry_key assoc from forpat typ with
-      | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj)
-      | (eobj,Some None,_) -> Symbols.snext
-      | (eobj,Some (Some (lev,cur)),_) ->
-          Symbols.snterml (Gram.Entry.obj eobj,constr_level lev)
-
-(** Binding general entry keys to symbol *)
-
-let tuplify l =
-  List.fold_left (fun accu x -> Obj.repr (x, accu)) (Obj.repr ()) l
-
-let rec adj : type a b c. (a, b, Loc.t -> Loc.t * c) adj -> _ = function
-| Adj0 -> Obj.magic (fun accu f loc -> f (Obj.repr (to_coqloc loc, tuplify accu)))
-| AdjS e -> Obj.magic (fun accu f x -> adj e (x :: accu) f)
-
-let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
-  | Atoken t -> Symbols.stoken t
-  | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
-  | Alist1sep (s,sep) ->
-      Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
-  | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s)
-  | Alist0sep (s,sep) ->
-      Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
-  | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s)
-  | Aself -> Symbols.sself
-  | Anext -> Symbols.snext
-  | Aentry e ->
-    let e = get_grammar e in
-    Symbols.snterm (Gram.Entry.obj (weaken_entry e))
-  | Aentryl (e, n) ->
-    let e = get_grammar e in
-    Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
-  | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x))
-
-and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
-| Stop -> fun accu -> accu
-| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
+let epsilon_value f e =
+  let r = Rule (Next (Stop, e), fun x _ -> f x) in
+  let ext = of_coq_extend_statement (None, [None, None, [r]]) in
+  let entry = G.entry_create "epsilon" in
+  let () = maybe_uncurry (G.extend entry) ext in
+  try Some (parse_string entry "") with _ -> None
 
-and symbol_of_rules : type a. a Extend.rules -> _ = function
-| Rule0 -> fun accu _ -> accu
-| RuleS (r, e, rs) -> fun accu f ->
-  let symb = symbol_of_rule r [] in
-  let act = adj e [] f in
-  symbol_of_rules rs ((symb, act) :: accu) (fun x -> IS (f x))
+(** Synchronized grammar extensions *)
 
-let level_of_snterml e = int_of_string (Symbols.snterml_level e)
+module GramState = Store.Make(struct end)
 
-let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function
-| Stop -> fun f -> Gram.action (fun loc -> f (to_coqloc loc))
-| Next (r, _) -> fun f -> Gram.action (fun x -> of_coq_action r (f x))
+type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 
-let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
-| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
+module GrammarCommand = Dyn.Make(struct end)
+module GrammarInterp = struct type 'a t = 'a grammar_extension end
+module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
 
-let of_coq_single_extend_statement (lvl, assoc, rule) =
-  (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
+let grammar_interp = ref GrammarInterpMap.empty
 
-let of_coq_extend_statement (pos, st) =
-  (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
-
-let grammar_extend e reinit ext =
-  let ext = of_coq_extend_statement ext in
-  unsafe_grammar_extend e reinit ext
+let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref []
 
-let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
+type 'a grammar_command = 'a GrammarCommand.tag
 
-let list_entry_names () = []
+let create_grammar_command name interp : _ grammar_command =
+  let obj = GrammarCommand.create name in
+  let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
+  obj
 
-let epsilon_value f e =
-  let r = Rule (Next (Stop, e), fun x _ -> f x) in
-  let ext = of_coq_extend_statement (None, [None, None, [r]]) in
-  let entry = G.entry_create "epsilon" in
-  let () = maybe_uncurry (Gram.extend entry) ext in
-  try Some (parse_string entry "") with _ -> None
+let extend_grammar_command tag g =
+  let modify = GrammarInterpMap.find tag !grammar_interp in
+  let grammar_state = match !grammar_stack with
+  | [] -> GramState.empty
+  | (_, _, st) :: _ -> st
+  in
+  let (rules, st) = modify g grammar_state in
+  let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in
+  let () = List.iter iter rules in
+  let nb = List.length rules in
+  grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack
+
+let recover_grammar_command (type a) (tag : a grammar_command) : a list =
+  let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) ->
+    match GrammarCommand.eq tag tag' with
+    | None -> None
+    | Some Refl -> Some v
+  in
+  List.map_filter filter !grammar_stack
+
+let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g
+
+(* Summary functions: the state of the lexer is included in that of the parser.
+   Because the grammar affects the set of keywords when adding or removing
+   grammar rules. *)
+type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t
+
+let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ())
+
+(* We compare the current state of the grammar and the state to unfreeze,
+   by computing the longest common suffixes *)
+let factorize_grams l1 l2 =
+  if l1 == l2 then ([], [], l1) else List.share_tails l1 l2
+
+let number_of_entries gcl =
+  List.fold_left (fun n (p,_,_) -> n + p) 0 gcl
+
+let unfreeze (grams, lex) =
+  let (undo, redo, common) = factorize_grams !grammar_stack grams in
+  let n = number_of_entries undo in
+  remove_grammars n;
+  grammar_stack := common;
+  CLexer.unfreeze lex;
+  List.iter extend_dyn_grammar (List.rev_map pi2 redo)
+
+(** No need to provide an init function : the grammar state is
+    statically available, and already empty initially, while
+    the lexer state should not be resetted, since it contains
+    keywords declared in g_*.ml4 *)
+
+let _ =
+  Summary.declare_summary "GRAMMAR_LEXER"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = Summary.nop }
+
+let with_grammar_rule_protection f x =
+  let fs = freeze false in
+  try let a = f x in unfreeze fs; a
+  with reraise ->
+    let reraise = Errors.push reraise in
+    let () = unfreeze fs in
+    iraise reraise
 
 (** Registering grammar of generic arguments *)