Fix Numeral Notations (4/4 - fixing synch)

This fixes #8401
Supersedes / closes #8407

Vernacular-command-registered numeral notations now live in the summary,
and the interpretation function for them is hard-coded.

Plugin-registered numeral notations are still unsynchronized, and only
the UIDs of these functions gets synchronized.  I am not 100% sure why
this is fine, but the test-suite file working suggests that it is fine.
I think it is because worker delegation correctly handles
non-synchronized state which is declared at `Declare ML Module`-time.

This final commit changes the synchronization of numeral notations (and
deletes no-longer-used declarations in notation.mli that were introduced
temporarily in the last commit).  Since the interpretation can now be
done in notation.ml, we no longer need to register unique ids for
numeral notation (un)interp functions, and can instead synchronize the
underlying constants with the document state.  This is the change that
actually fixes #8401.

9 files changed, 89 insertions, 67 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index eeee1ca899..02c7812e21 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -379,8 +379,14 @@ module InnerPrimToken = struct
 
 end
 
-(* The following two tables of (un)interpreters will *not* be synchronized.
-   But their indexes will be checked to be unique *)
+(* The following two tables of (un)interpreters will *not* be
+   synchronized.  But their indexes will be checked to be unique.
+   These tables contain primitive token interpreters which are
+   registered in plugins, such as string and ascii syntax.  It is
+   essential that only plugins add to these tables, and that
+   vernacular commands do not.  See
+   https://github.com/coq/coq/issues/8401 for details of what goes
+   wrong when vernacular commands add to these tables. *)
 let prim_token_interpreters =
   (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t)
 
@@ -701,15 +707,36 @@ let uninterp o (Glob_term.AnyGlobConstr n) =
   | NotANumber -> None (* all other functions except big2raw *)
 end
 
+(* A [prim_token_infos], which is synchronized with the document
+   state, either contains a unique id pointing to an unsynchronized
+   prim token function, or a numeral notation object describing how to
+   interpret and uninterpret.  We provide [prim_token_infos] because
+   we expect plugins to provide their own interpretation functions,
+   rather than going through numeral notations, which are available as
+   a vernacular. *)
+
+type prim_token_interp_info =
+    Uid of prim_token_uid
+  | NumeralNotation of numeral_notation_obj
+
+type prim_token_infos = {
+  pt_local : bool; (** Is this interpretation local? *)
+  pt_scope : scope_name; (** Concerned scope *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+  pt_required : required_module; (** Module that should be loaded first *)
+  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
+  pt_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
+
 (* Table from scope_name to backtrack-able informations about interpreters
    (in particular interpreter unique id). *)
 let prim_token_interp_infos =
-  ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t)
+  ref (String.Map.empty : (required_module * prim_token_interp_info) String.Map.t)
 
 (* Table from global_reference to backtrack-able informations about
    prim_token uninterpretation (in particular uninterpreter unique id). *)
 let prim_token_uninterp_infos =
-  ref (GlobRef.Map.empty : (scope_name * prim_token_uid * bool) GlobRef.Map.t)
+  ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t)
 
 let hashtbl_check_and_set allow_overwrite uid f h eq =
   match Hashtbl.find h uid with
@@ -739,23 +766,14 @@ let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninter
   register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
 
-type prim_token_infos = {
-  pt_local : bool; (** Is this interpretation local? *)
-  pt_scope : scope_name; (** Concerned scope *)
-  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
-  pt_required : required_module; (** Module that should be loaded first *)
-  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
-  pt_in_match : bool (** Is this prim token legal in match patterns ? *)
-}
-
 let cache_prim_token_interpretation (_,infos) =
+  let ptii = infos.pt_interp_info in
   let sc = infos.pt_scope in
-  let uid = infos.pt_uid in
   check_scope ~tolerant:true sc;
   prim_token_interp_infos :=
-    String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
+    String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
   List.iter (fun r -> prim_token_uninterp_infos :=
-                        GlobRef.Map.add r (sc,uid,infos.pt_in_match)
+                        GlobRef.Map.add r (sc,ptii,infos.pt_in_match)
                           !prim_token_uninterp_infos)
             infos.pt_refs
 
