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.

1 files changed, 55 insertions, 27 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