`deprecated` attribute support for notations and syntactic definitions

We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.

5 files changed, 77 insertions, 80 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 1ad5862d5d..ab14974598 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -73,11 +73,6 @@ module Notations = struct
 end
 open Notations
 
-type deprecation = { since : string option ; note : string option }
-
-let mk_deprecation ?(since=None) ?(note=None) () =
-  { since ; note }
-
 let assert_empty k v =
   if v <> VernacFlagEmpty
   then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
@@ -213,19 +208,16 @@ let polymorphic =
   universe_transform ~warn_unqualified:true >>
   qualify_attribute ukey polymorphic_base
 
-let deprecation_parser : deprecation key_parser = fun orig args ->
+let deprecation_parser : Deprecation.t key_parser = fun orig args ->
   assert_once ~name:"deprecation" orig;
   match args with
   | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
   | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
-    let since = Some since and note = Some note in
-    mk_deprecation ~since ~note ()
+    Deprecation.make ~since ~note ()
   | VernacFlagList [ "since", VernacFlagLeaf since ] ->
-    let since = Some since in
-    mk_deprecation ~since ()
+    Deprecation.make ~since ()
   | VernacFlagList [ "note", VernacFlagLeaf note ] ->
-    let note = Some note in
-    mk_deprecation ~note ()
+    Deprecation.make ~note ()
   |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
 
 let deprecation = attribute_of_list ["deprecated",deprecation_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 44688ddafc..53caf49efd 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -43,15 +43,11 @@ end
 
 (** Definitions for some standard attributes. *)
 
-type deprecation = { since : string option ; note : string option }
-
-val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
-
 val polymorphic : bool attribute
 val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
-val deprecation : deprecation option attribute
+val deprecation : Deprecation.t option attribute
 val canonical : bool attribute
 
 val program_mode_option_name : string list
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 50914959dc..b96f500beb 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -732,13 +732,8 @@ type syntax_extension = {
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
   synext_extra : (string * string) list;
-  synext_compat : Flags.compat_version option;
 }
 
-let is_active_compat = function
-| None -> true
-| Some v -> 0 <= Flags.version_compare v !Flags.compat_version
-
 type syntax_extension_obj = locality_flag * syntax_extension
 
 let check_and_extend_constr_grammar ntn rule =
@@ -759,7 +754,7 @@ let cache_one_syntax_extension se =
     let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
     if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
   with Not_found ->
-    if is_active_compat se.synext_compat then begin
+    begin
       (* Reserve the notation level *)
       Notgram_ops.declare_notation_level ntn prec ~onlyprint;
       (* Declare the parsing rule *)
@@ -934,10 +929,6 @@ let is_only_printing mods =
   let test = function SetOnlyPrinting -> true | _ -> false in
   List.exists test mods
 
-let get_compat_version mods =
-  let test = function SetCompatVersion v -> Some v | _ -> None in
-  try Some (List.find_map test mods) with Not_found -> None
-
 (* Compute precedences from modifiers (or find default ones) *)
 
 let set_entry_type from etyps (x,typ) =
@@ -1177,7 +1168,7 @@ module SynData = struct
     (* Fields coming from the vernac-level modifiers *)
     only_parsing  : bool;
     only_printing : bool;
-    compat        : Flags.compat_version option;
+    deprecation   : Deprecation.t option;
     format        : lstring option;
     extra         : (string * string) list;
 
@@ -1222,12 +1213,32 @@ let check_locality_compatibility local custom i_typs =
                     strbrk " which is local."))
       (List.uniquize allcustoms)
 
-let compute_syntax_data local df modifiers =
+let warn_deprecated_compat =
+  CWarnings.create ~name:"deprecated-compat" ~category:"deprecated"
+    (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++
+                   str"Please use the \"deprecated\" attributed instead."))
+
+(* Returns the new deprecation and the onlyparsing status. This should be
+removed together with the compat syntax modifier. *)
+let merge_compat_deprecation compat deprecation =
+  match compat, deprecation with
+  | Some Flags.Current, _ -> deprecation, true
+  | Some _, Some _ ->
+    CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute."
+                        ++ spc () ++ str"Please use only the latter.")
+  | Some v, None ->
+    warn_deprecated_compat ();
+    Some (Deprecation.make ~since:(Flags.pr_version v) ()), true
+  | None, Some _ -> deprecation, true
+  | None, None -> deprecation, false
+
+let compute_syntax_data ~local deprecation df modifiers =
   let open SynData in
   let open NotationMods in
   let mods = interp_modifiers modifiers in
   let onlyprint = mods.only_printing in
   let onlyparse = mods.only_parsing in
+  let deprecation, _ = merge_compat_deprecation mods.compat deprecation in
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
   let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
@@ -1265,7 +1276,7 @@ let compute_syntax_data local df modifiers =
 
     only_parsing  = mods.only_parsing;
     only_printing = mods.only_printing;
-    compat        = mods.compat;
+    deprecation;
     format        = mods.format;
     extra         = mods.extra;
 
@@ -1281,9 +1292,9 @@ let compute_syntax_data local df modifiers =
     not_data    = sy_fulldata;
   }
 
