Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations

Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle

6 files changed, 116 insertions, 33 deletions

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 5297409cdf..4ef5c1a918 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -915,8 +915,8 @@ let classify_ltac2 = function
 }
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
-  Tac2entries.register_struct ?local e
+| #[ deprecation = deprecation; local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+  Tac2entries.register_struct ?deprecation ?local e
   }
 | ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> {
   fun ~pstate -> Tac2entries.perform_eval ~pstate e
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index faa1e74728..0aa05934bf 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -57,6 +57,7 @@ type tacdef = {
   tacdef_mutable : bool;
   tacdef_expr : glb_tacexpr;
   tacdef_type : type_scheme;
+  tacdef_deprecation : Deprecation.t option;
 }
 
 let perform_tacdef visibility ((sp, kn), def) =
@@ -65,6 +66,7 @@ let perform_tacdef visibility ((sp, kn), def) =
     Tac2env.gdata_expr = def.tacdef_expr;
     gdata_type = def.tacdef_type;
     gdata_mutable = def.tacdef_mutable;
+    gdata_deprecation = def.tacdef_deprecation;
   } in
   Tac2env.define_global kn data
 
@@ -77,6 +79,7 @@ let cache_tacdef ((sp, kn), def) =
     Tac2env.gdata_expr = def.tacdef_expr;
     gdata_type = def.tacdef_type;
     gdata_mutable = def.tacdef_mutable;
+    gdata_deprecation = def.tacdef_deprecation;
   } in
   Tac2env.define_global kn data
 
@@ -322,7 +325,7 @@ let check_lowercase {loc;v=id} =
   if Tac2env.is_constructor (Libnames.qualid_of_ident id) then
     user_err ?loc (str "The identifier " ++ Id.print id ++ str " must be lowercase")
 
-let register_ltac ?(local = false) ?(mut = false) isrec tactics =
+let register_ltac ?deprecation ?(local = false) ?(mut = false) isrec tactics =
   let map ({loc;v=na}, e) =
     let id = match na with
     | Anonymous ->
@@ -359,6 +362,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics =
       tacdef_mutable = mut;
       tacdef_expr = e;
       tacdef_type = t;
+      tacdef_deprecation = deprecation;
     } in
     ignore (Lib.add_leaf id (inTacDef def))
   in
@@ -453,7 +457,7 @@ let register_typedef ?(local = false) isrec types =
   let iter (id, def) = ignore (Lib.add_leaf id (inTypDef def)) in
   List.iter iter types
 
-let register_primitive ?(local = false) {loc;v=id} t ml =
+let register_primitive ?deprecation ?(local = false) {loc;v=id} t ml =
   let t = intern_open_type t in
   let rec count_arrow = function
   | GTypArrow (_, t) -> 1 + count_arrow t
@@ -477,6 +481,7 @@ let register_primitive ?(local = false) {loc;v=id} t ml =
     tacdef_mutable = false;
     tacdef_expr = e;
     tacdef_type = t;
+    tacdef_deprecation = deprecation;
   } in
   ignore (Lib.add_leaf id (inTacDef def))
 
@@ -599,6 +604,18 @@ let parse_token = function
   let loc = loc_of_token tok in
   CErrors.user_err ?loc (str "Invalid parsing token")
 
+let rec print_scope = function
+| SexprStr s -> str s.CAst.v
+| SexprInt i -> int i.CAst.v
+| SexprRec (_, {v=na}, []) -> Option.cata Id.print (str "_") na
+| SexprRec (_, {v=na}, e) ->
+  Option.cata Id.print (str "_") na ++ str "(" ++ pr_sequence print_scope e ++ str ")"
+
+let print_token = function
+| SexprStr {v=s} -> quote (str s)
+| SexprRec (_, {v=na}, [tok]) -> print_scope tok
+| _ -> assert false
+
 end
 
 let parse_scope = ParseToken.parse_scope
@@ -608,6 +625,7 @@ type synext = {
   synext_exp : raw_tacexpr;
   synext_lev : int option;
   synext_loc : bool;
+  synext_depr : Deprecation.t option;
 }
 
 type krule =
@@ -628,10 +646,20 @@ let rec get_rule (tok : scope_rule token list) : krule = match tok with
   let act k _ = act k in
   KRule (rule, act)
 
+let deprecated_ltac2_notation =
+  Deprecation.create_warning
+    ~object_name:"Ltac2 notation"
+    ~warning_name:"deprecated-ltac2-notation"
+    (fun (toks : sexpr list) -> pr_sequence ParseToken.print_token toks)
+
 let perform_notation syn st =
   let tok = List.rev_map ParseToken.parse_token syn.synext_tok in
   let KRule (rule, act) = get_rule tok in
   let mk loc args =
+    let () = match syn.synext_depr with
+    | None -> ()
+    | Some depr -> deprecated_ltac2_notation ~loc (syn.synext_tok, depr)
+    in
     let map (na, e) =
       ((CAst.make ?loc:e.loc @@ CPatVar na), e)
     in
@@ -671,23 +699,24 @@ let inTac2Notation : synext -> obj =
 
 type abbreviation = {
   abbr_body : raw_tacexpr;
+  abbr_depr : Deprecation.t option;
 }
 
 let perform_abbreviation visibility ((sp, kn), abbr) =
   let () = Tac2env.push_ltac visibility sp (TacAlias kn) in
-  Tac2env.define_alias kn abbr.abbr_body
+  Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
 
 let load_abbreviation i obj = perform_abbreviation (Until i) obj
 let open_abbreviation i obj = perform_abbreviation (Exactly i) obj
 
 let cache_abbreviation ((sp, kn), abbr) =
   let () = Tac2env.push_ltac (Until 1) sp (TacAlias kn) in
-  Tac2env.define_alias kn abbr.abbr_body
+  Tac2env.define_alias ?deprecation:abbr.abbr_depr kn abbr.abbr_body
 
 let subst_abbreviation (subst, abbr) =
   let body' = subst_rawexpr subst abbr.abbr_body in
   if body' == abbr.abbr_body then abbr
-  else { abbr_body = body' }
+  else { abbr_body = body'; abbr_depr = abbr.abbr_depr }
 
 let classify_abbreviation o = Substitute o
 
@@ -699,12 +728,12 @@ let inTac2Abbreviation : abbreviation -> obj =
      subst_function = subst_abbreviation;
      classify_function = classify_abbreviation}
 
-let register_notation ?(local = false) tkn lev body = match tkn, lev with
+let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, lev with
 | [SexprRec (_, {loc;v=Some id}, [])], None ->
   (* Tactic abbreviation *)
   let () = check_lowercase CAst.(make ?loc id) in
   let body = Tac2intern.globalize Id.Set.empty body in
-  let abbr = { abbr_body = body } in
+  let abbr = { abbr_body = body; abbr_depr = deprecation } in
   ignore (Lib.add_leaf id (inTac2Abbreviation abbr))
 | _ ->
   (* Check that the tokens make sense *)
@@ -723,6 +752,7 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with
     synext_exp = body;
     synext_lev = lev;
     synext_loc = local;
+    synext_depr = deprecation;
   } in
   Lib.add_anonymous_leaf (inTac2Notation ext)
 
@@ -838,12 +868,21 @@ let perform_eval ~pstate e =
 
 (** Toplevel entries *)
 
-let register_struct ?local str = match str with
-| StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
-| StrTyp (isrec, t) -> register_type ?local isrec t
-| StrPrm (id, t, ml) -> register_primitive ?local id t ml
-| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
-| StrMut (qid, old, e) -> register_redefinition ?local qid old e
+let unsupported_deprecation = function
+| None -> ()
+| Some _ ->
+  Attributes.unsupported_attributes ["deprecated", Attributes.VernacFlagEmpty]
+
+let register_struct ?deprecation ?local str = match str with
+| StrVal (mut, isrec, e) -> register_ltac ?deprecation ?local ~mut isrec e
+| StrTyp (isrec, t) ->
+  let () = unsupported_deprecation deprecation in (* TODO *)
+  register_type ?local isrec t
+| StrPrm (id, t, ml) -> register_primitive ?deprecation ?local id t ml
+| StrSyn (tok, lev, e) -> register_notation ?deprecation ?local tok lev e
+| StrMut (qid, old, e) ->
+  let () = unsupported_deprecation deprecation in (* TODO: what does that mean? *)
+  register_redefinition ?local qid old e
 
 (** Toplevel exception *)
 
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 782968c6e1..a1e13b60fe 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -14,22 +14,19 @@ open Tac2expr
 
 (** {5 Toplevel definitions} *)
 
-val register_ltac : ?local:bool -> ?mut:bool -> rec_flag ->
+val register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> rec_flag ->
   (Names.lname * raw_tacexpr) list -> unit
 
 val register_type : ?local:bool -> rec_flag ->
   (qualid * redef_flag * raw_quant_typedef) list -> unit
 
-val register_primitive : ?local:bool ->
+val register_primitive : ?deprecation:Deprecation.t -> ?local:bool ->
   Names.lident -> raw_typexpr -> ml_tactic_name -> unit
 
-val register_struct
-  :  ?local:bool
-  -> strexpr
-  -> unit
+val register_struct : ?deprecation:Deprecation.t -> ?local:bool -> strexpr -> unit
 
-val register_notation : ?local:bool -> sexpr list -> int option ->
-  raw_tacexpr -> unit
+val register_notation : ?deprecation:Deprecation.t -> ?local:bool -> sexpr list ->
+  int option -> raw_tacexpr -> unit
 
 val perform_eval : pstate:Declare.Proof.t option -> raw_tacexpr -> unit
 
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 5479ba0d54..5eb57c8f9b 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -18,6 +18,7 @@ type global_data = {
   gdata_expr : glb_tacexpr;
   gdata_type : type_scheme;
   gdata_mutable : bool;
+  gdata_deprecation : Deprecation.t option;
 }
 
 type constructor_data = {
@@ -35,12 +36,17 @@ type projection_data = {
   pdata_indx : int;
 }
 
+type alias_data = {
+  alias_body : raw_tacexpr;
+  alias_depr : Deprecation.t option;
+}
+
 type ltac_state = {
   ltac_tactics : global_data KNmap.t;
   ltac_constructors : constructor_data KNmap.t;
   ltac_projections : projection_data KNmap.t;
   ltac_types : glb_quant_typedef KNmap.t;
-  ltac_aliases : raw_tacexpr KNmap.t;
+  ltac_aliases : alias_data KNmap.t;
 }
 
 let empty_state = {
@@ -79,9 +85,10 @@ let define_type kn e =
 
 let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types
 
-let define_alias kn tac =
+let define_alias ?deprecation kn tac =
   let state = !ltac_state in
-  ltac_state := { state with ltac_aliases = KNmap.add kn tac state.ltac_aliases }
+  let data = { alias_body = tac; alias_depr = deprecation } in
+  ltac_state := { state with ltac_aliases = KNmap.add kn data state.ltac_aliases }
 
 let interp_alias kn = KNmap.find kn ltac_state.contents.ltac_aliases
 
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 95dcdd7e1b..3800ad0198 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -23,6 +23,7 @@ type global_data = {
   gdata_expr : glb_tacexpr;
   gdata_type : type_scheme;
   gdata_mutable : bool;
+  gdata_deprecation : Deprecation.t option;
 }
 
 val define_global : ltac_constant -> global_data -> unit
@@ -72,8 +73,13 @@ val interp_projection : ltac_projection -> projection_data
 
 (** {5 Toplevel definition of aliases} *)
 
-val define_alias : ltac_constant -> raw_tacexpr -> unit
-val interp_alias : ltac_constant -> raw_tacexpr
+type alias_data = {
+  alias_body : raw_tacexpr;
+  alias_depr : Deprecation.t option;
+}
+
+val define_alias : ?deprecation:Deprecation.t -> ltac_constant -> raw_tacexpr -> unit
+val interp_alias : ltac_constant -> alias_data
 
 (** {5 Name management} *)
 
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index ddf70a5a65..90c8528203 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -655,6 +655,35 @@ let is_alias env qid = match get_variable env qid with
 | ArgArg (TacAlias _) -> true
 | ArgVar _ | (ArgArg (TacConstant _)) -> false
 
+let is_user_name qid = match qid with
+| AbsKn _ -> false
+| RelId _ -> true
+
+let deprecated_ltac2_alias =
+  Deprecation.create_warning
+    ~object_name:"Ltac2 alias"
+    ~warning_name:"deprecated-ltac2-alias"
+    (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacAlias kn)))
+
+let deprecated_ltac2_def =
+  Deprecation.create_warning
+    ~object_name:"Ltac2 definition"
+    ~warning_name:"deprecated-ltac2-definition"
+    (fun kn -> pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstant kn)))
+
+let check_deprecated_ltac2 ?loc qid def =
+  if is_user_name qid then match def with
+  | TacAlias kn ->
+    begin match (Tac2env.interp_alias kn).alias_depr with
+    | None -> ()
+    | Some depr -> deprecated_ltac2_alias ?loc (kn, depr)
+    end
+  | TacConstant kn ->
+    begin match (Tac2env.interp_global kn).gdata_deprecation with
+    | None -> ()
+    | Some depr -> deprecated_ltac2_def ?loc (kn, depr)
+    end
+
 let rec intern_rec env {loc;v=e} = match e with
 | CTacAtm atm -> intern_atm env atm
 | CTacRef qid ->
