From 8d02317cc02ae5d007f5d2486d26bb37865ca0a9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 30 Mar 2017 16:28:21 +0200 Subject: hints: add Hint Variables/Constants Opaque/Transparent commands This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables --- CHANGES | 3 +++ doc/sphinx/proof-engine/tactics.rst | 18 ++++++++----- tactics/hints.ml | 54 ++++++++++++++++++++++++++----------- tactics/hints.mli | 9 +++++-- test-suite/success/Hints.v | 30 +++++++++++++++++++++ theories/Init/Logic.v | 7 +++++ vernac/classes.ml | 2 +- vernac/g_proofs.mlg | 8 ++++-- vernac/ppvernac.ml | 5 +++- vernac/vernacexpr.ml | 7 ++++- 10 files changed, 114 insertions(+), 29 deletions(-) diff --git a/CHANGES b/CHANGES index 75f4df06a..9a5dade03 100644 --- a/CHANGES +++ b/CHANGES @@ -52,6 +52,9 @@ Vernacular Commands - Nested proofs may be enabled through the option `Nested Proofs Allowed`. By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. +- New Set Hint Variables/Constants Opaque/Transparent commands for setting + globally the opacity flag of variables and constants in hint databases, + overwritting the opacity set of the hint database. Coq binaries and process model diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index d0a0d568e..45667b099 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3422,18 +3422,24 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds each :n:`Hint Unfold @ident`. - .. cmdv:: Hint %( Transparent %| Opaque %) @qualid - :name: Hint ( Transparent | Opaque ) + .. cmdv:: Hint Transparent {+ @qualid} + Hint Opaque {+ @qualid} + :name: Hint Transparent; Hint Opaque - This adds a transparency hint to the database, making :n:`@qualid` a - transparent or opaque constant during resolution. This information is used + This adds transparency hints to the database, making :n:`@qualid` + transparent or opaque constants during resolution. This information is used during unification of the goal with any lemma in the database and inside the discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint %( Transparent %| Opaque %) {+ @ident} + .. cmdv:: Hint Variables %( Transparent %| Opaque %) + Hint Constants %( Transparent %| Opaque %) + :name: Hint Variables; Hint Constants - Declares each :n:`@ident` as a transparent or opaque constant. + This sets the transparency flag used during unification of + hints in the database for all constants or all variables, + overwritting the existing settings of opacity. It is advised + to use this just after a :cmd:`Create HintDb` command. .. cmdv:: Hint Extern @num {? @pattern} => @tactic :name: Hint Extern diff --git a/tactics/hints.ml b/tactics/hints.ml index d28d4848c..748e0362c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -165,12 +165,17 @@ type hint_mode = | ModeNoHeadEvar (* No evar at the head *) | ModeOutput (* Anything *) +type 'a hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of qualid list - | HintsTransparency of qualid list * bool + | HintsTransparency of qualid hints_transparency_target * bool | HintsMode of qualid * hint_mode list | HintsConstructors of qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument @@ -1024,15 +1029,19 @@ let add_hint dbname hintlist = let db' = Hint_db.add_list env sigma hintlist db in searchtable_add (dbname,db') -let add_transparency dbname grs b = +let add_transparency dbname target b = let db = get_db dbname in - let st = Hint_db.transparent_state db in + let (ids, csts as st) = Hint_db.transparent_state db in let st' = - List.fold_left (fun (ids, csts) gr -> - match gr with - | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts) - | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts) - st grs + match target with + | HintsVariables -> (if b then Id.Pred.full else Id.Pred.empty), csts + | HintsConstants -> ids, if b then Cpred.full else Cpred.empty + | HintsReferences grs -> + List.fold_left (fun (ids, csts) gr -> + match gr with + | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts) + | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts) + st grs in searchtable_add (dbname, Hint_db.set_transparent_state db st') let remove_hint dbname grs = @@ -1042,7 +1051,7 @@ let remove_hint dbname grs = type hint_action = | CreateDB of bool * transparent_state - | AddTransparency of evaluable_global_reference list * bool + | AddTransparency of evaluable_global_reference hints_transparency_target * bool | AddHints of hint_entry list | RemoveHints of GlobRef.t list | AddCut of hints_path @@ -1132,9 +1141,17 @@ let subst_autohint (subst, obj) = in let action = match obj.hint_action with | CreateDB _ -> obj.hint_action - | AddTransparency (grs, b) -> - let grs' = List.Smart.map (subst_evaluable_reference subst) grs in - if grs == grs' then obj.hint_action else AddTransparency (grs', b) + | AddTransparency (target, b) -> + let target' = + match target with + | HintsVariables -> target + | HintsConstants -> target + | HintsReferences grs -> + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in + if grs == grs' then target + else HintsReferences grs' + in + if target' == target then obj.hint_action else AddTransparency (target', b) | AddHints hintlist -> let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' @@ -1254,7 +1271,7 @@ type hints_entry = | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list - | HintsTransparencyEntry of evaluable_global_reference list * bool + | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument @@ -1357,14 +1374,19 @@ let interp_hints poly = let info = { info with hint_pattern = Option.map fp info.hint_pattern } in (info, poly, b, path, gr) in + let ft = function + | HintsVariables -> HintsVariables + | HintsConstants -> HintsConstants + | HintsReferences lhints -> HintsReferences (List.map fr lhints) + in + let fp = Constrintern.intern_constr_pattern (Global.env()) in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) | HintsResolveIFF (l2r, lc, n) -> HintsResolveEntry (List.map (project_hint ~poly n l2r) lc) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) - | HintsTransparency (lhints, b) -> - HintsTransparencyEntry (List.map fr lhints, b) + | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b) | HintsMode (r, l) -> HintsModeEntry (fref r, l) | HintsConstructors lqid -> let constr_hints_of_ind qid = @@ -1379,7 +1401,7 @@ let interp_hints poly = PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> - let pat = Option.map fp patcom in + let pat = Option.map (fp sigma) patcom in let l = match pat with None -> [] | Some (l, _) -> l in let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in diff --git a/tactics/hints.mli b/tactics/hints.mli index ca18f835a..9bf6c175a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -81,12 +81,17 @@ type hint_mode = | ModeNoHeadEvar (* No evar at the head *) | ModeOutput (* Anything *) +type 'a hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsResolveIFF of bool * Libnames.qualid list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.qualid list - | HintsTransparency of Libnames.qualid list * bool + | HintsTransparency of Libnames.qualid hints_transparency_target * bool | HintsMode of Libnames.qualid * hint_mode list | HintsConstructors of Libnames.qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument @@ -173,7 +178,7 @@ type hints_entry = | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list - | HintsTransparencyEntry of evaluable_global_reference list * bool + | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 717dc0deb..ebf5b094e 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -183,3 +183,33 @@ End HintCut. Goal forall (m : nat), exists n, m = n /\ m = n. intros m; eexists; split; [trivial | reflexivity]. Qed. + +Section HintTransparent. + + Definition fn (x : nat) := S x. + + Create HintDb trans. + + Hint Resolve eq_refl | (_ = _) : trans. + + (* No reduction *) + Hint Variables Opaque : trans. Hint Constants Opaque : trans. + + Goal forall x : nat, fn x = S x. + Proof. + intros. + Fail typeclasses eauto with trans. + unfold fn. + typeclasses eauto with trans. + Qed. + + (** Now allow unfolding fn *) + Hint Constants Transparent : trans. + + Goal forall x : nat, fn x = S x. + Proof. + intros. + typeclasses eauto with trans. + Qed. + +End HintTransparent. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 10ca9ecc9..817581cb2 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -29,6 +29,13 @@ Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope. +(** Create the "core" hint database, and set its transparent state for + variables and constants explicitely. *) + +Create HintDb core. +Hint Variables Opaque : core. +Hint Constants Opaque : core. + Hint Unfold not: core. (** [and A B], written [A /\ B], is the conjunction of [A] and [B] diff --git a/vernac/classes.ml b/vernac/classes.ml index 26d105ecf..bf734ab36 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -42,7 +42,7 @@ let typeclasses_db = "typeclass_instances" let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] - (Hints.HintsTransparencyEntry ([c], b)) + (Hints.HintsTransparencyEntry (Vernacexpr.HintsReferences [c], b)) let _ = Hook.set Typeclasses.add_instance_hint_hook diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 72db53f68..cccdbfc91 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -117,8 +117,12 @@ GRAMMAR EXTEND Gram | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural -> { HintsResolveIFF (false, lc, n) } | IDENT "Immediate"; lc = LIST1 reference_or_constr -> { HintsImmediate lc } - | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (lc, true) } - | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (lc, false) } + | IDENT "Variables"; IDENT "Transparent" -> { HintsTransparency (HintsVariables, true) } + | IDENT "Variables"; IDENT "Opaque" -> { HintsTransparency (HintsVariables, false) } + | IDENT "Constants"; IDENT "Transparent" -> { HintsTransparency (HintsConstants, true) } + | IDENT "Constants"; IDENT "Opaque" -> { HintsTransparency (HintsConstants, false) } + | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, true) } + | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, false) } | IDENT "Mode"; l = global; m = mode -> { HintsMode (l, m) } | IDENT "Unfold"; lqid = LIST1 global -> { HintsUnfold lqid } | IDENT "Constructors"; lc = LIST1 global -> { HintsConstructors lc } ] ] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 56dfaa54a..5fbe1f4e4 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -210,7 +210,10 @@ open Pputils | HintsTransparency (l, b) -> keyword (if b then "Transparent" else "Opaque") ++ spc () - ++ prlist_with_sep sep pr_qualid l + ++ (match l with + | HintsVariables -> keyword "Variables" + | HintsConstants -> keyword "Constants" + | HintsReferences l -> prlist_with_sep sep pr_qualid l) | HintsMode (m, l) -> keyword "Mode" ++ spc () diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index f74383b02..f5f37339c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -121,12 +121,17 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = type hint_info_expr = Hints.hint_info_expr [@@ocaml.deprecated "Please use [Hints.hint_info_expr]"] +type 'a hints_transparency_target = 'a Hints.hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of Hints.reference_or_constr list | HintsUnfold of qualid list - | HintsTransparency of qualid list * bool + | HintsTransparency of qualid hints_transparency_target * bool | HintsMode of qualid * Hints.hint_mode list | HintsConstructors of qualid list | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument -- cgit v1.2.3 From bc5304a91cf4627063551422ad6e5a2cd1059897 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 24 Jun 2018 15:55:36 +0200 Subject: Add Equations overlay --- dev/ci/user-overlays/07820-mattam82-hints-constants.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 dev/ci/user-overlays/07820-mattam82-hints-constants.sh diff --git a/dev/ci/user-overlays/07820-mattam82-hints-constants.sh b/dev/ci/user-overlays/07820-mattam82-hints-constants.sh new file mode 100644 index 000000000..2ae86ae22 --- /dev/null +++ b/dev/ci/user-overlays/07820-mattam82-hints-constants.sh @@ -0,0 +1,6 @@ +_OVERLAY_BRANCH=hints-variables-overlay + +if [ "$CI_PULL_REQUEST" = "7820" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" +fi -- cgit v1.2.3