Fix numeral notation for a rebase on top of master

Some of this code is cargo-culted or kludged to work.

As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter.  In
   this case, the function registration must be synchronized with the
   document state, but the functions should not be marshelled / stored
   in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
   In this case, the registration must be synchronized, and the function
   should be marshelled / stored in the .vo.

In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.

In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.

The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality.  For
plugins, a simple string suffices, as long as the string does not clash
between different plugins.  In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files.  Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.

----

Some of this code is response to comments on the PR

----

Some code is to fix an issue that bignums revealed:

Both Int31 and bignums registered numeral notations in int31_scope.  We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins.  This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).

1 files changed, 22 insertions, 15 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index f60ddcf909..56d6acbdae 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -378,38 +378,39 @@ let prim_token_interp_infos =
 let prim_token_uninterp_infos =
   ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t)
 
-let hashtbl_check_and_set uid f h eq =
+let hashtbl_check_and_set allow_overwrite uid f h eq =
   match Hashtbl.find h uid with
    | exception Not_found -> Hashtbl.add h uid f
+   | _ when allow_overwrite -> Hashtbl.add h uid f
    | g when eq f g -> ()
    | _ ->
       user_err ~hdr:"prim_token_interpreter"
        (str "Unique identifier " ++ str uid ++
         str " already used to register a numeral or string (un)interpreter.")
 
-let register_gen_interpretation uid (interp, uninterp) =
+let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
   hashtbl_check_and_set
-    uid interp prim_token_interpreters InnerPrimToken.interp_eq;
+    allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq;
   hashtbl_check_and_set
-    uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
+    allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq
 
-let register_rawnumeral_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp)
 
-let register_bignumeral_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp)
 
-let register_string_interpretation uid (interp, uninterp) =
-  register_gen_interpretation uid
+let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) =
+  register_gen_interpretation allow_overwrite uid
     (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp)
 
 type prim_token_infos = {
   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 : global_reference list; (** Entry points during uninterpretation *)
+  pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
 }
 
@@ -445,19 +446,25 @@ let enable_prim_token_interpretation infos =
     (the latter inside a [Mltop.declare_cache_obj]).
 *)
 
+let fresh_string_of =
+  let count = ref 0 in
+  fun root -> count := !count+1; (string_of_int !count)^"_"^root
+
 let declare_numeral_interpreter sc dir interp (patl,uninterp,b) =
-  register_bignumeral_interpretation sc (interp,uninterp);
+  let uid = fresh_string_of sc in
+  register_bignumeral_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
     { pt_scope = sc;
-      pt_uid = sc;
+      pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }
 let declare_string_interpreter sc dir interp (patl,uninterp,b) =
-  register_string_interpretation sc (interp,uninterp);
+  let uid = fresh_string_of sc in
+  register_string_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
     { pt_scope = sc;
-      pt_uid = sc;
+      pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
       pt_in_match = b }