aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hints.ml')
-rw-r--r--tactics/hints.ml128
1 files changed, 80 insertions, 48 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 85ff02824..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
@@ -828,38 +833,48 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
let cty = if hnf then hnf_constr env sigma cty else cty in
- match EConstr.kind sigma cty with
- | Prod _ ->
- let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
- let ce = mk_clenv_from_env env sigma' None (c,cty) in
- let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
- let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_apply_entry" in
- let nmiss = List.length (clenv_missing ce) in
- let secvars = secvars_of_constr env sigma c in
- let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in
- let pat = match info.hint_pattern with
- | Some p -> snd p | None -> pat
- in
- if Int.equal nmiss 0 then
- (Some hd,
- { pri; poly; pat = Some pat; name;
- db = None;
- secvars;
- code = with_uid (Res_pf(c,cty,ctx)); })
- else begin
- if not eapply then failwith "make_apply_entry";
- if verbose then
- Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++
- str " will only be used by eauto");
- (Some hd,
- { pri; poly; pat = Some pat; name;
- db = None; secvars;
- code = with_uid (ERes_pf(c,cty,ctx)); })
- end
- | _ -> failwith "make_apply_entry"
+ match EConstr.kind sigma cty with
+ | Prod _ ->
+ let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
+ let ce = mk_clenv_from_env env sigma' None (c,cty) in
+ let c' = clenv_type (* ~reduce:false *) ce in
+ let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
+ let hd =
+ try head_pattern_bound pat
+ with BoundPattern -> failwith "make_apply_entry" in
+ let miss = clenv_missing ce in
+ let nmiss = List.length miss in
+ let secvars = secvars_of_constr env sigma c in
+ let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in
+ let pat = match info.hint_pattern with
+ | Some p -> snd p | None -> pat
+ in
+ if Int.equal nmiss 0 then
+ (Some hd,
+ { pri; poly; pat = Some pat; name;
+ db = None;
+ secvars;
+ code = with_uid (Res_pf(c,cty,ctx)); })
+ else begin
+ if not eapply then failwith "make_apply_entry";
+ if verbose then begin
+ let variables = str (CString.plural nmiss "variable") in
+ Feedback.msg_info (
+ strbrk "The hint " ++
+ pr_leconstr_env env sigma' c ++
+ strbrk " will only be used by eauto, because applying " ++
+ pr_leconstr_env env sigma' c ++
+ strbrk " would leave " ++ variables ++ Pp.spc () ++
+ Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++
+ strbrk " as unresolved existential " ++ variables ++ str "."
+ )
+ end;
+ (Some hd,
+ { pri; poly; pat = Some pat; name;
+ db = None; secvars;
+ code = with_uid (ERes_pf(c,cty,ctx)); })
+ end
+ | _ -> failwith "make_apply_entry"
(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose
c is a constr
@@ -1014,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 =
@@ -1032,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
@@ -1122,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'
@@ -1244,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
@@ -1347,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 =
@@ -1369,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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 08:44:35 +0000