From 4950a69874524dd6d79ca6a83b0c36d6dd1a3e45 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 14:36:36 +0200
Subject: Removing dead code in Compat.

---
 parsing/pcoq.ml | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6dcf76da8c..8c82725893 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -19,6 +19,18 @@ module G = GrammarMake (CLexer)
 
 let warning_verbose = Compat.warning_verbose
 
+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
+
 module Symbols = GramextMake(G)
 
 let gram_token_of_token = Symbols.stoken
@@ -86,8 +98,10 @@ 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,[]])
@@ -135,8 +149,7 @@ let rec remove_grammars n =
     (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;
+           grammar_delete g reinit ext;
            camlp4_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
-- 
cgit v1.2.3


From 9891f2321f13861e3f48ddb28abcd5a77be30791 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 15:48:11 +0200
Subject: Hardening the obsolete unsafe_grammar_statement API.

---
 parsing/pcoq.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8c82725893..70bcf1def3 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -135,7 +135,18 @@ module Gram =
 
 (** This extension command is used by the Grammar constr *)
 
-let unsafe_grammar_extend e reinit ext =
+type unsafe_single_extend_statment =
+  string option *
+  gram_assoc option *
+  Gram.production_rule list
+
+type unsafe_extend_statment =
+  gram_position option *
+  unsafe_single_extend_statment list
+
+let unsafe_grammar_extend e reinit (pos, st) =
+  let map_s (lvl, assoc, rule) = (lvl, Option.map of_coq_assoc assoc, rule) in
+  let ext =  (Option.map of_coq_position pos, List.map map_s st) in
   camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
   camlp4_verbose (maybe_uncurry (G.extend e)) ext
 
@@ -706,10 +717,10 @@ 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)
+  (lvl, 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)
+  (pos, List.map of_coq_single_extend_statement st)
 
 let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
-- 
cgit v1.2.3


From 6150d15647afc739329019f7e9de595187ecc282 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 16:08:50 +0200
Subject: Removing the Entry module now that rules need not be marshalled.

---
 parsing/pcoq.ml | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 70bcf1def3..a7f7ad7bca 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -215,18 +215,9 @@ let get_univ u =
 (** 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
@@ -689,10 +680,8 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | 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))
 
@@ -726,8 +715,6 @@ let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   unsafe_grammar_extend e reinit ext
 
-let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
-
 let list_entry_names () = []
 
 let epsilon_value f e =
-- 
cgit v1.2.3


From 53724bbcce87da0b1a9a71da4e5334d7a893ba49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 19:12:24 +0200
Subject: Purer implementation of empty level registering in Pcoq.

---
 parsing/pcoq.ml | 64 +++++++++++++++++++++++++++++++++++----------------------
 1 file changed, 39 insertions(+), 25 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index a7f7ad7bca..42eb8724af 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -423,9 +423,6 @@ let default_pattern_levels =
    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 *)
@@ -453,12 +450,10 @@ 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
+let find_position_gen current ensure assoc lev =
   match lev with
   | None ->
-      level_stack := current :: !level_stack;
-      None, None, None, None
+      current, (None, None, None, None)
   | Some n ->
       let after = ref None in
       let init = ref None in
@@ -475,25 +470,24 @@ let find_position_gen forpat ensure assoc lev =
 	| 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 updated = add_level None current in
 	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
+	   updated, (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
+	   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
+	    current, (Some (Extend.Level (constr_level n)), None, None, None)
+
+let level_stack =
+  ref [(default_levels, default_pattern_levels)]
 
 let remove_levels n =
   level_stack := List.skipn n !level_stack
@@ -502,23 +496,43 @@ let rec list_mem_assoc_triple x = function
   | [] -> false
   | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l
 
+type gram_level =
+  gram_position option * gram_assoc option * string option *
+  (** for reinitialization: *) gram_reinit option
+
+let top = function
+| [] -> assert false
+| h :: _ -> h
+
 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
+  let rec filter accu = function
+  | [] -> ([], accu)
+  | n :: rem ->
+    let rem, accu = filter accu rem in
+    let (clev, plev) = top 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 :: accu
+    else rem, accu
   in
-  List.map_filter filter levels
+  let ans, accu = filter !level_stack levels in
+  let () = level_stack := accu in
+  ans
 
 let find_position forpat assoc level =
-  find_position_gen forpat false assoc level
+  let (clev, plev) = top !level_stack 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
+  level_stack := nlev :: !level_stack;
+  ans
 
 (* Synchronise the stack of level updates *)
 let synchronize_level_positions () =
-  let _ = find_position true None None in ()
+  let lev = top !level_stack in
+  level_stack := lev :: !level_stack
 
 (**********************************************************************)
 (* Binding constr entry keys to entries                               *)
-- 
cgit v1.2.3


From 946a3d4a800ae1f459cb67cc15c9e6ec44fb3f94 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 May 2016 08:56:15 +0200
Subject: Simpler data structure for Arules token.

---
 parsing/pcoq.ml | 25 +++++++++----------------
 1 file changed, 9 insertions(+), 16 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 42eb8724af..b06362dc38 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -675,12 +675,9 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
 
 (** 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 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))
 
 let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Atoken t -> Symbols.stoken t