@@ -663,11 +692,12 @@ let rec intern_rec env {loc;v=e} = match e with
     let sch = Id.Map.find id env.env_var in
     (GTacVar id, fresh_mix_type_scheme env sch)
   | ArgArg (TacConstant kn) ->
-    let { Tac2env.gdata_type = sch } =
+    let { Tac2env.gdata_type = sch; gdata_deprecation = depr } =
       try Tac2env.interp_global kn
       with Not_found ->
         CErrors.anomaly (str "Missing hardwired primitive " ++ KerName.print kn)
     in
+    let () = check_deprecated_ltac2 ?loc qid (TacConstant kn) in
     (GTacRef kn, fresh_type_scheme env sch)
   | ArgArg (TacAlias kn) ->
     let e =
@@ -675,7 +705,8 @@ let rec intern_rec env {loc;v=e} = match e with
       with Not_found ->
         CErrors.anomaly (str "Missing hardwired alias " ++ KerName.print kn)
     in
-    intern_rec env e
+    let () = check_deprecated_ltac2 ?loc qid (TacAlias kn) in
+    intern_rec env e.alias_body
   end
 | CTacCst qid ->
   let kn = get_constructor env qid in
@@ -695,12 +726,13 @@ let rec intern_rec env {loc;v=e} = match e with
 | CTacApp ({loc;v=CTacCst qid}, args) ->
   let kn = get_constructor env qid in
   intern_constructor env loc kn args
-| CTacApp ({v=CTacRef qid}, args) when is_alias env qid ->
+| CTacApp ({v=CTacRef qid; loc=aloc}, args) when is_alias env qid ->
   let kn = match get_variable env qid with
   | ArgArg (TacAlias kn) -> kn
   | ArgVar _ | (ArgArg (TacConstant _)) -> assert false
   in
   let e = Tac2env.interp_alias kn in
+  let () = check_deprecated_ltac2 ?loc:aloc qid (TacAlias kn) in
   let map arg =
     (* Thunk alias arguments *)
     let loc = arg.loc in
@@ -709,7 +741,7 @@ let rec intern_rec env {loc;v=e} = match e with
     CAst.make ?loc @@ CTacFun ([var], arg)
   in
   let args = List.map map args in
-  intern_rec env (CAst.make ?loc @@ CTacApp (e, args))
+  intern_rec env (CAst.make ?loc @@ CTacApp (e.alias_body, args))
 | CTacApp (f, args) ->
   let loc = f.loc in
   let (f, ft) = intern_rec env f in
@@ -1243,7 +1275,9 @@ let rec globalize ids ({loc;v=er} as e) = match er with
   let mem id = Id.Set.mem id ids in
   begin match get_variable0 mem ref with
   | ArgVar _ -> e
-  | ArgArg kn -> CAst.make ?loc @@ CTacRef (AbsKn kn)
+  | ArgArg kn ->
+    let () = check_deprecated_ltac2 ?loc ref kn in
+    CAst.make ?loc @@ CTacRef (AbsKn kn)
   end
 | CTacCst qid ->
   let knc = get_constructor () qid in