-let compute_pure_syntax_data local df mods =
+let compute_pure_syntax_data ~local df mods =
   let open SynData in
-  let sd = compute_syntax_data local df mods in
+  let sd = compute_syntax_data ~local None df mods in
   let msgs =
     if sd.only_parsing then
       (Feedback.msg_warning ?loc:None,
@@ -1301,7 +1312,7 @@ type notation_obj = {
   notobj_coercion : entry_coercion_kind option;
   notobj_onlyparse : bool;
   notobj_onlyprint : bool;
-  notobj_compat : Flags.compat_version option;
+  notobj_deprecation : Deprecation.t option;
   notobj_notation : notation * notation_location;
 }
 
@@ -1323,11 +1334,11 @@ let open_notation i (_, nobj) =
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
   let onlyprint = nobj.notobj_onlyprint  in
+  let deprecation = nobj.notobj_deprecation in
   let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
-  let active = is_active_compat nobj.notobj_compat in
-  if Int.equal i 1 && fresh && active then begin
+  if Int.equal i 1 && fresh then begin
     (* Declare the interpretation *)
-    let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
+    let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
     (* Declare the uninterpretation *)
     if not nobj.notobj_onlyparse then
       Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
@@ -1388,7 +1399,6 @@ let recover_notation_syntax ntn =
       synext_notgram = pa_rule;
       synext_unparsing = pp_rule;
       synext_extra = pp_extra_rules;
-      synext_compat = None;
     }
   with Not_found ->
     raise NoSyntaxRule
@@ -1437,7 +1447,6 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
     synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
     synext_unparsing = pp_rule;
     synext_extra  = sd.extra;
-    synext_compat = sd.compat;
   }
 
 (**********************************************************************)
@@ -1447,9 +1456,9 @@ let to_map l =
   let fold accu (x, v) = Id.Map.add x v accu in
   List.fold_left fold Id.Map.empty l
 
-let add_notation_in_scope local df env c mods scope =
+let add_notation_in_scope ~local deprecation df env c mods scope =
   let open SynData in
-  let sd = compute_syntax_data local df mods in
+  let sd = compute_syntax_data ~local deprecation df mods in
   (* Prepare the interpretation *)
   (* Prepare the parsing and printing rules *)
   let sy_rules = make_syntax_rules sd in
@@ -1470,7 +1479,7 @@ let add_notation_in_scope local df env c mods scope =
     notobj_onlyparse = onlyparse;
     notobj_coercion = coe;
     notobj_onlyprint = sd.only_printing;
-    notobj_compat = sd.compat;
+    notobj_deprecation = sd.deprecation;
     notobj_notation = sd.info;
   } in
   (* Ready to change the global state *)
@@ -1479,7 +1488,7 @@ let add_notation_in_scope local df env c mods scope =
   Lib.add_anonymous_leaf (inNotation notation);
   sd.info
 
-let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
+let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation =
   let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
@@ -1510,7 +1519,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
     notobj_onlyparse = onlyparse;
     notobj_coercion = coe;
     notobj_onlyprint = onlyprint;
-    notobj_compat = compat;
+    notobj_deprecation = deprecation;
     notobj_notation = df';
   } in
   Lib.add_anonymous_leaf (inNotation notation);
@@ -1518,41 +1527,40 @@ 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 local df mods in
-  let sy_rules = make_syntax_rules {psd with compat = None} in
+let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
+  let psd = compute_pure_syntax_data ~local df mods in
+  let sy_rules = make_syntax_rules {psd with deprecation = None} in
   Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
 (* Notations with only interpretation *)
 
 let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
-  let df' = add_notation_interpretation_core false df env c sc false false None in
+  let df' = add_notation_interpretation_core ~local:false df env c sc false false None in
   Dumpglob.dump_notation (loc,df') sc true
 
 let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
   (try ignore
-    (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
+    (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ());
   with NoSyntaxRule ->
     user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
 
 (* Main entry point *)
 
-let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
+let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc =
   let df' =
    if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
     let onlyparse = is_only_parsing modifiers in
     let onlyprint = is_only_printing modifiers in
-    let compat = get_compat_version modifiers in
-    try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat
+    try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
-      add_notation_in_scope local df env c modifiers sc
+      add_notation_in_scope ~local deprecation df env c modifiers sc
    else
     (* Declare both syntax and interpretation *)
-    add_notation_in_scope local df env c modifiers sc
+    add_notation_in_scope ~local deprecation df env c modifiers sc
   in
   Dumpglob.dump_notation (loc,df') sc true
 
@@ -1566,7 +1574,7 @@ let add_notation_extra_printing_rule df k v =
 
 let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None)
 
-let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
+let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc =
   check_infix_modifiers modifiers;
   (* check the precedence *)
   let vars = names_of_constr_expr pr in
@@ -1575,7 +1583,7 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
   let metas = [inject_var x; inject_var y] in
   let c = mkAppC (pr,metas) in
   let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
-  add_notation local env c (df,modifiers) sc
+  add_notation ~local deprecation env c (df,modifiers) sc
 
 (**********************************************************************)
 (* Scopes, delimiters and classes bound to scopes                     *)
@@ -1651,7 +1659,7 @@ let try_interp_name_alias = function
   | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
   | _ -> raise Not_found
 
-let add_syntactic_definition env ident (vars,c) local onlyparse =
+let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
   let vars,reversibility,pat =
     try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
     with Not_found ->
@@ -1665,11 +1673,9 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
       let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, reversibility, pat
   in
-  let onlyparse = match onlyparse with
-    | None when fst (printability None false reversibility pat) -> Some Flags.Current
-    | p -> p
-  in
-  Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+  let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in
+  let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
+  Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
 
 (**********************************************************************)
 (* Declaration of custom entry                                        *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 6435df23c7..6532cee367 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -19,10 +19,10 @@ val add_token_obj : string -> unit
 
 (** Adding a (constr) notation in the environment*)
 
-val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) ->
+val add_infix : local:bool -> Deprecation.t option -> env -> (lstring * syntax_modifier list) ->
   constr_expr -> scope_name option -> unit
 
-val add_notation : locality_flag -> env -> constr_expr ->
+val add_notation : local:bool -> Deprecation.t option -> env -> constr_expr ->
   (lstring * syntax_modifier list) -> scope_name option -> unit
 
 val add_notation_extra_printing_rule : string -> string -> string -> unit
@@ -47,12 +47,12 @@ val set_notation_for_interpretation : env -> Constrintern.internalization_env ->
 (** Add only the parsing/printing rule of a notation *)
 
 val add_syntax_extension :
-  locality_flag -> (lstring * syntax_modifier list) -> unit
+  local:bool -> (lstring * syntax_modifier list) -> unit
 
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
-val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
-  bool -> Flags.compat_version option -> unit
+val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
+  Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit
 
 (** Print the Camlp5 state of a grammar *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 18e0fde296..66b172f277 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -85,7 +85,7 @@ module DefAttributes = struct
     locality : bool option;
     polymorphic : bool;
     program : bool;
-    deprecated : deprecation option;
+    deprecated : Deprecation.t option;
   }
 
   let parse f =
@@ -96,6 +96,8 @@ module DefAttributes = struct
     { polymorphic; program; locality; deprecated }
 end
 
+let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
+
 let with_locality ~atts f =
   let local = Attributes.(parse locality atts) in
   f ~local
@@ -106,8 +108,7 @@ let with_section_locality ~atts f =
   f ~section_local
 
 let with_module_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  let module_local = make_module_locality local in
+  let module_local = Attributes.(parse module_locality atts) in
   f ~module_local
 
 let with_def_attributes ~atts f =
@@ -511,7 +512,7 @@ let dump_global r =
 
 let vernac_syntax_extension ~module_local infix l =
   if infix then Metasyntax.check_infix_modifiers (snd l);
-  Metasyntax.add_syntax_extension module_local l
+  Metasyntax.add_syntax_extension ~local:module_local l
 
 let vernac_declare_scope ~module_local sc =
   Metasyntax.declare_scope module_local sc
@@ -530,11 +531,13 @@ let vernac_open_close_scope ~section_local (b,s) =
 let vernac_arguments_scope ~section_local r scl =
   Notation.declare_arguments_scope section_local (smart_global r) scl
 
-let vernac_infix ~module_local =
-  Metasyntax.add_infix module_local (Global.env())
+let vernac_infix ~atts =
+  let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+  Metasyntax.add_infix ~local:module_local deprecation (Global.env())
 
-let vernac_notation ~module_local =
-  Metasyntax.add_notation module_local (Global.env())
+let vernac_notation ~atts =
+  let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+  Metasyntax.add_notation ~local:module_local deprecation (Global.env())
 
 let vernac_custom_entry ~module_local s =
   Metasyntax.declare_custom_entry module_local s
@@ -1261,9 +1264,10 @@ let vernac_hints ~atts dbnames h =
   let local = enforce_module_locality local in
   Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
 
-let vernac_syntactic_definition ~module_local lid x y =
+let vernac_syntactic_definition ~atts lid x compat =
+  let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
   Dumpglob.dump_definition lid false "syndef";
-  Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
+  Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
 
 let cache_bidi_hints (_name, (gr, ohint)) =
   match ohint with
@@ -2374,9 +2378,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacOpenCloseScope (b, s) ->
     VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s))
   | VernacInfix (mv,qid,sc) ->
-    VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc)
+    VtDefault(fun () -> vernac_infix ~atts mv qid sc)
   | VernacNotation (c,infpl,sc) ->
-    VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc)
+    VtDefault(fun () -> vernac_notation ~atts c infpl sc)
   | VernacNotationAddFormat(n,k,v) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
@@ -2554,8 +2558,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
     VtDefault(fun () ->
         vernac_hints ~atts dbnames hints)
   | VernacSyntacticDefinition (id,c,b) ->
-    VtDefault(fun () ->
-        with_module_locality ~atts vernac_syntactic_definition id c b)
+    VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
   | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
     VtDefault(fun () ->
         with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))