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.

8 files changed, 613 insertions, 799 deletions

diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 310a44149a..2b67693d28 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -21,17 +21,11 @@ end
 exception Exc_located = Ploc.Exc
 
 IFDEF CAMLP5_6_00 THEN
-let ploc_make_loc fname lnb pos bpep = Ploc.make_loc fname lnb pos bpep ""
 let ploc_file_name = Ploc.file_name
 ELSE
-let ploc_make_loc fname lnb pos bpep = Ploc.make lnb pos bpep
 let ploc_file_name _ = ""
 END
 
-let of_coqloc loc =
-  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
-  ploc_make_loc fname lnb pos (bp,ep)
-
 let to_coqloc loc =
   Loc.create (ploc_file_name loc) (Ploc.line_nb loc)
     (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc)
@@ -44,10 +38,6 @@ module CompatLoc = Camlp4.PreCast.Loc
 
 exception Exc_located = CompatLoc.Exc_located
 
-let of_coqloc loc =
-  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
-  CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false)
-
 let to_coqloc loc =
   Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc)
     (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc)
@@ -65,6 +55,7 @@ IFDEF CAMLP5 THEN
 
 module PcamlSig = struct end
 module Token = Token
+module CompatGramext = struct include Gramext type assoc = g_assoc end
 
 ELSE
 
@@ -73,68 +64,10 @@ module Ast = Camlp4.PreCast.Ast
 module Pcaml = Camlp4.PreCast.Syntax
 module MLast = Ast
 module Token = struct exception Error of string end
+module CompatGramext = Camlp4.Sig.Grammar
 
 END
 
-
-(** Grammar auxiliary types *)
-
-IFDEF CAMLP5 THEN
-
-let to_coq_assoc = function
-| Gramext.RightA -> Extend.RightA
-| Gramext.LeftA -> Extend.LeftA
-| Gramext.NonA -> Extend.NonA
-
-let of_coq_assoc = function
-| Extend.RightA -> Gramext.RightA
-| Extend.LeftA -> Gramext.LeftA
-| Extend.NonA -> Gramext.NonA
-
-let of_coq_position = function
-| Extend.First -> Gramext.First
-| Extend.Last -> Gramext.Last
-| Extend.Before s -> Gramext.Before s
-| Extend.After s -> Gramext.After s
-| Extend.Level s -> Gramext.Level s
-
-let to_coq_position = function
-| Gramext.First -> Extend.First
-| Gramext.Last -> Extend.Last
-| Gramext.Before s -> Extend.Before s
-| Gramext.After s -> Extend.After s
-| Gramext.Level s -> Extend.Level s
-| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *)
-
-ELSE
-
-let to_coq_assoc = function
-| PcamlSig.Grammar.RightA -> Extend.RightA
-| PcamlSig.Grammar.LeftA -> Extend.LeftA
-| PcamlSig.Grammar.NonA -> Extend.NonA
-
-let of_coq_assoc = function
-| Extend.RightA -> PcamlSig.Grammar.RightA
-| Extend.LeftA -> PcamlSig.Grammar.LeftA
-| Extend.NonA -> PcamlSig.Grammar.NonA
-
-let of_coq_position = function
-| Extend.First -> PcamlSig.Grammar.First
-| Extend.Last -> PcamlSig.Grammar.Last
-| Extend.Before s -> PcamlSig.Grammar.Before s
-| Extend.After s -> PcamlSig.Grammar.After s
-| Extend.Level s -> PcamlSig.Grammar.Level s
-
-let to_coq_position = function
-| PcamlSig.Grammar.First -> Extend.First
-| PcamlSig.Grammar.Last -> Extend.Last
-| PcamlSig.Grammar.Before s -> Extend.Before s
-| PcamlSig.Grammar.After s -> Extend.After s
-| PcamlSig.Grammar.Level s -> Extend.Level s
-
-END
-
-
 (** Signature of CLexer *)
 
 IFDEF CAMLP5 THEN
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index eff666c9c4..21a9afa293 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
 open Errors
 open Util
 open Pcoq
