aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--dev/ci/user-overlays/07820-mattam82-hints-constants.sh6
-rw-r--r--doc/sphinx/proof-engine/tactics.rst18
-rw-r--r--tactics/hints.ml54
-rw-r--r--tactics/hints.mli9
-rw-r--r--test-suite/success/Hints.v30
-rw-r--r--theories/Init/Logic.v7
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/g_proofs.mlg8
-rw-r--r--vernac/ppvernac.ml5
-rw-r--r--vernac/vernacexpr.ml7
11 files changed, 120 insertions, 29 deletions
diff --git a/CHANGES b/CHANGES
index 886216724..3ec53fad2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -55,6 +55,9 @@ Vernacular Commands
- Added option Uniform Inductive Parameters which abstracts over parameters
before typechecking constructors, allowing to write for example
`Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
+- 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/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
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-08 21:20:59 +0000