aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/auto.ml27
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/class_tactics.ml51
-rw-r--r--tactics/eauto.ml17
-rw-r--r--tactics/hints.ml63
-rw-r--r--tactics/hints.mli2
6 files changed, 79 insertions, 85 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4ed01d4e65..f041af1db1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -69,7 +69,7 @@ let auto_unif_flags =
(* Try unification with the precompiled clause, then use registered Apply *)
-let connect_hint_clenv ~poly h gl =
+let connect_hint_clenv h gl =
let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
(* [clenv] has been generated by a hint-making function, so the only relevant
data in its evarmap is the set of metas. The [evar_reset_evd] function
@@ -78,7 +78,7 @@ let connect_hint_clenv ~poly h gl =
let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
(* Still, we need to update the universes *)
let clenv, c =
- if poly then
+ if h.hint_poly then
(* Refresh the instance of the hint *)
let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let emap c = Vars.subst_univs_level_constr subst c in
@@ -96,22 +96,22 @@ let connect_hint_clenv ~poly h gl =
{ clenv with evd = evd ; env = Proofview.Goal.env gl }, c
in clenv, c
-let unify_resolve ~poly flags (h : hint) =
+let unify_resolve flags (h : hint) =
Proofview.Goal.enter begin fun gl ->
- let clenv, c = connect_hint_clenv ~poly h gl in
+ let clenv, c = connect_hint_clenv h gl in
let clenv = clenv_unique_resolver ~flags clenv gl in
Clenvtac.clenv_refine clenv
end
-let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h
+let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
-let unify_resolve_gen ~poly = function
- | None -> unify_resolve_nodelta poly
- | Some flags -> unify_resolve ~poly flags
+let unify_resolve_gen = function
+ | None -> unify_resolve_nodelta
+ | Some flags -> unify_resolve flags
-let exact poly h =
+let exact h =
Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv ~poly h gl in
+ let clenv', c = connect_hint_clenv h gl in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
(exact_check c)
@@ -383,16 +383,15 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
(local_db::db_list)
and tac_of_hint dbg db_list local_db concl (flags, h) =
- let poly = FullHint.is_polymorphic h in
let tactic = function
- | Res_pf h -> unify_resolve_gen ~poly flags h
+ | Res_pf h -> unify_resolve_gen flags h
| ERes_pf _ -> Proofview.Goal.enter (fun gl ->
let info = Exninfo.reify () in
Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
- | Give_exact h -> exact poly h
+ | Give_exact h -> exact h
| Res_pf_THEN_trivial_fail h ->
Tacticals.New.tclTHEN
- (unify_resolve_gen ~poly flags h)
+ (unify_resolve_gen flags h)
(* With "(debug) trivial", we shouldn't end here, and
with "debug auto" we don't display the details of inner trivial *)
(trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 9be58cb3fa..903da143d2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ val default_search_depth : int ref
val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
val connect_hint_clenv
- : poly:bool -> hint -> Proofview.Goal.t -> clausenv * constr
+ : hint -> Proofview.Goal.t -> clausenv * constr
(** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : poly:bool -> Unification.unify_flags -> hint -> unit Proofview.tactic
+val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic
(** [ConclPattern concl pat tacast]:
if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fe7b62b316..484aab2f00 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,13 +144,13 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
resolve_evars = false
}
-let e_give_exact flags poly h =
+let e_give_exact flags h =
let { hint_term = c; hint_clnv = clenv } = h in
let open Tacmach.New in
Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
let c, sigma =
- if poly then
+ if h.hint_poly then
let clenv', subst = Clenv.refresh_undefined_univs clenv in
let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
let c = Vars.subst_univs_level_constr subst c in
@@ -173,24 +173,24 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
end
-let unify_e_resolve poly flags = begin fun gls (h, _) ->
- let clenv', c = connect_hint_clenv ~poly h gls in
+let unify_e_resolve flags = begin fun gls (h, _) ->
+ let clenv', c = connect_hint_clenv h gls in
clenv_unique_resolver_tac true ~flags clenv' end
-let unify_resolve poly flags = begin fun gls (h, _) ->
- let clenv', _ = connect_hint_clenv ~poly h gls in
+let unify_resolve flags = begin fun gls (h, _) ->
+ let clenv', _ = connect_hint_clenv h gls in
clenv_unique_resolver_tac false ~flags clenv'
end
(** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine poly flags gls (h, n) =
+let unify_resolve_refine flags gls (h, n) =
let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in
let open Clenv in
let env = Proofview.Goal.env gls in
let concl = Proofview.Goal.concl gls in
Refine.refine ~typecheck:false begin fun sigma ->
let sigma, term, ty =
- if poly then
+ if h.hint_poly then
let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let map c = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
@@ -207,9 +207,9 @@ let unify_resolve_refine poly flags gls (h, n) =
env sigma' cl.cl_concl concl)
in (sigma', term) end
-let unify_resolve_refine poly flags gl clenv =
+let unify_resolve_refine flags gl clenv =
Proofview.tclORELSE
- (unify_resolve_refine poly flags gl clenv)
+ (unify_resolve_refine flags gl clenv)
(fun (exn,info) ->
match exn with
| Evarconv.UnableToUnify _ ->
@@ -222,8 +222,8 @@ let unify_resolve_refine poly flags gl clenv =
(** Dealing with goals of the form A -> B and hints of the form
C -> A -> B.
*)
-let clenv_of_prods poly nprods h gl =
- let { hint_term = c; hint_clnv = clenv } = h in
+let clenv_of_prods nprods h gl =
+ let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
if poly || Int.equal nprods 0 then Some (None, clenv)
else
let sigma = Tacmach.New.project gl in
@@ -235,10 +235,10 @@ let clenv_of_prods poly nprods h gl =
mk_clenv_from_n gl (Some diff) (c,ty))
else None
-let with_prods nprods poly h f =
+let with_prods nprods h f =
if get_typeclasses_limit_intros () then
Proofview.Goal.enter begin fun gl ->
- try match clenv_of_prods poly nprods h gl with
+ try match clenv_of_prods nprods h gl with
| None ->
let info = Exninfo.reify () in
Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
@@ -351,33 +351,32 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
let tac_of_hint =
fun (flags, h) ->
let b = FullHint.priority h in
- let poly = FullHint.is_polymorphic h in
let p = FullHint.pattern h in
let name = FullHint.name h in
let tac = function
| Res_pf h ->
if get_typeclasses_filtered_unification () then
let tac =
- with_prods nprods poly h
+ with_prods nprods h
(fun gl clenv ->
matches_pattern concl p <*>
- unify_resolve_refine poly flags gl clenv)
+ unify_resolve_refine flags gl clenv)
in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
let tac =
- with_prods nprods poly h (unify_resolve poly flags) in
+ with_prods nprods h (unify_resolve flags) in
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| ERes_pf h ->
if get_typeclasses_filtered_unification () then
- let tac = (with_prods nprods poly h
+ let tac = (with_prods nprods h
(fun gl clenv ->
matches_pattern concl p <*>
- unify_resolve_refine poly flags gl clenv)) in
+ unify_resolve_refine flags gl clenv)) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
let tac =
- with_prods nprods poly h (unify_e_resolve poly flags) in
+ with_prods nprods h (unify_e_resolve flags) in
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| Give_exact h ->
@@ -385,12 +384,12 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
let tac =
matches_pattern concl p <*>
Proofview.Goal.enter
- (fun gl -> unify_resolve_refine poly flags gl (h, None)) in
+ (fun gl -> unify_resolve_refine flags gl (h, None)) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
- e_give_exact flags poly h
+ e_give_exact flags h
| Res_pf_THEN_trivial_fail h ->
- let fst = with_prods nprods poly h (unify_e_resolve poly flags) in
+ let fst = with_prods nprods h (unify_e_resolve flags) in
let snd = if complete then Tacticals.New.tclIDTAC
else e_trivial_fail_db only_classes db_list local_db secvars in
Tacticals.New.tclTHEN fst snd
@@ -1251,8 +1250,8 @@ let autoapply c i =
(Hints.Hint_db.transparent_state hintdb) in
let cty = Tacmach.New.pf_get_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
- let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce } in
- unify_e_resolve false flags gl (h, 0) <*>
+ let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in
+ unify_e_resolve flags gl (h, 0) <*>
Proofview.tclEVARMAP >>= (fun sigma ->
let sigma = Typeclasses.make_unresolvables
(fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 4a6364795b..0ff90bc046 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -65,9 +65,9 @@ open Auto
(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
(***************************************************************************)
-let unify_e_resolve poly flags h =
+let unify_e_resolve flags h =
Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv ~poly h gl in
+ let clenv', c = connect_hint_clenv h gl in
let clenv' = clenv_unique_resolver ~flags clenv' gl in
Proofview.tclTHEN
(Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl =
else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
(* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
-let e_exact poly flags h =
+let e_exact flags h =
Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv ~poly h gl in
+ let clenv', c = connect_hint_clenv h gl in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
(e_give_exact c)
@@ -121,17 +121,16 @@ and e_my_find_search env sigma db_list local_db secvars concl =
in
let tac_of_hint =
fun (st, h) ->
- let poly = FullHint.is_polymorphic h in
let b = match FullHint.repr h with
| Unfold_nth _ -> 1
| _ -> FullHint.priority h
in
let tac = function
- | Res_pf h -> unify_resolve ~poly st h
- | ERes_pf h -> unify_e_resolve poly st h
- | Give_exact h -> e_exact poly st h
+ | Res_pf h -> unify_resolve st h
+ | ERes_pf h -> unify_e_resolve st h
+ | Give_exact h -> e_exact st h
| Res_pf_THEN_trivial_fail h ->
- Tacticals.New.tclTHEN (unify_e_resolve poly st h)
+ Tacticals.New.tclTHEN (unify_e_resolve st h)
(e_trivial_fail_db db_list local_db)
| Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
| Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0a213d5d0e..7a5615dd8e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -135,20 +135,20 @@ type 'a with_uid = {
uid : KerName.t;
}
-type raw_hint = constr * types * Univ.ContextSet.t
+type raw_hint = constr * types * Univ.ContextSet.t * bool (* poly *)
type hint = {
hint_term : constr;
hint_type : types;
hint_uctx : Univ.ContextSet.t;
hint_clnv : clausenv;
+ hint_poly : bool;
+ (** Is the hint polymorpic and hence should be refreshed at each application *)
}
type 'a with_metadata =
{ pri : int
(** A number lower is higher priority *)
- ; poly : bool
- (** Is the hint polymorpic and hence should be refreshed at each application *)
; pat : constr_pattern option
(** A pattern for the concl of the Goal *)
; name : hints_path_atom
@@ -305,14 +305,14 @@ let strip_params env sigma c =
| _ -> c
let instantiate_hint env sigma p =
- let mk_clenv (c, cty, ctx) =
+ let mk_clenv (c, cty, ctx, poly) =
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
let cl = mk_clenv_from_env env sigma None (c,cty) in
let cl = {cl with templval =
{ cl.templval with rebus = strip_params env sigma cl.templval.rebus };
env = empty_env}
in
- { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
+ { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; hint_poly = poly }
in
let code = match p.code.obj with
| Res_pf c -> Res_pf (mk_clenv c)
@@ -806,9 +806,9 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
| None -> pat
in
(Some hd,
- { pri; poly; pat = Some pat; name;
+ { pri; pat = Some pat; name;
db = None; secvars;
- code = with_uid (Give_exact (c, cty, ctx)); })
+ code = with_uid (Give_exact (c, cty, ctx, poly)); })
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
@@ -830,10 +830,10 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
in
if Int.equal nmiss 0 then
(Some hd,
- { pri; poly; pat = Some pat; name;
+ { pri; pat = Some pat; name;
db = None;
secvars;
- code = with_uid (Res_pf(c,cty,ctx)); })
+ code = with_uid (Res_pf(c,cty,ctx,poly)); })
else begin
if not eapply then failwith "make_apply_entry";
if verbose then begin
@@ -849,9 +849,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
)
end;
(Some hd,
- { pri; poly; pat = Some pat; name;
+ { pri; pat = Some pat; name;
db = None; secvars;
- code = with_uid (ERes_pf(c,cty,ctx)); })
+ code = with_uid (ERes_pf(c,cty,ctx,poly)); })
end
| _ -> failwith "make_apply_entry"
@@ -922,7 +922,6 @@ let make_unfold eref =
let g = global_of_evaluable_reference eref in
(Some g,
{ pri = 4;
- poly = false;
pat = None;
name = PathHints [g];
db = None;
@@ -933,7 +932,6 @@ let make_extern pri pat tacast =
let hdconstr = Option.map try_head_pattern pat in
(hdconstr,
{ pri = pri;
- poly = false;
pat = pat;
name = PathAny;
db = None;
@@ -960,12 +958,11 @@ let make_trivial env sigma poly ?(name=PathAny) r =
let ce = mk_clenv_from_env env sigma None (c,t) in
(Some hd,
{ pri=1;
- poly = poly;
pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
name = name;
db = None;
secvars = secvars_of_constr env sigma c;
- code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
+ code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx,poly)) })
@@ -1076,29 +1073,30 @@ let subst_autohint (subst, obj) =
(try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
with Bound -> gr')
in
+ let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
+ let subst_aux ((c, t, ctx, poly) as h) =
+ let c' = subst_mps subst c in
+ let t' = subst_mps subst t in
+ if c==c' && t'==t then h else (c', t', ctx, poly)
+ in
let subst_hint (k,data as hint) =
let k' = Option.Smart.map subst_key k in
let env = Global.env () in
let sigma = Evd.from_env env in
let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
- let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
let code' = match data.code.obj with
- | Res_pf (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx)
- | ERes_pf (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx)
- | Give_exact (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx)
- | Res_pf_THEN_trivial_fail (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx)
+ | Res_pf h ->
+ let h' = subst_aux h in
+ if h == h' then data.code.obj else Res_pf h'
+ | ERes_pf h ->
+ let h' = subst_aux h in
+ if h == h' then data.code.obj else ERes_pf h'
+ | Give_exact h ->
+ let h' = subst_aux h in
+ if h == h' then data.code.obj else Give_exact h'
+ | Res_pf_THEN_trivial_fail h ->
+ let h' = subst_aux h in
+ if h == h' then data.code.obj else Res_pf_THEN_trivial_fail h'
| Unfold_nth ref ->
let ref' = subst_evaluable_reference subst ref in
if ref==ref' then data.code.obj else Unfold_nth ref'
@@ -1587,7 +1585,6 @@ module FullHint =
struct
type t = full_hint
let priority (h : t) = h.pri
- let is_polymorphic (h : t) = h.poly
let pattern (h : t) = h.pat
let database (h : t) = h.db
let run (h : t) k = run_hint h.code k
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 29fd90d3ef..8243716624 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -44,6 +44,7 @@ type hint = {
hint_type : types;
hint_uctx : Univ.ContextSet.t;
hint_clnv : clausenv;
+ hint_poly : bool;
}
type 'a hints_path_atom_gen =
@@ -58,7 +59,6 @@ module FullHint :
sig
type t
val priority : t -> int
- val is_polymorphic : t -> bool
val pattern : t -> Pattern.constr_pattern option
val database : t -> string option
val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:20:55 +0000