Turning the grammar extend command API into a state-passing one.

4 files changed, 31 insertions, 17 deletions

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 5c1e7c033..aedcb76eb 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -157,7 +157,7 @@ let rec prod_item_of_symbol lev = function
 
 (** Tactic grammar extensions *)
 
-let add_tactic_entry (kn, ml, tg) =
+let add_tactic_entry (kn, ml, tg) state =
   let open Tacexpr in
   let entry, pos = get_tactic_entry tg.tacgram_level in
   let mkact loc l =
@@ -186,7 +186,7 @@ let add_tactic_entry (kn, ml, tg) =
   let rules = make_rule mkact prods in
   synchronize_level_positions ();
   grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
-  1
+  (1, state)
 
 let tactic_grammar =
   create_grammar_command "TacticGrammar" add_tactic_entry
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 9cfd534b0..72cb14bad 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -343,12 +343,12 @@ let extend_constr forpat ng =
   in
   List.fold_left fold 0 ng.notgram_prods
 
-let extend_constr_notation (_, ng) =
+let extend_constr_notation (_, ng) state =
   (* Add the notation in constr *)
   let nb = extend_constr ForConstr ng in
   (* Add the notation in cases_pattern *)
   let nb' = extend_constr ForPattern ng in
-  nb + nb'
+  (nb + nb', state)
 
 let constr_grammar : (Notation.level * notation_grammar) grammar_command =
   create_grammar_command "Notation" extend_constr_notation
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index de57feb7f..efb52dc23 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
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1021ef484..98fc47133 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -234,11 +234,16 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
 (** {5 Extending the parser with Summary-synchronized commands} *)
 
+module GramState : Store.S
+(** Auxilliary state of the grammar. Any added data must be marshallable. *)
+
 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
+type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t
+
+val create_grammar_command : string -> 'a grammar_extension -> '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. *)