Moving the grammar summary to Pcoq.

5 files changed, 100 insertions, 97 deletions

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index f829ae4f5..5c1e7c033 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) =
 let tactic_grammar =
   create_grammar_command "TacticGrammar" add_tactic_entry
 
-let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn)
+let extend_tactic_grammar kn ml ntn = extend_grammar_command tactic_grammar (kn, ml, ntn)
 
 (**********************************************************************)
 (* Tactic Notation                                                    *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 4c038db65..9cfd534b0 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -350,85 +350,16 @@ let extend_constr_notation (_, ng) =
   let nb' = extend_constr ForPattern 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_grammar tag g =
-  let nb = GrammarInterpMap.find tag !grammar_interp g in
-  grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
-
-let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
-
-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 6ec106626..1fe06a29d 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/pcoq.ml b/parsing/pcoq.ml
index 631c5325d..de57feb7f 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 () =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 72edab8f2..1021ef484 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -106,9 +106,6 @@ val grammar_extend :
   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
@@ -235,6 +232,25 @@ val set_command_entry : vernac_expr Gram.entry -> unit
 
 val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 
+(** {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_command : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
+
+val recover_grammar_command : 'a grammar_command -> 'a list
+(** Recover the current stack of grammar extensions. *)
+
+val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
+
 (** Registering/resetting the level of a constr entry *)
 
 type gram_level =
@@ -247,5 +263,3 @@ val find_position :
 val synchronize_level_positions : unit -> unit
 
 val register_empty_levels : bool -> int list -> gram_level list
-
-val remove_levels : int -> unit