@@ -697,25 +694,21 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
     Symbols.snterm (Gram.Entry.obj (weaken_entry e))
   | Aentryl (e, n) ->
     Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
-  | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x))
+  | Arules rs ->
+    Gram.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
-| 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))
+| 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 level_of_snterml e = int_of_string (Symbols.snterml_level e)
 
-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))
-
 let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
 | Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
 
-- 
cgit v1.2.3


From 61f79019be6082c3ebabd503c322fb2edb05a99a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 May 2016 11:11:39 +0200
Subject: AlistNsep token now accepts an arbitrary separator.

---
 parsing/pcoq.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b06362dc38..2790063e67 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -683,10 +683,10 @@ 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)
+      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, gram_token_of_string 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
-- 
cgit v1.2.3


From 810afe7c16ca2d18ac7fb39b1d3bd1a3db1c1331 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 May 2016 09:59:41 +0200
Subject: Type-safe constr notations.

This removes the last call to unsafe_grammar_extend, so that all handwritten
grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are
still using the unsafe interface, but as they insert explicit casts they are
deemed safe.
---
 parsing/pcoq.ml | 156 --------------------------------------------------------
 1 file changed, 156 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 2790063e67..8fa5da4bd9 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -33,9 +33,6 @@ let of_coq_position = function
 
 module Symbols = GramextMake(G)
 
-let gram_token_of_token = Symbols.stoken
-let gram_token_of_string s = gram_token_of_token (CLexer.terminal s)
-
 let camlp4_verbosity silent f x =
   let a = !warning_verbose in
   warning_verbose := silent;
@@ -135,15 +132,6 @@ module Gram =
 
 (** This extension command is used by the Grammar constr *)
 
-type unsafe_single_extend_statment =
-  string option *
-  gram_assoc option *
-  Gram.production_rule list
-
-type unsafe_extend_statment =
-  gram_position option *
-  unsafe_single_extend_statment list
-
 let unsafe_grammar_extend e reinit (pos, st) =
   let map_s (lvl, assoc, rule) = (lvl, Option.map of_coq_assoc assoc, rule) in
   let ext =  (Option.map of_coq_position pos, List.map map_s st) in
@@ -212,9 +200,6 @@ 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 new_entry u s =
   let ename = u ^ ":" ^ s in
   let e = Gram.entry_create ename in
@@ -534,145 +519,6 @@ let synchronize_level_positions () =
   let lev = top !level_stack in
   level_stack := lev :: !level_stack
 
-(**********************************************************************)
-(* 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 rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function
@@ -707,8 +553,6 @@ and symbol_of_rules : type a. a Extend.rules -> _ = function
   let act = of_coq_action r.norec_rule act in
   (symb, act)
 
-let level_of_snterml e = int_of_string (Symbols.snterml_level e)
-
 let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
 | Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
 
-- 
cgit v1.2.3


From bc3981687cd363820e35e5a2bd037d50e213f524 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 May 2016 19:42:39 +0200
Subject: Overlooked use of Gram instead of G module in Pcoq.

This was probably wreaking havoc in tricky undo-redo scenarii.
---
 parsing/pcoq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8fa5da4bd9..305cd4f80f 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -572,7 +572,7 @@ 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
+  let () = maybe_uncurry (G.extend entry) ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Registering grammar of generic arguments *)
-- 
cgit v1.2.3


From f2983cec3544473b18ebc4d4e3a20b941decd196 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 May 2016 19:46:39 +0200
Subject: Delimiting the use of unsafe code in Pcoq.

---
 parsing/pcoq.ml | 133 ++++++++++++++++++++++----------------------------------
 1 file changed, 52 insertions(+), 81 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 305cd4f80f..631c5325dc 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -41,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 =
@@ -72,20 +52,68 @@ 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 ext_kind =
-  | ByGrammar of
-      grammar_object G.entry
+  | ByGrammar :
+      'a G.entry
       * gram_reinit option (** for reinitialization if ever needed *)
-      * G.extend_statment
+      * 'a Extend.extend_statment -> ext_kind
   | ByEXTEND of (unit -> unit) * (unit -> unit)
 
 (** The list of extensions *)
 
 let camlp4_state = ref []
 
