[parsing] Track need to reinit by typing

This PR is in preparation of #9067 (together with #11647) .

Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.

10 files changed, 84 insertions, 58 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 72b7cb2f84..e723d4ea1b 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -266,7 +266,7 @@ let print_rule fmt r =
 let print_entry fmt e =
   let print_position_opt fmt pos = print_opt fmt print_position pos in
   let print_rules fmt rules = print_list fmt print_rule rules in
-  fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ "
+  fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ "
     e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
 
 let print_ast fmt ext =
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 26afdcb9d5..92c3b7c6e8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -212,7 +212,8 @@ type 'a extend_statement =
   'a single_extend_statement list
 
 type extend_rule =
-| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
 
 module EntryCommand = Dyn.Make ()
 module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end
@@ -231,33 +232,39 @@ let camlp5_entries = ref EntryDataMap.empty
 
 (** Deletion *)
 
-let grammar_delete e reinit (pos,rls) =
+let grammar_delete e (pos,rls) =
   List.iter
     (fun (n,ass,lev) ->
       List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
-    (List.rev rls);
-  match reinit with
-  | Some (a,ext) ->
-    let lev = match pos with
+    (List.rev rls)
+
+let grammar_delete_reinit e reinit (pos, rls) =
+  grammar_delete e (pos, rls);
+  let a, ext = reinit in
+  let lev = match pos with
     | Some (Gramext.Level n) -> n
     | _ -> assert false
-    in
-    let warning msg = Feedback.msg_warning Pp.(str msg) in
-    (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
-  | None -> ()
+  in
+  let warning msg = Feedback.msg_warning Pp.(str msg) in
+  (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
 
 (** Extension *)
 
-let grammar_extend e reinit ext =
+let grammar_extend e ext =
   let ext = of_coq_extend_statement ext in
-  let undo () = grammar_delete e reinit ext in
+  let undo () = grammar_delete e ext in
   let pos, ext = fix_extend_statement ext in
   let redo () = G.safe_extend ~warning:None e pos ext in
   camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
-let grammar_extend_sync e reinit ext =
-  camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
+let grammar_extend_sync e ext =
+  camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
+  let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
+  G.safe_extend ~warning:None e pos ext
+
+let grammar_extend_sync_reinit e reinit ext =
+  camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
   let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
   G.safe_extend ~warning:None e pos ext
 
@@ -278,8 +285,12 @@ let rec remove_grammars n =
   if n>0 then
     match !camlp5_state with
        | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
-       | ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
-           grammar_delete g reinit (of_coq_extend_statement ext);
+       | ByGrammar (ExtendRuleReinit (g, reinit, ext)) :: t ->
+           grammar_delete_reinit g reinit (of_coq_extend_statement ext);
+           camlp5_state := t;
+           remove_grammars (n-1)
+       | ByGrammar (ExtendRule (g, ext)) :: t ->
+           grammar_delete g (of_coq_extend_statement ext);
            camlp5_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
@@ -507,6 +518,12 @@ let create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) ent
   let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in
   obj
 
+let iter_extend_sync = function
+  | ExtendRule (e, ext) ->
+    grammar_extend_sync e ext
+  | ExtendRuleReinit (e, reinit, ext) ->
+    grammar_extend_sync_reinit e reinit ext
+
 let extend_grammar_command tag g =
   let modify = GrammarInterpMap.find tag !grammar_interp in
   let grammar_state = match !grammar_stack with
@@ -514,8 +531,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_sync e reinit ext in
-  let () = List.iter iter rules in
+  let () = List.iter iter_extend_sync rules in
   let nb = List.length rules in
   grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 404fbdb4fd..f2fc007a7b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -225,7 +225,7 @@ type 'a extend_statement =
   Gramlib.Gramext.position option *
   'a single_extend_statement list
 
-val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit
+val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
@@ -242,7 +242,8 @@ type 'a grammar_command
     marshallable. *)
 
 type extend_rule =
-| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
 
 type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 (** Grammar extension entry point. Given some ['a] and a current grammar state,
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 13a2f3b8c0..8b4520947b 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
-  let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in
+  let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
   ([r], state)
 
 let tactic_grammar =
@@ -415,7 +415,7 @@ let create_ltac_quotation name cast (e, l) =
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
   let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
+  Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
 
 (** Command *)
 
@@ -759,7 +759,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
     e
   | Vernacextend.Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
-    let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+    let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
     e
   in
   let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index c1bd585f3f..5317aa4d91 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -889,7 +889,7 @@ let rules = [
 ] in
 
 Hook.set Tac2entries.register_constr_quotations begin fun () ->
-  Pcoq.grammar_extend Pcoq.Constr.operconstr None (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
+  Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
 end
 
 }
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d6db4a735c..70cba858c9 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -643,7 +643,7 @@ let perform_notation syn st =
   | Some lev -> Some (string_of_int lev)
   in
   let rule = (lev, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.tac2expr, None, (None, [rule]))], st)
+  ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st)
 
 let ltac2_notation =
   Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 72e6d41969..ead86bd12f 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -96,38 +96,38 @@ let create_pos = function
 let find_position_gen current ensure assoc lev =
   match lev with
   | None ->
