Make Numeral Notation obey Local/Global

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

10 files changed, 47 insertions, 19 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
 
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 9bf0b29b61..5e36fbeb81 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -92,7 +92,8 @@ let _ =
   let sc = "char_scope" in
   register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
   at_declare_ml_module enable_prim_token_interpretation
-    { pt_scope = sc;
+    { pt_local = false;
+      pt_scope = sc;
       pt_uid = sc;
       pt_required = (ascii_path,ascii_module);
       pt_refs = [static_glob_Ascii];
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 4e29e6a6a4..ec14df3baa 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -13,6 +13,7 @@ DECLARE PLUGIN "numeral_notation_plugin"
 open Numeral
 open Pp
 open Names
+open Vernacinterp
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
@@ -32,5 +33,5 @@ END
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
-    [ vernac_numeral_notation ty f g (Id.to_string sc) o ]
+    [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ]
 END
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index 731eae349a..d3ffe936a9 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -106,7 +106,8 @@ let at_declare_ml_module f x =
 let _ =
   register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31);
   at_declare_ml_module enable_prim_token_interpretation
-    { pt_scope = int31_scope;
+    { pt_local = false;
+      pt_scope = int31_scope;
       pt_uid = int31_scope;
       pt_required = (int31_path,int31_module);
       pt_refs = [int31_construct];
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 321992eda6..fee93593d0 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -411,7 +411,7 @@ let type_error_of g ty loadZ =
      str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
      (if loadZ then str " (require BinNums first)." else str "."))
 
-let vernac_numeral_notation ty f g scope opts =
+let vernac_numeral_notation local ty f g scope opts =
   let int_ty = locate_int () in
   let z_pos_ty = locate_z () in
   let tyc = Smartlocate.global_inductive_with_alias ty in
@@ -467,7 +467,8 @@ let vernac_numeral_notation ty f g scope opts =
   (* TODO: un hash suffit-il ? *)
   let uid = Marshal.to_string o [] in
   let i = Notation.(
-       { pt_scope = scope;
+       { pt_local = local;
+         pt_scope = scope;
          pt_uid = uid;
          pt_required = Nametab.path_of_global (IndRef tyc),[];
          pt_refs = constructors;
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 2ad3574fe7..83ede6f48f 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -10,6 +10,7 @@
 
 open Libnames
 open Constrexpr
+open Vernacexpr
 
 (** * Numeral notation *)
 
@@ -18,4 +19,4 @@ type numnot_option =
   | Warning of raw_natural_number
   | Abstract of raw_natural_number
 
-val vernac_numeral_notation : qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
+val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index eccc544e41..04946c158b 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -141,7 +141,8 @@ let r_scope = "R_scope"
 let _ =
   register_bignumeral_interpretation r_scope (r_of_int,uninterp_r);
   at_declare_ml_module enable_prim_token_interpretation
-    { pt_scope = r_scope;
+    { pt_local = false;
+      pt_scope = r_scope;
       pt_uid = r_scope;
       pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
       pt_refs = [glob_IZR];
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index ca1bf0df27..640bcfde91 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -73,7 +73,8 @@ let _ =
   let sc = "string_scope" in
   register_string_interpretation sc (interp_string,uninterp_string);
   at_declare_ml_module enable_prim_token_interpretation
-    { pt_scope = sc;
+    { pt_local = false;
+      pt_scope = sc;
       pt_uid = sc;
       pt_required = (string_path,["Coq";"Strings";"String"]);
       pt_refs = [static_glob_String; static_glob_EmptyString];
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index bacc982ccc..4521ad0e37 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -139,7 +139,7 @@ Module Test8.
     Context (dummy : unit).
     Definition wrap' := let __ := dummy in wrap.
     Definition unwrap' := let __ := dummy in unwrap.
-    Global Numeral Notation wuint wrap' unwrap' : wuint8_scope.
+    Numeral Notation wuint wrap' unwrap' : wuint8_scope.
     Check let v := 0%wuint8 in v : wuint.
   End with_var.
   Check let v := 0%wuint8 in v : nat.
@@ -231,19 +231,33 @@ End Test13.
 
 Module Test14.
   (* Test that numeral notations follow [Import], not [Require], and
-     also test for current (INCORRECT!!) behavior that [Local] has no
-     effect in modules. *)
+     also test that [Local Numeral Notation]s do not escape modules
+     nor sections. *)
   Delimit Scope test14_scope with test14.
   Delimit Scope test14'_scope with test14'.
+  Delimit Scope test14''_scope with test14''.
+  Delimit Scope test14'''_scope with test14'''.
   Module Inner.
     Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
     Definition of_uint (x : Decimal.uint) : unit := tt.
     Local Numeral Notation unit of_uint to_uint : test14_scope.
     Global Numeral Notation unit of_uint to_uint : test14'_scope.
+    Check let v := 0%test14 in v : unit.
+    Check let v := 0%test14' in v : unit.
   End Inner.
   Fail Check let v := 0%test14 in v : unit.
   Fail Check let v := 0%test14' in v : unit.
   Import Inner.
-  Check let v := 0%test14 in v : unit. (* THIS SHOULD FAIL!! *)
+  Fail Check let v := 0%test14 in v : unit.
   Check let v := 0%test14' in v : unit.
+  Section InnerSection.
+    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Local Numeral Notation unit of_uint to_uint : test14''_scope.
+    Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope.
+    Check let v := 0%test14'' in v : unit.
+    Fail Check let v := 0%test14''' in v : unit.
+  End InnerSection.
+  Fail Check let v := 0%test14'' in v : unit.
+  Fail Check let v := 0%test14''' in v : unit.
 End Test14.