Make Numeral Notation obey Local/Global

Thanks to Emilio and Pierre-Marie Pédrot for pointers.

2 files changed, 14 insertions, 7 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index d6bd62e121..551f1bfa83 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -407,6 +407,7 @@ let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninter
     (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 *)
@@ -429,12 +430,15 @@ let subst_prim_token_interpretation (subs,infos) =
   { infos with
     pt_refs = List.map (subst_global_reference subs) infos.pt_refs }
 
+let classify_prim_token_interpretation infos =
+    if infos.pt_local then Dispose else Substitute infos
+
 let inPrimTokenInterp : prim_token_infos -> obj =
   declare_object {(default_object "PRIM-TOKEN-INTERP") with
      open_function  = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
      cache_function = cache_prim_token_interpretation;
      subst_function = subst_prim_token_interpretation;
-     classify_function = (fun o -> Substitute o)}
+     classify_function = classify_prim_token_interpretation}
 
 let enable_prim_token_interpretation infos =
   Lib.add_anonymous_leaf (inPrimTokenInterp infos)
@@ -450,20 +454,22 @@ 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) =
+let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   let uid = fresh_string_of sc in
   register_bignumeral_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
-    { pt_scope = sc;
+    { pt_local = local;
+      pt_scope = 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) =
+let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
   let uid = fresh_string_of sc in
   register_string_interpretation uid (interp,uninterp);
   enable_prim_token_interpretation
-    { pt_scope = sc;
+    { pt_local = local;
+      pt_scope = sc;
       pt_uid = uid;
       pt_required = dir;
       pt_refs = List.map_filter glob_prim_constr_key patl;
diff --git a/interp/notation.mli b/interp/notation.mli
index 1d01d75c82..e5478eff48 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -100,6 +100,7 @@ val register_string_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
 
 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 *)
@@ -123,10 +124,10 @@ val enable_prim_token_interpretation : prim_token_infos -> unit
     (the latter inside a [Mltop.declare_cache_obj]).
 *)
 
-val declare_numeral_interpreter : scope_name -> required_module ->
+val declare_numeral_interpreter : ?local:bool -> 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 ->
+val declare_string_interpreter : ?local:bool -> scope_name -> required_module ->
   string prim_token_interpreter ->
   glob_constr list * string prim_token_uninterpreter * bool -> unit