+let grammar_extend e reinit ext =
+  camlp4_state := ByGrammar (e,reinit,ext) :: !camlp4_state;
+  let ext = of_coq_extend_statement ext in
+  camlp4_verbose (maybe_uncurry (G.extend e)) ext
+
 (** Deletion *)
 
 let grammar_delete e reinit (pos,rls) =
@@ -130,14 +158,6 @@ module Gram =
       G.delete_rule e pil
   end
 
-(** This extension command is used by the Grammar constr *)
-
-let unsafe_grammar_extend e reinit (pos, st) =
-  let map_s (lvl, assoc, rule) = (lvl, Option.map of_coq_assoc assoc, rule) in
-  let ext =  (Option.map of_coq_position pos, List.map map_s st) in
-  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!)
@@ -148,7 +168,7 @@ let rec remove_grammars n =
     (match !camlp4_state with
        | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove")
        | ByGrammar(g,reinit,ext)::t ->
-           grammar_delete g reinit ext;
+           grammar_delete g reinit (of_coq_extend_statement ext);
            camlp4_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
@@ -519,55 +539,6 @@ let synchronize_level_positions () =
   let lev = top !level_stack in
   level_stack := lev :: !level_stack
 
-(** Binding general entry keys to symbol *)
-
-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))
-
-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 (Gram.Entry.obj (weaken_entry e))
-  | Aentryl (e, n) ->
-    Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
-  | Arules rs ->
-    Gram.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, assoc, List.map of_coq_production_rule rule)
-
-let of_coq_extend_statement (pos, st) =
-  (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 list_entry_names () = []
-
 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
-- 
cgit v1.2.3


From 17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 10:30:49 +0200
Subject: Moving the grammar summary to Pcoq.

---
 parsing/pcoq.ml | 74 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 631c5325dc..de57feb7f3 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -546,6 +546,80 @@ let epsilon_value f e =
   let () = maybe_uncurry (G.extend entry) ext in
   try Some (parse_string entry "") with _ -> None
 
+(** Synchronized grammar extensions *)
+
+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_grammar_command tag g =
+  let nb = GrammarInterpMap.find tag !grammar_interp g in
+  grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
+
+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_state
+
+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) 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
+
 (** Registering grammar of generic arguments *)
 
 let () =
-- 
cgit v1.2.3


From df2d71323081f8a395881ffc0e1793e429abc3bb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 11:28:04 +0200
Subject: Turning the grammar extend command API into a state-passing one.

---
 parsing/pcoq.ml | 33 +++++++++++++++++++++------------
 1 file changed, 21 insertions(+), 12 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index de57feb7f3..efb52dc233 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -548,13 +548,17 @@ let epsilon_value f e =
 
 (** Synchronized grammar extensions *)
 
+module GramState = Store.Make(struct end)
+
+type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t
+
 module GrammarCommand = Dyn.Make(struct end)
-module GrammarInterp = struct type 'a t = 'a -> int end
+module GrammarInterp = struct type 'a t = 'a grammar_extension end
 module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
 
 let grammar_interp = ref GrammarInterpMap.empty
 
-let (grammar_state : (int * GrammarCommand.t) list ref) = ref []
+let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref []
 
 type 'a grammar_command = 'a GrammarCommand.tag
 
@@ -564,25 +568,30 @@ let create_grammar_command name interp : _ grammar_command =
   obj
 
 let extend_grammar_command tag g =
-  let nb = GrammarInterpMap.find tag !grammar_interp g in
-  grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
+  let modify = GrammarInterpMap.find tag !grammar_interp in
+  let grammar_state = match !grammar_stack with
+  | [] -> GramState.empty
+  | (_, _, st) :: _ -> st
+  in
+  let (nb, st) = modify g grammar_state 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)) ->
+  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_state
+  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) list * CLexer.frozen_t
+type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t
 
-let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ())
+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 *)
@@ -590,16 +599,16 @@ 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
+  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 (undo, redo, common) = factorize_grams !grammar_stack grams in
   let n = number_of_entries undo in
   remove_grammars n;
   remove_levels n;
-  grammar_state := common;
+  grammar_stack := common;
   CLexer.unfreeze lex;
-  List.iter extend_dyn_grammar (List.rev_map snd redo)
+  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
-- 
cgit v1.2.3


From 85753a0bdb6183604a78232c4c32fd15f7a21a2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 13:25:02 +0200
Subject: Moving the constr empty entry registering to the state-based API.

---
 parsing/pcoq.ml | 146 --------------------------------------------------------
 1 file changed, 146 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index efb52dc233..1cc7b6c540 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -394,151 +394,6 @@ 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]
