Merge PR #10180: `deprecated` attribute support for notations and syntactic definitions

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin

7 files changed, 101 insertions, 52 deletions

diff --git a/interp/deprecation.ml b/interp/deprecation.ml
new file mode 100644
index 0000000000..b6f0dceb89
--- /dev/null
+++ b/interp/deprecation.ml
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type t = { since : string option ; note : string option }
+
+let make ?since ?note () = { since ; note }
+
+let create_warning ~object_name ~warning_name name_printer =
+  let open Pp in
+  CWarnings.create ~name:warning_name ~category:"deprecated"
+    (fun (qid,depr) -> str object_name ++ spc () ++ name_printer qid ++
+      strbrk " is deprecated" ++
+      pr_opt (fun since -> str "since " ++ str since) depr.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.note)
diff --git a/interp/deprecation.mli b/interp/deprecation.mli
new file mode 100644
index 0000000000..aab87c11a2
--- /dev/null
+++ b/interp/deprecation.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type t = { since : string option ; note : string option }
+
+val make : ?since:string -> ?note:string -> unit -> t
+
+val create_warning : object_name:string -> warning_name:string ->
+  ('b -> Pp.t) -> ?loc:Loc.t -> 'b * t -> unit
diff --git a/interp/interp.mllib b/interp/interp.mllib
index b65a171ef9..52978a2ab6 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+Deprecation
 NumTok
 Constrexpr
 Tactypes
diff --git a/interp/notation.ml b/interp/notation.ml
index a7bac96d31..cc06d5abfc 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -72,6 +72,7 @@ type notation_location = (DirPath.t * DirPath.t) * string
 type notation_data = {
   not_interp : interpretation;
   not_location : notation_location;
+  not_deprecation : Deprecation.t option;
 }
 
 type scope = {
@@ -1095,7 +1096,7 @@ let warn_notation_overridden =
                     str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
                     ++ strbrk "was already used" ++ which_scope ++ str ".")
 
-let declare_notation_interpretation ntn scopt pat df ~onlyprint =
+let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   if not onlyprint then begin
@@ -1109,6 +1110,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
     let notdata = {
       not_interp = pat;
       not_location = df;
+      not_deprecation = deprecation;
     } in
     let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in
     scope_map := String.Map.add scope sc !scope_map
@@ -1125,10 +1127,10 @@ let declare_uninterpretation rule (metas,c as pat) =
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
   | Scope scope :: scopes ->
-      (try let (pat,df) = find scope in pat,(df,Some scope)
+      (try let n = find scope in (n,Some scope)
        with Not_found -> find_interpretation ntn find scopes)
   | SingleNotation ntn'::scopes when notation_eq ntn' ntn ->
-      (try let (pat,df) = find default_scope in pat,(df,None)
+      (try let n = find default_scope in (n,None)
        with Not_found ->
          (* e.g. because single notation only for constr, not cases_pattern *)
          find_interpretation ntn find scopes)
@@ -1136,8 +1138,7 @@ let rec find_interpretation ntn find = function
       find_interpretation ntn find scopes
 
 let find_notation ntn sc =
-  let n = NotationMap.find ntn (find_scope sc).notations in
-  (n.not_interp, n.not_location)
+  NotationMap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
   | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
@@ -1147,7 +1148,9 @@ let notation_of_prim_token = function
 let find_prim_token check_allowed ?loc p sc =
   (* Try for a user-defined numerical notation *)
   try
-    let (_,c),df = find_notation (notation_of_prim_token p) sc in
+    let n = find_notation (notation_of_prim_token p) sc in
+    let (_,c) = n.not_interp in
+    let df = n.not_location in
     let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in
     check_allowed pat;
     pat, df
@@ -1167,7 +1170,9 @@ let find_prim_token check_allowed ?loc p sc =
 let interp_prim_token_gen ?loc g p local_scopes =
   let scopes = make_current_scopes local_scopes in
   let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
-  try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
+  try
+    let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
+    pat, (loc,sc)
   with Not_found ->
     user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
@@ -1192,11 +1197,18 @@ let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function
 let interp_prim_token_cases_pattern_expr ?loc looked_for p =
   interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p
 
+let warn_deprecated_notation =
+  Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-notation"
+    pr_notation
+
 let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
-  try find_interpretation ntn (find_notation ntn) scopes
+  try
+    let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
+    Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation;
+    n.not_interp, (n.not_location, sc)
   with Not_found ->
-    user_err ?loc 
+    user_err ?loc
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
 let uninterp_notations c =
diff --git a/interp/notation.mli b/interp/notation.mli
index a67948a778..b32561d908 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -217,7 +217,8 @@ type interp_rule =
   | SynDefRule of KerName.t
 
 val declare_notation_interpretation : notation -> scope_name option ->
-      interpretation -> notation_location -> onlyprint:bool -> unit
+  interpretation -> notation_location -> onlyprint:bool ->
+  Deprecation.t option -> unit
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a7e1de736c..8df04187f1 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -19,20 +19,24 @@ open Notation_term
 
 (* Syntactic definitions. *)
 
-type version = Flags.compat_version option
+type syndef =
+  { syndef_pattern : interpretation;
+    syndef_onlyparsing : bool;
+    syndef_deprecation : Deprecation.t option;
+  }
 
 let syntax_table =
-  Summary.ref (KNmap.empty : (interpretation*version) KNmap.t)
-    ~name:"SYNTAXCONSTANT"
+  Summary.ref (KNmap.empty : syndef KNmap.t)
+    ~name:"SYNDEFS"
 
-let add_syntax_constant kn c onlyparse =
-  syntax_table := KNmap.add kn (c,onlyparse) !syntax_table
+let add_syntax_constant kn syndef =
+  syntax_table := KNmap.add kn syndef !syntax_table
 
-let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(_local,syndef)) =
   if Nametab.exists_cci sp then
     user_err ~hdr:"cache_syntax_constant"
       (Id.print (basename sp) ++ str " already exists");
-  add_syntax_constant kn pat onlyparse;
+  add_syntax_constant kn syndef;
   Nametab.push_syndef (Nametab.Until i) sp kn
 
 let is_alias_of_already_visible_name sp = function
@@ -42,30 +46,29 @@ let is_alias_of_already_visible_name sp = function
   | _ ->
       false
 
-let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
+let open_syntax_constant i ((sp,kn),(_local,syndef)) =
+  let pat = syndef.syndef_pattern in
   if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
     Nametab.push_syndef (Nametab.Exactly i) sp kn;
-    match onlyparse with
-    | None ->
+    if not syndef.syndef_onlyparsing then
       (* Redeclare it to be used as (short) name in case an other (distfix)
          notation was declared in between *)
       Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
-    | _ -> ()
   end
 
 let cache_syntax_constant d =
   load_syntax_constant 1 d;
   open_syntax_constant 1 d
 
-let subst_syntax_constant (subst,(local,pat,onlyparse)) =
-  (local,Notation_ops.subst_interpretation subst pat,onlyparse)
+let subst_syntax_constant (subst,(local,syndef)) =
+  let syndef_pattern = Notation_ops.subst_interpretation subst syndef.syndef_pattern in
+  (local, { syndef with syndef_pattern })
 
-let classify_syntax_constant (local,_,_ as o) =
+let classify_syntax_constant (local,_ as o) =
   if local then Dispose else Substitute o
 
-let in_syntax_constant
- : bool * interpretation * Flags.compat_version option -> obj =
-  declare_object {(default_object "SYNTAXCONSTANT") with
+let in_syntax_constant : (bool * syndef) -> obj =
+  declare_object {(default_object "SYNDEF") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
     open_function = open_syntax_constant;
@@ -79,36 +82,31 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
 let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
 
-let declare_syntactic_definition local id onlyparse pat =
-  let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
-
-let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
-
-let pr_compat_warning (kn, def, v) =
-  let pp_def = match def with
-    | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r
-    | _ -> strbrk " is a compatibility notation"
+let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
+  let syndef =
+    { syndef_pattern = in_pat pat;
+      syndef_onlyparsing = onlyparsing;
+      syndef_deprecation = deprecation;
+    }
   in
-  pr_syndef kn ++ pp_def
+  let _ = add_leaf id (in_syntax_constant (local,syndef)) in ()
 
-let warn_compatibility_notation =
-  CWarnings.(create ~name:"compatibility-notation"
-                    ~category:"deprecated" ~default:Enabled pr_compat_warning)
+let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)
 
-let verbose_compat ?loc kn def = function
-  | Some v when Flags.version_strictly_greater v ->
-     warn_compatibility_notation ?loc (kn, def, v)
-  | _ -> ()
+let warn_deprecated_syntactic_definition =
+  Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition"
+    pr_syndef
 
 let search_syntactic_definition ?loc kn =
-  let pat,v = KNmap.find kn !syntax_table in
-  let def = out_pat pat in
-  verbose_compat ?loc kn def v;
+  let syndef = KNmap.find kn !syntax_table in
+  let def = out_pat syndef.syndef_pattern in
+  Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
   def
 
 let search_filtered_syntactic_definition ?loc filter kn =
-  let pat,v = KNmap.find kn !syntax_table in
-  let def = out_pat pat in
+  let syndef = KNmap.find kn !syntax_table in
+  let def = out_pat syndef.syndef_pattern in
   let res = filter def in
-  (match res with Some _ -> verbose_compat ?loc kn def v | None -> ());
+  if Option.has_some res then
+    Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
   res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 77873f8f67..e6e3b9cffa 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -15,8 +15,8 @@ open Notation_term
 
 type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 
-val declare_syntactic_definition : bool -> Id.t ->
-  Flags.compat_version option -> syndef_interpretation -> unit
+val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
+  onlyparsing:bool -> syndef_interpretation -> unit
 
 val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation