prim notations backtrackable, their declarations now in two parts (API change)

 The first part (e.g. register_bignumeral_interpretation) deals only with
 the interp/uninterp closures. It should typically be done as a side
 effect during a syntax plugin loading. No prim notation are active yet
 after this phase.

 The second part (enable_prim_token_interpretation) activates the prim
 notation. It is now correctly talking to Summary and to the LibStack.
 To avoid "phantom" objects in libstack after a mere Require, this
 second part should be done inside a Mltop.declare_cache_obj

 The link between the two parts is a prim_token_uid (a string), which
 should be unique for each primitive notation. When this primitive
 notation is specific to a scope, the scope_name could be used as uid.

 Btw, the list of "patterns" for detecting when an uninterpreter should
 be considered is now restricted to a list of global_reference
 (inductive constructors, or injection functions such as IZR).
 The earlier API was accepting a glob_constr list, but was actually
 only working well for global_reference.

 A minimal compatibility is provided (declare_numeral_interpreter),
 but is discouraged, since it is known to store uncessary objects
 in the libstack.

1 files changed, 48 insertions, 12 deletions

diff --git a/interp/notation.mli b/interp/notation.mli
index e8408330af..2545e494ef 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Bigint
 open Names
 open Libnames
 open Constrexpr
@@ -75,24 +74,61 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 type notation_location = (DirPath.t * DirPath.t) * string
 type required_module = full_path * string list
-type cases_pattern_status = bool (** true = use prim token in patterns *)
+type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
 
-type 'a prim_token_interpreter =
-    ?loc:Loc.t -> 'a -> glob_constr
+(** The unique id string below will be used to refer to a particular
+    registered interpreter/uninterpreter of numeral or string notation.
+    Using the same uid for different (un)interpreters will fail.
+    If at most one interpretation of prim token is used per scope,
+    then the scope name could be used as unique id. *)
 
-type 'a prim_token_uninterpreter =
-    glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status
+type prim_token_uid = string
 
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr
+type 'a prim_token_uninterpreter = any_glob_constr -> 'a option
 
-val declare_rawnumeral_interpreter : scope_name -> required_module ->
-  rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit
+type 'a prim_token_interpretation =
+  'a prim_token_interpreter * 'a prim_token_uninterpreter
 
-val declare_numeral_interpreter : scope_name -> required_module ->
-  bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit
+val register_rawnumeral_interpretation :
+  prim_token_uid -> rawnum prim_token_interpretation -> unit
+
+val register_bignumeral_interpretation :
+  prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+
+val register_string_interpretation :
+  prim_token_uid -> string prim_token_interpretation -> unit
+
+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_in_match : bool (** Is this prim token legal in match patterns ? *)
+}
 
+(** Note: most of the time, the [pt_refs] field above will contain
+    inductive constructors (e.g. O and S for nat). But it could also be
+    injection functions such as IZR for reals. *)
+
+(** Activate a prim token interpretation whose unique id and functions
+    have already been registered. *)
+
+val enable_prim_token_interpretation : prim_token_infos -> unit
+
+(** Compatibility.
+    Avoid the next two functions, they will now store unnecessary
+    objects in the library segment. Instead, combine
+    [register_*_interpretation] and [enable_prim_token_interpretation]
+    (the latter inside a [Mltop.declare_cache_obj]).
+*)
+
+val declare_numeral_interpreter : scope_name -> required_module ->
+  Bigint.bigint prim_token_interpreter ->
+  glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
 val declare_string_interpreter : scope_name -> required_module ->
-  string prim_token_interpreter -> string prim_token_uninterpreter -> unit
+  string prim_token_interpreter ->
+  glob_constr list * string prim_token_uninterpreter * bool -> unit
 
 (** Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)