-
-(* 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 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 level_stack =
-  ref [(default_levels, default_pattern_levels)]
-
-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
-
-type gram_level =
-  gram_position option * gram_assoc option * string option *
-  (** for reinitialization: *) gram_reinit option
-
-let top = function
-| [] -> assert false
-| h :: _ -> h
-
-let register_empty_levels forpat levels =
-  let rec filter accu = function
-  | [] -> ([], accu)
-  | n :: rem ->
-    let rem, accu = filter accu rem in
-    let (clev, plev) = top 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 :: accu
-    else rem, accu
-  in
-  let ans, accu = filter !level_stack levels in
-  let () = level_stack := accu in
-  ans
-
-let find_position forpat assoc level =
-  let (clev, plev) = top !level_stack 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
-  level_stack := nlev :: !level_stack;
-  ans
-
-(* Synchronise the stack of level updates *)
-let synchronize_level_positions () =
-  let lev = top !level_stack in
-  level_stack := lev :: !level_stack
-
 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
@@ -605,7 +460,6 @@ let unfreeze (grams, lex) =
   let (undo, redo, common) = factorize_grams !grammar_stack grams in
   let n = number_of_entries undo in
   remove_grammars n;
-  remove_levels n;
   grammar_stack := common;
   CLexer.unfreeze lex;
   List.iter extend_dyn_grammar (List.rev_map pi2 redo)
-- 
cgit v1.2.3


From 16d0e6f7cfc453944874cc1665a0eb4db8ded354 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 15:33:47 +0200
Subject: Making the grammar command extend API purely functional.

Instead of leaving the responsibility of extending the grammar to the caller,
we ask for a list of extensions in the return value of the function.
---
 parsing/pcoq.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 1cc7b6c540..ae56c4723b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -98,11 +98,11 @@ let of_coq_extend_statement (pos, 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 :
-      'a G.entry
-      * gram_reinit option (** for reinitialization if ever needed *)
-      * 'a Extend.extend_statment -> ext_kind
+  | ByGrammar of extend_rule
   | ByEXTEND of (unit -> unit) * (unit -> unit)
 
 (** The list of extensions *)
@@ -110,7 +110,7 @@ type ext_kind =
 let camlp4_state = ref []
 
 let grammar_extend e reinit ext =
-  camlp4_state := ByGrammar (e,reinit,ext) :: !camlp4_state;
+  camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
   let ext = of_coq_extend_statement ext in
   camlp4_verbose (maybe_uncurry (G.extend e)) ext
 
@@ -167,7 +167,7 @@ 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 ->
+       | ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
            grammar_delete g reinit (of_coq_extend_statement ext);
            camlp4_state := t;
            remove_grammars (n-1)
@@ -405,7 +405,7 @@ let epsilon_value f e =
 
 module GramState = Store.Make(struct end)
 
-type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t
+type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 
 module GrammarCommand = Dyn.Make(struct end)
 module GrammarInterp = struct type 'a t = 'a grammar_extension end
@@ -428,7 +428,10 @@ let extend_grammar_command tag g =
   | [] -> GramState.empty
   | (_, _, st) :: _ -> st
   in
-  let (nb, st) = modify g grammar_state in
+  let (rules, st) = modify g grammar_state in
+  let iter (ExtendRule (e, reinit, ext)) = grammar_extend 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 =
-- 
cgit v1.2.3


From 9acfdfd9b7d1cae34b97a4c06c52c4646e15589b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 18:57:53 +0200
Subject: The grammar_extend function now registers unsynchronized extensions.

This made little sense, as all the uses of this function were actually
called from toplevel ML modules. This was at best useless, and at worst
a source of bugs when loading plugins and messing with backtracking.
---
 parsing/pcoq.ml | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

(limited to 'parsing/pcoq.ml')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index ae56c4723b..efb89cd6e1 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -109,11 +109,6 @@ type ext_kind =
 
 let camlp4_state = ref []
 
-let grammar_extend e reinit ext =
-  camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
-  let ext = of_coq_extend_statement ext in
-  camlp4_verbose (maybe_uncurry (G.extend e)) ext
-
 (** Deletion *)
 
 let grammar_delete e reinit (pos,rls) =
@@ -132,6 +127,19 @@ let grammar_delete e reinit (pos,rls) =
     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. *)
 
@@ -429,7 +437,7 @@ let extend_grammar_command tag g =
   | (_, _, st) :: _ -> st
   in
   let (rules, st) = modify g grammar_state in
-  let iter (ExtendRule (e, reinit, ext)) = grammar_extend e reinit ext 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
-- 
cgit v1.2.3