@@ -793,7 +811,7 @@ let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   enable_prim_token_interpretation
     { pt_local = local;
       pt_scope = sc;
-      pt_uid = uid;
+      pt_interp_info = Uid uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
@@ -803,7 +821,7 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   enable_prim_token_interpretation
     { pt_local = local;
       pt_scope = sc;
-      pt_uid = uid;
+      pt_interp_info = Uid uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
@@ -919,9 +937,12 @@ let find_prim_token check_allowed ?loc p sc =
     pat, df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in
+  let (spdir,info) = String.Map.find sc !prim_token_interp_infos in
   check_required_module ?loc sc spdir;
-  let interp = Hashtbl.find prim_token_interpreters uid in
+  let interp = match info with
+    | Uid uid -> Hashtbl.find prim_token_interpreters uid
+    | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+  in
   let pat = InnerPrimToken.do_interp ?loc interp p in
   check_allowed pat;
   pat, ((dirpath (fst spdir),DirPath.empty),"")
@@ -1097,8 +1118,11 @@ let uninterp_prim_token c =
   | None -> raise Notation_ops.No_match
   | Some r ->
      try
-       let (sc,uid,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
-       let uninterp = Hashtbl.find prim_token_uninterpreters uid in
+       let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in
+       let uninterp = match info with
+         | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
+         | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+       in
        match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
        | None -> raise Notation_ops.No_match
        | Some n -> (sc,n)
@@ -1113,12 +1137,16 @@ let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
     try
       let uid = snd (String.Map.find scope !prim_token_interp_infos) in
-      let interp = Hashtbl.find prim_token_interpreters uid in
       let open InnerPrimToken in
-      match n, interp with
-      | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
-      | String _, StringInterp _ -> true
-      | _ -> false
+      match n, uid with
+      | Numeral _, NumeralNotation _ -> true
+      | _, NumeralNotation _ -> false
+      | _, Uid uid ->
+        let interp = Hashtbl.find prim_token_interpreters uid in
+        match n, interp with
+        | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+        | String _, StringInterp _ -> true
+        | _ -> false
     with Not_found -> false
   in
   let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation.mli b/interp/notation.mli
index 76bf70d452..734198bbf6 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -139,15 +139,14 @@ type numeral_notation_obj =
     num_ty : Libnames.qualid; (* for warnings / error messages *)
     warning : numnot_option }
 
-module Numeral : sig
-  val interp : numeral_notation_obj -> rawnum prim_token_interpreter
-  val uninterp : numeral_notation_obj -> rawnum prim_token_uninterpreter
-end
+type prim_token_interp_info =
+    Uid of prim_token_uid
+  | NumeralNotation of numeral_notation_obj
 
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
-  pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
   pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 5e36fbeb81..53153198f9 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -94,7 +94,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = Uid sc;
       pt_required = (ascii_path,ascii_module);
       pt_refs = [static_glob_Ascii];
       pt_in_match = true }
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 68b8178368..55f61a58f9 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,8 +10,8 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
-open Numeral
 open Notation
+open Numeral
 open Pp
 open Names
 open Vernacinterp
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index d3ffe936a9..e34a401c2c 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -108,7 +108,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = int31_scope;
-      pt_uid = int31_scope;
+      pt_interp_info = Uid int31_scope;
       pt_required = (int31_path,int31_module);
       pt_refs = [int31_construct];
       pt_in_match = true }
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 1a70c9536d..10a0af0b8f 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -27,29 +27,6 @@ let warn_abstract_large_num_no_op =
       Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
       strbrk "option type.")
 
-(* Here we only register the interp and uninterp functions
-   for a particular Numeral Notation (determined by a unique
-   string). The actual activation of the notation will be done
-   later (cf. Notation.enable_prim_token_interpretation).
-   This registration of interp/uninterp must be added in the
-   libstack, otherwise this won't work through a Require. *)
-
-let load_numeral_notation _ (_, (uid,opts)) =
-  Notation.register_rawnumeral_interpretation
-    ~allow_overwrite:true uid (Notation.Numeral.interp opts, Notation.Numeral.uninterp opts)
-
-let cache_numeral_notation x = load_numeral_notation 1 x
-
-(* TODO: substitution ?
-   TODO: uid pas stable par substitution dans opts
- *)
-
-let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj =
-  Libobject.declare_object {
-    (Libobject.default_object "NUMERAL NOTATION") with
-    Libobject.cache_function = cache_numeral_notation;
-    Libobject.load_function = load_numeral_notation }
-
 let get_constructors ind =
   let mib,oib = Global.lookup_inductive ind in
   let mc = oib.Declarations.mind_consnames in
@@ -154,15 +131,12 @@ let vernac_numeral_notation local ty f g scope opts =
   (match opts, to_kind with
    | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
    | _ -> ());
-  (* TODO: un hash suffit-il ? *)
-  let uid = Marshal.to_string o [] in
-  let i = Notation.(
+  let i =
        { pt_local = local;
          pt_scope = scope;
-         pt_uid = uid;
+         pt_interp_info = NumeralNotation o;
          pt_required = Nametab.path_of_global (IndRef tyc),[];
          pt_refs = constructors;
-         pt_in_match = true })
+         pt_in_match = true }
   in
-  Lib.add_anonymous_leaf (inNumeralNotation (uid,o));
-  Notation.enable_prim_token_interpretation i
+  enable_prim_token_interpretation i
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 04946c158b..49497aef54 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -143,7 +143,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = r_scope;
-      pt_uid = r_scope;
+      pt_interp_info = Uid r_scope;
       pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
       pt_refs = [glob_IZR];
       pt_in_match = false }
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 640bcfde91..7478c1e978 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -75,7 +75,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = Uid sc;
       pt_required = (string_path,["Coq";"Strings";"String"]);
       pt_refs = [static_glob_String; static_glob_EmptyString];
       pt_in_match = true }
diff --git a/test-suite/vio/numeral.v b/test-suite/vio/numeral.v
new file mode 100644
index 0000000000..f28355bb29
--- /dev/null
+++ b/test-suite/vio/numeral.v
@@ -0,0 +1,21 @@
+Lemma foo : True.
+Proof.
+Check 0 : nat.
+Check 0 : nat.
+exact I.
+Qed.
+
+Lemma bar : True.
+Proof.
+pose (0 : nat).
+exact I.
+Qed.
+
+Require Import Coq.Strings.Ascii.
+Open Scope char_scope.
+
+Lemma baz : True.
+Proof.
+pose "s".
+exact I.
+Qed.