@@ -16,6 +15,136 @@ open Notation_term
 open Libnames
 open Names
 
+(**********************************************************************)
+(* 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 default_constr_levels = (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 open Pp in
+  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)
+
+type gram_level =
+  gram_position option * gram_assoc option * string option *
+  (** for reinitialization: *) gram_reinit option
+
+let find_position_gen current ensure assoc lev =
+  match lev with
+  | None ->
+      current, (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 = add_level None current in
+	let assoc = create_assoc assoc in
+        begin match !init with
+        | None ->
+	  (* Create the entry *)
+	   updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
+        | _ ->
+	  (* The reinit flag has been updated *)
+	   updated, (Some (Extend.Level (constr_level n)), None, None, !init)
+        end
+      with
+	  (* Nothing has changed *)
+          Exit ->
+	    (* Just inherit the existing associativity and name (None) *)
+	    current, (Some (Extend.Level (constr_level n)), None, None, None)
+
+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 accu forpat levels =
+  let rec filter accu = function
+  | [] -> ([], accu)
+  | n :: rem ->
+    let rem, accu = filter accu rem in
+    let (clev, plev) = accu in
+    let levels = if forpat then plev else clev in
+    if not (list_mem_assoc_triple n levels) then
+      let nlev, ans = find_position_gen levels true None (Some n) in
+      let nlev = if forpat then (clev, nlev) else (nlev, plev) in
+      ans :: rem, nlev
+    else rem, accu
+  in
+  filter accu levels
+
+let find_position accu forpat assoc level =
+  let (clev, plev) = accu in
+  let levels = if forpat then plev else clev in
+  let nlev, ans = find_position_gen levels false assoc level in
+  let nlev = if forpat then (clev, nlev) else (nlev, plev) in
+  (ans, nlev)
+
 (**************************************************************************)
 (*
  * --- Note on the mapping of grammar productions to camlp4 actions ---
@@ -43,6 +172,146 @@ open Names
 (**********************************************************************)
 (** Declare Notations grammar rules                                   *)
 
+(**********************************************************************)
+(* 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 NonA | Some RightA -> RightA
+  | None | Some LeftA -> LeftA
+
+let assoc_eq al ar = match al, ar with
+| NonA, NonA
+| RightA, RightA
+| LeftA, 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 (NonA|LeftA))) ->
+      Some None
+  (* If RightA on the right-hand side, set to the explicit (current) level *)
+  | (NumLevel n,BorderProd (Right,Some 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 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
+    | LeftA -> Some (Some (n, true))
+    | _ -> Some None
+    end
+  (* None means NEXT *)
+  | (NextLevel,_) -> Some None
+(* Compute production name elsewhere *)
+  | (NumLevel n,InternalProd) ->
+    if from = n + 1 then Some None else Some (Some (n, Int.equal n from))
+
+type _ target =
+| ForConstr : constr_expr target
+| ForPattern : cases_pattern_expr target
+
+type prod_info = production_level * production_position
+
+type (_, _) entry =
+| TTName : ('self, Name.t Loc.located) entry
+| TTReference : ('self, reference) entry
+| TTBigint : ('self, Bigint.bigint) entry
+| TTBinder : ('self, local_binder list) entry
+| TTConstr : prod_info * 'r target -> ('r, 'r) entry
+| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
+| TTBinderListT : ('self, local_binder list) entry
+| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry
+
+type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
+
+(* This computes the name of the level where to add a new rule *)
+let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option =
+  fun forpat level -> match forpat with
+  | ForConstr ->
+    if level = 200 then Constr.binder_constr, None
+    else Constr.operconstr, Some level
+  | ForPattern -> Constr.pattern, Some level
+
+let target_entry : type s. s target -> s Gram.entry = function
+| ForConstr -> Constr.operconstr
+| ForPattern -> Constr.pattern
+
+let is_self from e = match e with
+| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false
+| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n
+| _ -> false
+
+let is_binder_level from e = match e with
+| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200
+| _ -> false
+
+let make_sep_rules tkl =
+  let rec mkrule : Tok.t list -> unit rules = function
+  | [] -> Rules ({ norec_rule = Stop }, ignore)
+  | tkn :: rem ->
+    let Rules ({ norec_rule = r }, f) = mkrule rem in
+    let r = { norec_rule = Next (r, Atoken tkn) } in
+    Rules (r, fun _ -> f)
+  in
+  let r = mkrule (List.rev tkl) in
+  Arules [r]
+
+let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat ->
+  if is_binder_level from p then Aentryl (target_entry forpat, 200)
+  else if is_self from p then Aself
+  else
+    let g = target_entry forpat in
+    let lev = adjust_level assoc from p in
+    begin match lev with
+    | None -> Aentry g
+    | Some None -> Anext
+    | Some (Some (lev, cur)) -> Aentryl (g, lev)
+    end
+
+let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
+| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat
+| TTConstrList (typ', [], forpat) ->
+  Alist1 (symbol_of_target typ' assoc from forpat)
+| TTConstrList (typ', tkl, forpat) ->
+  Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
+| TTBinderListF [] -> Alist1 (Aentry Constr.binder)
+| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
+| TTName -> Aentry Prim.name
+| TTBinder -> Aentry Constr.binder
+| TTBinderListT -> Aentry Constr.open_binders
+| TTBigint -> Aentry Prim.bigint
+| TTReference -> Aentry Constr.global
+
+let interp_entry forpat e = match e with
+| ETName -> TTAny TTName
+| ETReference -> TTAny TTReference
+| ETBigint -> TTAny TTBigint
+| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList")
+| ETBinder false  -> TTAny TTBinder
+| ETConstr p -> TTAny (TTConstr (p, forpat))
+| ETPattern -> assert false (** not used *)
+| ETOther _ -> assert false (** not used *)
+| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETBinderList (true, []) -> TTAny TTBinderListT
+| ETBinderList (true, _) -> assert false
+| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl)
+
 let constr_expr_of_name (loc,na) = match na with
   | Anonymous -> CHole (loc,None,Misctypes.IntroAnonymous,None)
   | Name id -> CRef (Ident (loc,id), None)
@@ -58,140 +327,122 @@ type grammar_constr_prod_item =
     (* tells action rule to make a list of the n previous parsed items;
        concat with last parsed list if true *)
 
-let make_constr_action
-  (f : Loc.t -> constr_notation_substitution -> constr_expr) pil =
-  let rec make (constrs,constrlists,binders as fullsubst) = function
-  | [] ->
-      Gram.action (fun (loc:CompatLoc.t) -> f (!@loc) fullsubst)
-  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
-      (* parse a non-binding item *)
-      Gram.action (fun _ -> make fullsubst tl)
-  | GramConstrNonTerminal (typ, Some _) :: tl ->
-      (* parse a binding non-terminal *)
-    (match typ with
-    | (ETConstr _| ETOther _) ->
-	Gram.action (fun (v:constr_expr) ->
-	  make (v :: constrs, constrlists, binders) tl)
-    | ETReference ->
-        Gram.action (fun (v:reference) ->
-	  make (CRef (v,None) :: constrs, constrlists, binders) tl)
-    | ETName ->
-        Gram.action (fun (na:Loc.t * Name.t) ->
-	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
-    | ETBigint ->
-        Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPrim(Loc.ghost,Numeral v) :: constrs, constrlists, binders) tl)
-    | ETConstrList (_,n) ->
-	Gram.action (fun (v:constr_expr list) ->
-	  make (constrs, v::constrlists, binders) tl)
-    | ETBinder _ | ETBinderList (true,_) ->
-	Gram.action (fun (v:local_binder list) ->
-	  make (constrs, constrlists, v::binders) tl)
-    | ETBinderList (false,_) ->
-	Gram.action (fun (v:local_binder list list) ->
-	  make (constrs, constrlists, List.flatten v::binders) tl)
-    | ETPattern ->
-	failwith "Unexpected entry of type cases pattern")
-  | GramConstrListMark (n,b) :: tl ->
-      (* Rebuild expansions of ConstrList *)
-      let heads,constrs = List.chop n constrs in
-      let constrlists =
-	if b then (heads@List.hd constrlists)::List.tl constrlists
-	else heads::constrlists
-      in make (constrs, constrlists, binders) tl
-  in
-  make ([],[],[]) (List.rev pil)
-
-let check_cases_pattern_env loc (env,envlist,hasbinders) =
-  if hasbinders then Topconstr.error_invalid_pattern_notation loc
-  else (env,envlist)
-
-let make_cases_pattern_action
-  (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
-  let rec make (env,envlist,hasbinders as fullenv) = function
-  | [] ->
-      Gram.action
-	(fun (loc:CompatLoc.t) ->
-	  let loc = !@loc in
-	  f loc (check_cases_pattern_env loc fullenv))
-  | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
-      (* parse a non-binding item *)
-      Gram.action (fun _ -> make fullenv tl)
-  | GramConstrNonTerminal (typ, Some _) :: tl ->
-      (* parse a binding non-terminal *)
-    (match typ with
-    | ETConstr _ -> (* pattern non-terminal *)
-        Gram.action (fun (v:cases_pattern_expr) ->
-          make (v::env, envlist, hasbinders) tl)
-    | ETReference ->
-        Gram.action (fun (v:reference) ->
-	  make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl)
-    | ETName ->
-        Gram.action (fun (na:Loc.t * Name.t) ->
-	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
-    | ETBigint ->
-        Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (Loc.ghost,Numeral v) :: env, envlist, hasbinders) tl)
-    | ETConstrList (_,_) ->
-        Gram.action  (fun (vl:cases_pattern_expr list) ->
-	  make (env, vl :: envlist, hasbinders) tl)
-    | ETBinder _ | ETBinderList (true,_) ->
-	Gram.action (fun (v:local_binder list) ->
-	  make (env, envlist, hasbinders) tl)
-    | ETBinderList (false,_) ->
-	Gram.action (fun (v:local_binder list list) ->
-	  make (env, envlist, true) tl)
-    | (ETPattern | ETOther _) ->
-        anomaly (Pp.str "Unexpected entry of type cases pattern or other"))
-  | GramConstrListMark (n,b) :: tl ->
-      (* Rebuild expansions of ConstrList *)
-      let heads,env = List.chop n env in
-      if b then
-        make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
-      else
-        make (env,heads::envlist,hasbinders) tl
+type 'r env = {
+  constrs : 'r list;
+  constrlists : 'r list list;
+  binders : (local_binder list * bool) list;
+}
+
+let push_constr subst v = { subst with constrs = v :: subst.constrs }
+
+let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v ->
+match e with
+| TTConstr _ -> push_constr subst v
+| TTName ->
+  begin match forpat with
+  | ForConstr -> push_constr subst (constr_expr_of_name v)
+  | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
+  end
+| TTBinder -> { subst with binders = (v, true) :: subst.binders }
+| TTBinderListT -> { subst with binders = (v, true) :: subst.binders }
+| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
+| TTBigint ->
+  begin match forpat with
+  | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v))
+  | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v))
+  end
+| TTReference ->
+  begin match forpat with
+  | ForConstr -> push_constr subst (CRef (v, None))
+  | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v))
+  end
+| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
+
+type (_, _) ty_symbol =
+| TyTerm : Tok.t -> ('s, string) ty_symbol
+| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol
+
+type ('self, _, 'r) ty_rule =
+| TyStop : ('self, 'r, 'r) ty_rule
+| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule
+| TyMark : int * bool * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule
+
+type 'r gen_eval = Loc.t -> 'r env -> 'r
+
+let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> a = function
+| TyStop ->
+  fun f env loc -> f loc env
+| TyNext (rem, TyTerm _) ->
+  fun f env _ -> ty_eval rem f env
+| TyNext (rem, TyNonTerm (_, _, _, false)) ->
+  fun f env _ -> ty_eval rem f env
+| TyNext (rem, TyNonTerm (forpat, e, _, true)) ->
+  fun f env v ->
+    ty_eval rem f (push_item forpat e env v)
+| TyMark (n, b, rem) ->
+  fun f env ->
+    let heads, constrs = List.chop n env.constrs in
+    let constrlists =
+      if b then (heads @ List.hd env.constrlists) :: List.tl env.constrlists
+      else heads :: env.constrlists
+    in
+    ty_eval rem f { env with constrs; constrlists; } 
+
+let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
+| TyStop -> Stop
+| TyMark (_, _, r) -> ty_erase r
+| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok)
+| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s)
+
+type ('self, 'r) any_ty_rule =
+| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
+
+let make_ty_rule assoc from forpat prods =
+  let rec make_ty_rule = function
+  | [] -> AnyTyRule TyStop
+  | GramConstrTerminal tok :: rem ->
+    let AnyTyRule r = make_ty_rule rem in
+    AnyTyRule (TyNext (r, TyTerm tok))
+  | GramConstrNonTerminal (e, var) :: rem ->
+    let AnyTyRule r = make_ty_rule rem in
+    let TTAny e = interp_entry forpat e in
+    let s = symbol_of_entry assoc from e in
+    let bind = match var with None -> false | Some _ -> true in
+    AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind)))
+  | GramConstrListMark (n, b) :: rem ->
+    let AnyTyRule r = make_ty_rule rem in
+    AnyTyRule (TyMark (n, b, r))
   in
