aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh6
-rw-r--r--engine/evd.ml5
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/uState.ml29
-rw-r--r--engine/uState.mli2
-rw-r--r--proofs/clenv.ml10
-rw-r--r--proofs/clenv.mli3
-rw-r--r--tactics/auto.ml43
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/class_tactics.ml120
-rw-r--r--tactics/eauto.ml14
-rw-r--r--tactics/hints.ml42
-rw-r--r--tactics/hints.mli7
13 files changed, 111 insertions, 176 deletions
diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh
new file mode 100644
index 0000000000..e57f95ef19
--- /dev/null
+++ b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then
+
+ coqhammer_CI_REF=factor-class-hint-clenv
+ coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+fi
diff --git a/engine/evd.ml b/engine/evd.ml
index c570f75c6b..e85cbc96b2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -987,11 +987,6 @@ let check_constraints evd csts =
let fix_undefined_variables evd =
{ evd with universes = UState.fix_undefined_variables evd.universes }
-let refresh_undefined_universes evd =
- let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
- let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
- evd', subst
-
let nf_univ_variables evd =
let subst, uctx' = UState.normalize_variables evd.universes in
let evd' = {evd with universes = uctx'} in
diff --git a/engine/evd.mli b/engine/evd.mli
index 679173ca72..3f17e63034 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -643,8 +643,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
val fix_undefined_variables : evar_map -> evar_map
-val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
-
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index d4cb59da26..ca0a21acf7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -718,35 +718,6 @@ let fix_undefined_variables uctx =
{ uctx with univ_variables = vars';
univ_algebraic = algs' }
-let refresh_undefined_univ_variables uctx =
- let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in
- let subst_fn u = subst_univs_level_level subst u in
- let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc)
- uctx.univ_algebraic LSet.empty
- in
- let vars =
- LMap.fold
- (fun u v acc ->
- LMap.add (subst_fn u)
- (Option.map (subst_univs_level_universe subst) v) acc)
- uctx.univ_variables LMap.empty
- in
- let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in
- let lbound = uctx.universes_lbound in
- let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g)
- (ContextSet.levels ctx') g in
- let initial = declare uctx.initial_universes in
- let univs = declare UGraph.initial_universes in
- let uctx' = {names = uctx.names;
- local = ctx';
- seff_univs = uctx.seff_univs;
- univ_variables = vars; univ_algebraic = alg;
- universes = univs;
- universes_lbound = lbound;
- initial_universes = initial;
- weak_constraints = weak; } in
- uctx', subst
-
let minimize uctx =
let open UnivMinim in
let lbound = uctx.universes_lbound in
diff --git a/engine/uState.mli b/engine/uState.mli
index 45a0f9964e..607c6c9452 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -154,8 +154,6 @@ val abstract_undefined_variables : t -> t
val fix_undefined_variables : t -> t
-val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
-
(** Universe minimization *)
val minimize : t -> t
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 9bd7ccda5d..db76d08736 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -47,16 +47,6 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv
let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval
let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp
-let refresh_undefined_univs clenv =
- match EConstr.kind clenv.evd clenv.templval.rebus with
- | Var _ -> clenv, Univ.empty_level_subst
- | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
- | _ ->
- let evd', subst = Evd.refresh_undefined_universes clenv.evd in
- let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
- { clenv with evd = evd'; templval = map_freelisted clenv.templval;
- templtyp = map_freelisted clenv.templtyp }, subst
-
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index fd1e2fe593..43e808dac7 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -45,9 +45,6 @@ val mk_clenv_from_n :
Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
-(** Refresh the universes in a clenv *)
-val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
-
(** {6 linking of clenvs } *)
val clenv_fchain :
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3287c1c354..0931c3e61e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,11 +12,9 @@ open Pp
open Util
open Names
open Termops
-open EConstr
open Environ
open Genredexpr
open Tactics
-open Clenv
open Locus
open Proofview.Notations
open Hints
@@ -69,38 +67,7 @@ let auto_unif_flags =
(* Try unification with the precompiled clause, then use registered Apply *)
-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
- below just replaces the metas of sigma by those coming from the clenv. *)
- let sigma = Tacmach.New.project gl in
- 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 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
- let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
- (* Only metas are mentioning the old universes. *)
- let clenv = {
- templval = Evd.map_fl emap clenv.templval;
- templtyp = Evd.map_fl emap clenv.templtyp;
- evd = Evd.map_metas emap evd;
- env = Proofview.Goal.env gl;
- } in
- clenv, emap c
- else
- let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
- { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
- in clenv, c
-
-let unify_resolve flags (h : hint) =
- Proofview.Goal.enter begin fun gl ->
- let clenv, c = connect_hint_clenv h gl in
- Clenv.res_pf ~flags clenv
- end
+let unify_resolve flags h = Hints.hint_res_pf ~flags h
let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
@@ -110,10 +77,10 @@ let unify_resolve_gen = function
let exact h =
Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv h gl in
- Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
- (exact_check c)
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, c = Hints.fresh_hint env sigma h in
+ Proofview.Unsafe.tclEVARS sigma <*> exact_check c
end
(* Util *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 903da143d2..bc2eee0e4c 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -12,7 +12,6 @@
open Names
open EConstr
-open Clenv
open Pattern
open Hints
open Tactypes
@@ -23,9 +22,6 @@ val default_search_depth : int ref
val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
-val connect_hint_clenv
- : hint -> Proofview.Goal.t -> clausenv * constr
-
(** Try unification with the precompiled clause, then use registered Apply *)
val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 63cafbf76d..36544883aa 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,61 +144,50 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
}
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 env = Proofview.Goal.env gl in
let sigma = project gl in
- let c, sigma =
- 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
- c, evd
- else c, sigma
- in
+ let sigma, c = Hints.fresh_hint env sigma h in
let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
Proofview.Unsafe.tclEVARS sigma <*>
Clenv.unify ~flags t1 <*> exact_no_check c
end
-let unify_e_resolve flags = begin fun gls (h, _) ->
- let clenv', c = connect_hint_clenv h gls in
- Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
- end
-
-let unify_resolve flags = begin fun gls (h, _) ->
- let clenv', _ = connect_hint_clenv h gls in
- Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
+let unify_resolve ~with_evars flags h diff = match diff with
+| None ->
+ Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h
+| Some (diff, ty) ->
+ let () = assert (not h.hint_poly) in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let sigma, c = Hints.fresh_hint env sigma h in
+ let clenv = mk_clenv_from_env env sigma (Some diff) (c, ty) in
+ Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv
end
(** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine flags gls (h, n) =
- let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in
+let unify_resolve_refine flags h diff =
+ let len = match diff with None -> None | Some (diff, _) -> Some diff in
+ Proofview.Goal.enter begin fun gls ->
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 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
- sigma, map c, map t
- else
- let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- sigma, c, t
- in
- let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
- let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
- let sigma' =
- Evarconv.(unify_leq_delay
- ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
- env sigma' cl.cl_concl concl)
- in (sigma', term) end
-
-let unify_resolve_refine flags gl clenv =
+ let sigma, term = Hints.fresh_hint env sigma h in
+ let ty = Retyping.get_type_of env sigma term in
+ let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in
+ let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
+ let flags = Evarconv.default_flags_of flags.core_unify_flags.modulo_delta in
+ let sigma = Evarconv.unify_leq_delay ~flags env sigma cl.cl_concl concl in
+ (sigma, term)
+ end
+ end
+
+let unify_resolve_refine flags h diff =
Proofview.tclORELSE
- (unify_resolve_refine flags gl clenv)
+ (unify_resolve_refine flags h diff)
(fun (exn,info) ->
match exn with
| Evarconv.UnableToUnify _ ->
@@ -211,35 +200,21 @@ let unify_resolve_refine flags gl clenv =
(** Dealing with goals of the form A -> B and hints of the form
C -> A -> B.
*)
-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
- let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
- let diff = nb_prod sigma ty - nprods in
- if (>=) diff 0 then
- (* Was Some clenv... *)
- Some (Some diff,
- mk_clenv_from_n gl (Some diff) (c,ty))
- else None
-
let with_prods nprods h f =
if get_typeclasses_limit_intros () then
Proofview.Goal.enter begin fun gl ->
- try match clenv_of_prods nprods h gl with
- | None ->
- let info = Exninfo.reify () in
- Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
- | Some (diff, clenv') ->
- let h = { h with hint_clnv = clenv' } in
- f gl (h, diff)
- with e when CErrors.noncritical e ->
- let e, info = Exninfo.capture e in
- Proofview.tclZERO ~info e end
+ let { hint_term = c; hint_poly = poly } = h in
+ if poly || Int.equal nprods 0 then f None
+ else
+ let sigma = Tacmach.New.project gl in
+ let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+ let diff = nb_prod sigma ty - nprods in
+ if (>=) diff 0 then f (Some (diff, ty))
+ else Tacticals.New.tclZEROMSG (str"Not enough premisses")
+ end
else Proofview.Goal.enter
begin fun gl ->
- if Int.equal nprods 0 then f gl (h, None)
+ if Int.equal nprods 0 then f None
else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
let matches_pattern concl pat =
@@ -347,25 +322,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
if get_typeclasses_filtered_unification () then
let tac =
with_prods nprods h
- (fun gl clenv ->
+ (fun diff ->
matches_pattern concl p <*>
- unify_resolve_refine flags gl clenv)
+ unify_resolve_refine flags h diff)
in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
let tac =
- with_prods nprods h (unify_resolve flags) in
+ with_prods nprods h (unify_resolve ~with_evars:false flags h) 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 h
- (fun gl clenv ->
+ (fun diff ->
matches_pattern concl p <*>
- unify_resolve_refine flags gl clenv)) in
+ unify_resolve_refine flags h diff)) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
let tac =
- with_prods nprods h (unify_e_resolve flags) in
+ with_prods nprods h (unify_resolve ~with_evars:true flags h) in
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| Give_exact h ->
@@ -373,12 +348,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 flags gl (h, None)) in
+ (fun gl -> unify_resolve_refine flags h None) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
e_give_exact flags h
| Res_pf_THEN_trivial_fail h ->
- let fst = with_prods nprods h (unify_e_resolve flags) in
+ let fst = with_prods nprods h (unify_resolve ~with_evars:true flags h) 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
@@ -1235,8 +1210,7 @@ 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; hint_poly = false } in
- unify_e_resolve flags gl (h, 0) <*>
+ Clenv.res_pf ~with_evars:true ~with_classes:false ~flags ce <*>
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 686303a2ab..9a554b117e 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -19,7 +19,6 @@ open Tacticals
open Tacmach
open Evd
open Tactics
-open Clenv
open Auto
open Genredexpr
open Tactypes
@@ -66,10 +65,7 @@ open Auto
(***************************************************************************)
let unify_e_resolve flags h =
- Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv h gl in
- Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv'
- end
+ Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h
let hintmap_of sigma secvars concl =
(* Warning: for computation sharing, we need to return a closure *)
@@ -87,10 +83,10 @@ let hintmap_of sigma secvars concl =
let e_exact flags h =
Proofview.Goal.enter begin fun gl ->
- 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)
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, c = Hints.fresh_hint env sigma h in
+ Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c
end
let rec e_trivial_fail_db db_list local_db =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 58bebe319b..41b200bb83 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1599,3 +1599,45 @@ struct
let repr (h : t) = h.code.obj
end
+
+let connect_hint_clenv h gl =
+ let { 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
+ below just replaces the metas of sigma by those coming from the clenv. *)
+ let sigma = Tacmach.New.project gl in
+ let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
+ (* Still, we need to update the universes *)
+ 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
+ let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+ (* Only metas are mentioning the old universes. *)
+ {
+ templval = Evd.map_fl emap clenv.templval;
+ templtyp = Evd.map_fl emap clenv.templtyp;
+ evd = Evd.map_metas emap evd;
+ env = Proofview.Goal.env gl;
+ }
+ else
+ let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+ { clenv with evd = evd ; env = Proofview.Goal.env gl }
+
+let fresh_hint env sigma h =
+ let { hint_term = c; hint_uctx = ctx } = h in
+ if h.hint_poly then
+ (* Refresh the instance of the hint *)
+ let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
+ let c = Vars.subst_univs_level_constr subst c in
+ let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+ sigma, c
+ else
+ let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+ sigma, c
+
+let hint_res_pf ?with_evars ?with_classes ?flags h =
+ Proofview.Goal.enter begin fun gl ->
+ let clenv = connect_hint_clenv h gl in
+ Clenv.res_pf ?with_evars ?with_classes ?flags clenv
+ end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 8243716624..f0fed75828 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -39,7 +39,7 @@ type 'a hint_ast =
| Unfold_nth of evaluable_global_reference (* Hint Unfold *)
| Extern of Genarg.glob_generic_argument (* Hint Extern *)
-type hint = {
+type hint = private {
hint_term : constr;
hint_type : types;
hint_uctx : Univ.ContextSet.t;
@@ -239,6 +239,11 @@ val wrap_hint_warning_fun : env -> evar_map ->
(evar_map -> 'a * evar_map) -> 'a * evar_map
(** Variant of the above for non-tactics *)
+val fresh_hint : env -> evar_map -> hint -> evar_map * constr
+
+val hint_res_pf : ?with_evars:bool -> ?with_classes:bool ->
+ ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic
+
(** Printing hints *)
val pr_searchtable : env -> evar_map -> Pp.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:37:56 +0000