-      current, (None, None, None, 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
+    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)
+          updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
         | _ ->
           (* The reinit flag has been updated *)
-           updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
-        end
-      with
-          (* Nothing has changed *)
-          Exit ->
-            (* Just inherit the existing associativity and name (None) *)
-            current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
+          updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
+      end
+    with
+    (* Nothing has changed *)
+      Exit ->
+      (* Just inherit the existing associativity and name (None) *)
+      current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
 
 let rec list_mem_assoc_triple x = function
   | [] -> false
@@ -505,7 +505,11 @@ let target_to_bool : type r. r target -> bool = function
 
 let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
   let empty = (pos, [(name, p4assoc, [])]) in
-  ExtendRule (target_entry where forpat, reinit, empty)
+  match reinit with
+  | None ->
+    ExtendRule (target_entry where forpat, empty)
+  | Some reinit ->
+    ExtendRuleReinit (target_entry where forpat, reinit, empty)
 
 let different_levels (custom,opt_level) (custom',string_level) =
   match opt_level with
@@ -552,7 +556,12 @@ let extend_constr state forpat ng =
         | MayRecRNo symbs -> Rule (symbs, act)
         | MayRecRMay symbs -> Rule (symbs, act) in
       name, p4assoc, [r] in
-    let r = ExtendRule (entry, reinit, (pos, [rule])) in
+    let r = match reinit with
+      | None ->
+        ExtendRule (entry, (pos, [rule]))
+      | Some reinit ->
+        ExtendRuleReinit (entry, reinit, (pos, [rule]))
+    in
     (accu @ empty_rules @ [r], state)
   in
   List.fold_left fold ([], state) ng.notgram_prods
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 62eb561f3c..2b1d99c7a9 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl =
   vernac_exts := (s,gl) :: !vernac_exts;
   let mkact loc l = VernacExtend (s, l) in
   let rules = [make_rule mkact gl] in
-  grammar_extend nt None (None, [None, None, rules])
+  grammar_extend nt (None, [None, None, rules])
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 826e88cabf..2425f3d6c1 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -58,7 +58,7 @@ module Vernac_ =
         Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
         Rule (Next (Stop, Aentry vernac_control), act_vernac);
       ] in
-      Pcoq.grammar_extend main_entry None (None, [None, None, rule])
+      Pcoq.grammar_extend main_entry (None, [None, None, rule])
 
     let select_tactic_entry spec =
       match spec with
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index e29086d726..f41df06f85 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -254,7 +254,7 @@ let vernac_argument_extend ~name arg =
     e
   | Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
-    let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+    let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
     e
   in
   let pr = arg.arg_printer in