Supporting locality flag for custom entries + compatibility with modules.

Also prevents to use an entry name already defined.

7 files changed, 82 insertions, 17 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8455992f20..8dc2b7e139 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -564,18 +564,23 @@ let find_grammars_by_name name =
 
 let custom_entries = ref String.Map.empty
 
-let create_custom_entries s =
+let create_custom_entry local s =
+  if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
+    user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
   let sc = "constr:"^s in
   let sp = "pattern:"^s in
   let c = (Gram.entry_create sc : Constrexpr.constr_expr Gram.entry) in
   let p = (Gram.entry_create sp : Constrexpr.cases_pattern_expr Gram.entry) in
   register_grammars_by_name s [AnyEntry c; AnyEntry p];
-  custom_entries := String.Map.add s (c,p) !custom_entries
+  custom_entries := String.Map.add s (local,(c,p)) !custom_entries
 
-let find_custom_entries s =
+let lookup_custom_entry s =
   try String.Map.find s !custom_entries
   with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
 
+let find_custom_entry s = snd (lookup_custom_entry s)
+let locality_of_custom_entry s = fst (lookup_custom_entry s)
+
 (** Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
@@ -583,7 +588,7 @@ type frozen_t =
   (int * GrammarCommand.t * GramState.t) list *
   CLexer.keyword_state *
   any_entry list String.Map.t *
-  (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry) Util.String.Map.t
+  (bool * (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)) Util.String.Map.t
 
 let freeze _ : frozen_t =
   (!grammar_stack, CLexer.get_keyword_state (),
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9711cd0461..b2e1259646 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -273,7 +273,8 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list
 
-(** Create a custom entry of some name *)
+(** Create a custom entry of some name; boolean is [true] if local *)
 
-val create_custom_entries : string -> unit
-val find_custom_entries : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
+val create_custom_entry : bool -> string -> unit
+val find_custom_entry : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
+val locality_of_custom_entry : string -> bool
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index d01ebfb18e..1b33863e3b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -134,3 +134,23 @@ Module M15.
   Fail Local Notation "###### x" := (S x) (right associativity, at level 79).
   Local Notation "###### x" := (S x) (at level 79).
 End M15.
+
+(* 16. Some test about custom entries *)
+Module M16.
+  (* Test locality *)
+  Local Declare Custom Entry foo.
+  Fail Notation "#" := 0 (in custom foo). (* Should be local *)
+  Local Notation "#" := 0 (in custom foo).
+
+  (* Test import *)
+  Module A.
+  Declare Custom Entry foo2.
+  End A.
+  Fail Notation "##" := 0 (in custom foo2).
+  Import A.
+  Local Notation "##" := 0 (in custom foo2).
+
+  (* Test Print Grammar *)
+  Print Grammar foo.
+  Print Grammar foo2.
+End M16.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 65e5f4bede..720f9b774a 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -255,7 +255,7 @@ let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int op
   fun custom forpat level ->
   match custom with
   | InCustomEntry s ->
-     (let (entry_for_constr, entry_for_patttern) = find_custom_entries s in
+     (let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
      match forpat with
      | ForConstr -> entry_for_constr, Some level
      | ForPattern -> entry_for_patttern, Some level)
@@ -272,7 +272,7 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function
    | ForConstr -> Constr.operconstr
    | ForPattern -> Constr.pattern)
 | InCustomEntry s ->
-   let (entry_for_constr, entry_for_patttern) = find_custom_entries s in
+   let (entry_for_constr, entry_for_patttern) = find_custom_entry s in
    function
    | ForConstr -> entry_for_constr
    | ForPattern -> entry_for_patttern
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 67506a2551..34e18938dc 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1213,7 +1213,17 @@ let find_subentry_types from n assoc etyps symbols =
   let prec = List.map (assoc_of_type from n) sy_typs in
   sy_typs, prec
 
-let compute_syntax_data df modifiers =
+let check_locality_compatibility local custom i_typs =
+  if not local then
+    let subcustom = List.map_filter (function _,ETConstr (InCustomEntry s,_,_) -> Some s | _ -> None) i_typs in
+    let allcustoms = match custom with InCustomEntry s -> s::subcustom | _ -> subcustom in
+    List.iter (fun s ->
+        if Pcoq.locality_of_custom_entry s then
+          user_err (strbrk "Notation has to be declared local as it depends on custom entry " ++ str s ++
+                    strbrk " which is local."))
+      (List.uniquize allcustoms)
+
+let compute_syntax_data local df modifiers =
   let open SynData in
   let open NotationMods in
   let mods = interp_modifiers modifiers in
@@ -1244,6 +1254,7 @@ let compute_syntax_data df modifiers =
     else
       sy_typs, prec in
   let i_typs = set_internalization_type sy_typs in
+  check_locality_compatibility local mods.custom sy_typs;
   let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
   let pp_sy_data = (sy_typs,symbols) in
   let sy_fulldata = (ntn_for_grammar,(mods.custom,n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
@@ -1271,9 +1282,9 @@ let compute_syntax_data df modifiers =
     not_data    = sy_fulldata;
   }
 
-let compute_pure_syntax_data df mods =
+let compute_pure_syntax_data local df mods =
   let open SynData in
-  let sd = compute_syntax_data df mods in
+  let sd = compute_syntax_data local df mods in
   let msgs =
     if sd.only_parsing then
       (Feedback.msg_warning ?loc:None,
@@ -1429,7 +1440,7 @@ let to_map l =
 
 let add_notation_in_scope local df env c mods scope =
   let open SynData in
-  let sd = compute_syntax_data df mods in
+  let sd = compute_syntax_data local df mods in
   (* Prepare the interpretation *)
   (* Prepare the parsing and printing rules *)
   let sy_rules = make_syntax_rules sd in
@@ -1499,7 +1510,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
 (* Notations without interpretation (Reserved Notation) *)
 
 let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
-  let psd = compute_pure_syntax_data df mods in
+  let psd = compute_pure_syntax_data local df mods in
   let sy_rules = make_syntax_rules {psd with compat = None} in
   Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
@@ -1631,4 +1642,27 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
 (**********************************************************************)
 (* Declaration of custom entry                                        *)
 
-let declare_custom_entry = Pcoq.create_custom_entries
+let load_custom_entry _ _ = ()
+
+let open_custom_entry _ (_,(local,s)) =
+  Pcoq.create_custom_entry local s
+
+let cache_custom_entry o =
+  load_custom_entry 1 o;
+  open_custom_entry 1 o
+
+let subst_custom_entry (subst,x) = x
+
+let classify_custom_entry (local,s as o) =
+  if local then Dispose else Substitute o
+
+let inCustomEntry : locality_flag * string -> obj =
+  declare_object {(default_object "CUSTOM-ENTRIES") with
+      cache_function = cache_custom_entry;
+      open_function = open_custom_entry;
+      load_function = load_custom_entry;
+      subst_function = subst_custom_entry;
+      classify_function = classify_custom_entry}
+
+let declare_custom_entry local s =
+  Lib.add_anonymous_leaf (inCustomEntry (local,s))
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 045b8fa05c..73bee7121b 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -61,4 +61,4 @@ val check_infix_modifiers : syntax_modifier list -> unit
 
 val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
 
-val declare_custom_entry : string -> unit
+val declare_custom_entry : locality_flag -> string -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0f6cbd228e..9824172315 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -431,6 +431,10 @@ let vernac_notation ~atts =
   let local = enforce_module_locality atts.locality in
   Metasyntax.add_notation local (Global.env())
 
+let vernac_custom_entry ~atts s =
+  let local = enforce_module_locality atts.locality in
+  Metasyntax.declare_custom_entry local s
+
 (***********)
 (* Gallina *)
 
@@ -2097,7 +2101,7 @@ let interp ?proof ~atts ~st c =
   | VernacNotationAddFormat(n,k,v) ->
       Metasyntax.add_notation_extra_printing_rule n k v
   | VernacDeclareCustomEntry s ->
-      Metasyntax.declare_custom_entry s
+      vernac_custom_entry ~atts s
 
   (* Gallina *)
   | VernacDefinition ((discharge,kind),lid,d) ->
@@ -2226,6 +2230,7 @@ let check_vernac_supports_locality c l =
   | Some _, (
       VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+    | VernacDeclareCustomEntry _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
     | VernacAssumption _ | VernacStartTheoremProof _
     | VernacCoercion _ | VernacIdentityCoercion _