Supporting locality flag for custom entries + compatibility with modules.

Also prevents to use an entry name already defined.

4 files changed, 49 insertions, 10 deletions

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 _