-  make ([],[],false) (List.rev pil)
-
-let rec make_constr_prod_item assoc from forpat = function
-  | GramConstrTerminal tok :: l ->
-      gram_token_of_token tok :: make_constr_prod_item assoc from forpat l
-  | GramConstrNonTerminal (nt, ovar) :: l ->
-      symbol_of_constr_prod_entry_key assoc from forpat nt
-      :: make_constr_prod_item assoc from forpat l
-  | GramConstrListMark _ :: l ->
-      make_constr_prod_item assoc from forpat l
-  | [] ->
-      []
+  make_ty_rule (List.rev prods)
+
+let target_to_bool : type r. r target -> bool = function
+| ForConstr -> false
+| ForPattern -> true
 
 let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
   let empty = (pos, [(name, p4assoc, [])]) in
-  if forpat then grammar_extend Constr.pattern reinit empty
-  else grammar_extend Constr.operconstr reinit empty
-
-let pure_sublevels level symbs =
-  let filter s =
-    try
-      let i = level_of_snterml s in
-      begin match level with
-      | Some j when Int.equal i j -> None
-      | _ -> Some i
-      end
-    with Failure _ -> None
-  in
-  List.map_filter filter symbs
-
-let extend_constr (entry,level) (n,assoc) mkact forpat rules =
-  List.fold_left (fun nb pt ->
-  let symbs = make_constr_prod_item assoc n forpat pt in
-  let pure_sublevels = pure_sublevels level symbs in
-  let needed_levels = register_empty_levels forpat pure_sublevels in
-  let pos,p4assoc,name,reinit = find_position forpat assoc level in
-  let nb_decls = List.length needed_levels + 1 in
-  List.iter (prepare_empty_levels forpat) needed_levels;
-  unsafe_grammar_extend entry reinit (Option.map of_coq_position pos,
-    [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]);
-  nb_decls) 0 rules
+  if forpat then ExtendRule (Constr.pattern, reinit, empty)
+  else ExtendRule (Constr.operconstr, reinit, empty)
+
+let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with
+| Stop -> []
+| Next (rem, Aentryl (_, i)) ->
+  let rem = pure_sublevels level rem in
+  begin match level with
+  | Some j when Int.equal i j -> rem
+  | _ -> i :: rem
+  end
+| Next (rem, _) -> pure_sublevels level rem
+
+let make_act : type r. r target -> _ -> r gen_eval = function
+| ForConstr -> fun notation loc env ->
+  let env = (env.constrs, env.constrlists, List.map fst env.binders) in
+  CNotation (loc, notation , env)
+| ForPattern -> fun notation loc env ->
+  let invalid = List.exists (fun (_, b) -> not b) env.binders in
+  let () = if invalid then Topconstr.error_invalid_pattern_notation loc in
+  let env = (env.constrs, env.constrlists) in
+  CPatNotation (loc, notation, env, [])
 
 type notation_grammar = {
   notgram_level : int;
@@ -201,106 +452,51 @@ type notation_grammar = {
   notgram_typs : notation_var_internalization_type list;
 }
 
-let extend_constr_constr_notation ng =
-  let level = ng.notgram_level in
-  let mkact loc env = CNotation (loc, ng.notgram_notation, env) in
-  let e = interp_constr_entry_key false level in
-  let ext = (ETConstr (level, ()), ng.notgram_assoc) in
-  extend_constr e ext (make_constr_action mkact) false ng.notgram_prods
-
-let extend_constr_pat_notation ng =
-  let level = ng.notgram_level in
-  let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in
-  let e = interp_constr_entry_key true level in
-  let ext = ETConstr (level, ()), ng.notgram_assoc in
-  extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
-
-let extend_constr_notation (_, ng) =
-  (* Add the notation in constr *)
-  let nb = extend_constr_constr_notation ng in
-  (* Add the notation in cases_pattern *)
-  let nb' = extend_constr_pat_notation ng in
-  nb + nb'
-
-module GrammarCommand = Dyn.Make(struct end)
-module GrammarInterp = struct type 'a t = 'a -> int end
-module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
-
-let grammar_interp = ref GrammarInterpMap.empty
-
-let (grammar_state : (int * GrammarCommand.t) list ref) = ref []
-
-type 'a grammar_command = 'a GrammarCommand.tag
-
-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 extend_constr state forpat ng =
+  let n = ng.notgram_level in
+  let assoc = ng.notgram_assoc in
+  let (entry, level) = interp_constr_entry_key forpat n in
+  let fold (accu, state) pt =
+    let AnyTyRule r = make_ty_rule assoc n forpat pt in
+    let symbs = ty_erase r in
+    let pure_sublevels = pure_sublevels level symbs in
+    let isforpat = target_to_bool forpat in
+    let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
+    let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
+    let nb_decls = List.length needed_levels + 1 in
+    let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
+    let empty = { constrs = []; constrlists = []; binders = [] } in
+    let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
+    let rule = (name, p4assoc, [Rule (symbs, act)]) in
+    let r = ExtendRule (entry, reinit, (pos, [rule])) in
+    (accu @ empty_rules @ [r], state)
+  in
+  List.fold_left fold ([], state) ng.notgram_prods
 
-let extend_grammar tag g =
-  let nb = GrammarInterpMap.find tag !grammar_interp g in
-  grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
+let constr_levels = GramState.field ()
 
-let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
+let extend_constr_notation (_, ng) state =
+  let levels = match GramState.get state constr_levels with
+  | None -> default_constr_levels
+  | Some lev -> lev
+  in
+  (* Add the notation in constr *)
+  let (r, levels) = extend_constr levels ForConstr ng in
+  (* Add the notation in cases_pattern *)
+  let (r', levels) = extend_constr levels ForPattern ng in
+  let state = GramState.set state constr_levels levels in
+  (r @ r', state)
 
-let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag =
+let constr_grammar : (Notation.level * notation_grammar) grammar_command =
   create_grammar_command "Notation" extend_constr_notation
 
-let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn)
+let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn)
 
 let recover_constr_grammar ntn prec =
-  let filter (_, gram) : notation_grammar option = match gram with
-  | GrammarCommand.Dyn (tag, obj) ->
-    match GrammarCommand.eq tag constr_grammar with
-    | None -> None
-    | Some Refl ->
-      let (prec', ng) = obj in
-      if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
-      else None
+  let filter (prec', ng) =
+    if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
+    else None
   in
-  match List.map_filter filter !grammar_state with
+  match List.map_filter filter (recover_grammar_command constr_grammar) with
   | [x] -> x
   | _ -> assert false
-
-(* 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) list * CLexer.frozen_t
-
-let freeze _ : frozen_t = (!grammar_state, 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_state grams in
-  let n = number_of_entries undo in
-  remove_grammars n;
-  remove_levels n;
-  grammar_state := common;
-  CLexer.unfreeze lex;
-  List.iter extend_dyn_grammar (List.rev_map snd 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
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 6ec1066260..1fe06a29df 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -36,20 +36,6 @@ type notation_grammar = {
   notgram_typs : notation_var_internalization_type list;
 }
 
-(** {5 Extending the parser with Summary-synchronized commands} *)
-
-type 'a grammar_command
-(** Type of synchronized parsing extensions. The ['a] type should be
-    marshallable. *)
-
-val create_grammar_command : string -> ('a -> int) -> 'a grammar_command
-(** Create a new grammar-modifying command with the given name. The function
-    should modify the parser state and return the number of grammar extensions
-    performed. *)
-
-val extend_grammar : 'a grammar_command -> 'a -> unit
-(** Extend the grammar of Coq with the given data. *)
-
 (** {5 Adding notations} *)
 
 val extend_constr_grammar : Notation.level -> notation_grammar -> unit
@@ -58,5 +44,3 @@ val extend_constr_grammar : Notation.level -> notation_grammar -> unit
 val recover_constr_grammar : notation -> Notation.level -> notation_grammar
 (** For a declared grammar, returns the rule + the ordered entry types
     of variables in the rule (for use in the interpretation) *)
-
-val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/entry.ml b/parsing/entry.ml
deleted file mode 100644
index b7c6c23fa6..0000000000
--- a/parsing/entry.ml
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Errors
-open Util
-
-type 'a t = string
-
-(** Entries are registered with a unique name *)
-
-let entries = ref String.Set.empty
-
-let create name =
-  let () =
-    if String.Set.mem name !entries then
-    anomaly (Pp.str ("Entry " ^ name ^ " already defined"))
-  in
-  let () = entries := String.Set.add name !entries in
-  name
-
-let unsafe_of_name name =
-  assert (String.Set.mem name !entries);
-  name
-
-let repr s = s
diff --git a/parsing/entry.mli b/parsing/entry.mli
deleted file mode 100644
index 4c73fe2049..0000000000
--- a/parsing/entry.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Typed grammar entries *)
-
-type 'a t
-(** Typed grammar entries. We need to defined them here so that they are
-    marshallable and defined before the Pcoq.Gram module. They are basically
-    unique names. They should be kept synchronized with the {!Pcoq} entries. *)
-
-val create : string -> 'a t
-(** Create an entry. They should be synchronized with the entries defined in
-    {!Pcoq}. *)
-
-(** {5 Meta-programming} *)
-
-val repr : 'a t -> string
-val unsafe_of_name : string -> 'a t
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index b052b6ee6d..0e1c79c91b 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,7 +1,6 @@
 Tok
 Compat
 CLexer
-Entry
 Pcoq
 Egramml
 Egramcoq
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 *)
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d320520015..319ca256e1 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -19,7 +19,7 @@ open Genredexpr
 
 (** The parser of Coq *)
 
-module Gram : Compat.GrammarSig
+module Gram : module type of Compat.GrammarMake(CLexer)
 
 (** The parser of Coq is built from three kinds of rule declarations:
 
@@ -96,36 +96,6 @@ module Gram : Compat.GrammarSig
 
 *)
 
-val gram_token_of_token : Tok.t -> Gram.symbol
-val gram_token_of_string : string -> Gram.symbol
-
-(** The superclass of all grammar entries *)
-type grammar_object
-
-(** Type of reinitialization data *)
-type gram_reinit = gram_assoc * gram_position
-
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-(** Add one extension at some camlp4 position of some camlp4 entry *)
-val unsafe_grammar_extend :
-  grammar_object Gram.entry ->
-  gram_reinit option (** for reinitialization if ever needed *) ->
-  Gram.extend_statment -> unit
-
-val grammar_extend :
-  'a Gram.entry ->
-  gram_reinit option (** for reinitialization if ever needed *) ->
-  'a Extend.extend_statment -> unit
-
-(** Remove the last n extensions *)
-val remove_grammars : int -> unit
-
 (** Temporary activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
@@ -145,7 +115,6 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
-val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
 
@@ -251,40 +220,45 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry
 val get_command_entry : unit -> vernac_expr Gram.entry
 val set_command_entry : vernac_expr Gram.entry -> unit
 
-(** Mapping formal entries into concrete ones *)
-
-(** Binding constr entry keys to entries and symbols *)
+val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
-val interp_constr_entry_key : bool (** true for cases_pattern *) ->
-  int -> grammar_object Gram.entry * int option
+(** {5 Extending the parser without synchronization} *)
 
-val symbol_of_constr_prod_entry_key : gram_assoc option ->
-  constr_entry_key -> bool -> constr_prod_entry_key ->
-    Gram.symbol
+type gram_reinit = gram_assoc * gram_position
+(** Type of reinitialization data *)
 
-val name_of_entry : 'a Gram.entry -> 'a Entry.t
+val grammar_extend : 'a Gram.entry -> gram_reinit option ->
+  'a Extend.extend_statment -> unit
+(** Extend the grammar of Coq, without synchronizing it with the bactracking
+    mechanism. This means that grammar extensions defined this way will survive
+    an undo. *)
 
-val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
+(** {5 Extending the parser with summary-synchronized commands} *)
 
-(** Binding general entry keys to symbols *)
+module GramState : Store.S
+(** Auxilliary state of the grammar. Any added data must be marshallable. *)
 
-(** Recover the list of all known tactic notation entries. *)
-val list_entry_names : unit -> (string * argument_type) list
+type 'a grammar_command
+(** Type of synchronized parsing extensions. The ['a] type should be
+    marshallable. *)
 
-(** Registering/resetting the level of a constr entry *)
+type extend_rule =
+| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule
 
-val find_position :
-  bool (** true if for creation in pattern entry; false if in constr entry *) ->
-  Extend.gram_assoc option -> int option ->
-    Extend.gram_position option * Extend.gram_assoc option * string option *
-    (** for reinitialization: *) gram_reinit option
+type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
+(** Grammar extension entry point. Given some ['a] and a current grammar state,
+    such a function must produce the list of grammar extensions that will be
+    applied in the same order and kept synchronized w.r.t. the summary, together
+    with a new state. It should be pure. *)
 
-val synchronize_level_positions : unit -> unit
+val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command
+(** Create a new grammar-modifying command with the given name. The extension
+    function is called to generate the rules for a given data. *)
 
-val register_empty_levels : bool -> int list ->
-    (Extend.gram_position option * Extend.gram_assoc option *
-     string option * gram_reinit option) list
+val extend_grammar_command : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
 
-val remove_levels : int -> unit
+val recover_grammar_command : 'a grammar_command -> 'a list
+(** Recover the current stack of grammar extensions. *)
 
-val level_of_snterml : Gram.symbol -> int
+val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b