From 8cdaa1b5c485ed351f9b3bf212ec5d88f8561908 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 12 Jun 2018 17:02:34 +0200 Subject: Deprecating the declaration of arbitrary terms as hints. We restrict hints to be global references, so as to further simplify the implementation. Allowing arbitrary terms makes it difficult or expensive to handle properly some actions like universe contexts or hint equality. Ultimately, the IsConstr constructor for hints should also be removed. --- .../07-commands-and-options/7791-deprecate-hint-constr.rst | 5 +++++ vernac/g_proofs.mlg | 11 ++++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst diff --git a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst new file mode 100644 index 0000000000..d2af6a4ca7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + Deprecated the declaration of arbitrary terms as hints. Global + references are now mandatory. + (`#7791 `_, + by Pierre-Marie Pédrot). diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 03dfc576a1..596b04f7e3 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -43,6 +43,13 @@ let warn_deprecated_unfocus = CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" (fun () -> Pp.strbrk "The Unfocus command is deprecated") +let warn_deprecated_hint_constr = + CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + (fun () -> + Pp.strbrk + "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" + ) + } (* Proof commands *) @@ -107,7 +114,9 @@ GRAMMAR EXTEND Gram ] ]; reference_or_constr: [ [ r = global -> { HintsReference r } - | c = constr -> { HintsConstr c } ] ] + | c = constr -> + { warn_deprecated_hint_constr ~loc (); + HintsConstr c } ] ] ; hint: [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> -- cgit v1.2.3 From 3034319a2f52baeca172a33eb98b20b3e559201f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 3 Feb 2020 10:29:14 +0100 Subject: Adapt the documentation after deprecation of term hints. Interestingly, the documentation for Hint Resolve -> qualid was outdated. It was claiming that any term would be accepted, but actually with this particular syntax, only qualified names would be parsed already. --- doc/sphinx/proof-engine/tactics.rst | 44 ++++++++++++++++++------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2fa4f1fa42..aee62f1b27 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3761,18 +3761,18 @@ automatically created. Local is useless since hints do not survive anyway to the closure of sections. - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident + .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve - This command adds :n:`simple apply @term` to the hint list with the head - symbol of the type of :n:`@term`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The + This command adds :n:`simple apply @qualid` to the hint list with the head + symbol of the type of :n:`@qualid`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@term` does not start with a product the tactic added in the hint list - is :n:`exact @term`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @term` is also stored in - the hints list. If the inferred type of :n:`@term` contains a dependent + :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@qualid` does not start with a product the tactic added in the hint list + is :n:`exact @qualid`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @qualid` is also stored in + the hints list. If the inferred type of :n:`@qualid` contains a dependent quantification on a variable which occurs only in the premisses of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is added to the hint list @@ -3780,32 +3780,32 @@ automatically created. typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable + The head symbol of the type of :n:`@qualid` is a bound variable such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} : @ident + .. cmdv:: Hint Resolve {+ @qualid} : @ident - Adds each :n:`Hint Resolve @term`. + Adds each :n:`Hint Resolve @qualid`. - .. cmdv:: Hint Resolve -> @term : @ident + .. cmdv:: Hint Resolve -> @qualid : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentioned + the hint will be used as :n:`apply <- @qualid`, although as mentioned before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Hint Resolve <- @term + .. cmdv:: Hint Resolve <- @qualid Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term : @ident + .. cmdv:: Hint Immediate @qualid : @ident :name: Hint Immediate - This command adds :n:`simple apply @term; trivial` to the hint list associated + This command adds :n:`simple apply @qualid; trivial` to the hint list associated with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @term` are + tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are not solved immediately by the :tacn:`trivial` tactic (which only tries tactics with cost 0).This command is useful for theorems such as the symmetry of equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited @@ -3813,12 +3813,12 @@ automatically created. never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` itself. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint :undocumented: - .. cmdv:: Hint Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @qualid} : @ident - Adds each :n:`Hint Immediate @term`. + Adds each :n:`Hint Immediate @qualid`. .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors -- cgit v1.2.3 From eabde14cce66553f9ba7b583507af51973ded850 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 28 Feb 2020 10:29:01 +0100 Subject: Move the warning code out of the parser. --- tactics/hints.ml | 11 ++++++++++- vernac/g_proofs.mlg | 11 +---------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index 86aa046586..731792e34e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1325,6 +1325,13 @@ let project_hint ~poly pri l2r r = let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) +let warn_deprecated_hint_constr = + CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + (fun () -> + Pp.strbrk + "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" + ) + let interp_hints ~poly = fun h -> let env = Global.env () in @@ -1349,7 +1356,9 @@ let interp_hints ~poly = | HintsReference c -> let gr = global_with_alias c in (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> (PathAny, poly, f poly c) + | HintsConstr c -> + let () = warn_deprecated_hint_constr () in + (PathAny, poly, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 596b04f7e3..03dfc576a1 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -43,13 +43,6 @@ let warn_deprecated_unfocus = CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" (fun () -> Pp.strbrk "The Unfocus command is deprecated") -let warn_deprecated_hint_constr = - CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" - (fun () -> - Pp.strbrk - "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" - ) - } (* Proof commands *) @@ -114,9 +107,7 @@ GRAMMAR EXTEND Gram ] ]; reference_or_constr: [ [ r = global -> { HintsReference r } - | c = constr -> - { warn_deprecated_hint_constr ~loc (); - HintsConstr c } ] ] + | c = constr -> { HintsConstr c } ] ] ; hint: [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> -- cgit v1.2.3 From db4cbfef3226cd999b3554b9b8160bc331f45c05 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 28 Feb 2020 10:34:29 +0100 Subject: Deprecate the OCaml API to declare term Hints. --- tactics/class_tactics.ml | 3 ++- tactics/hints.mli | 2 +- vernac/classes.ml | 4 +++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 28feeecb86..02186f6a98 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -528,9 +528,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> + let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info ~poly:false - (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) + h) hints) else [] in diff --git a/tactics/hints.mli b/tactics/hints.mli index 9c9f0b7708..7bb17489bf 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -181,7 +181,7 @@ type hnf = bool type hint_term = | IsGlobRef of GlobRef.t - | IsConstr of constr * Univ.ContextSet.t + | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"] type hints_entry = | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list diff --git a/vernac/classes.ml b/vernac/classes.ml index b92c9e9b71..16b9e07fb2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -60,7 +60,9 @@ let add_instance check inst = let local = is_local_for_hint inst in add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path + List.iter (fun (path, pri, c) -> + let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in + add_instance_hint h path local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) -- cgit v1.2.3