aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/reductionops.ml55
-rw-r--r--pretyping/reductionops.mli6
-rw-r--r--pretyping/typing.ml2
-rw-r--r--proofs/clenv.ml54
-rw-r--r--proofs/clenv.mli8
-rw-r--r--tactics/equality.ml3
-rw-r--r--tactics/hints.ml23
-rw-r--r--tactics/tactics.ml10
8 files changed, 103 insertions, 58 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7a5d0897b5..9580825010 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1184,11 +1184,15 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
let default_plain_instance_ident = Id.of_string "H"
+type subst_fun = { sfun : metavariable -> EConstr.t }
+
(* Try to replace all metas. Does not replace metas in the metas' values
* Differs from (strong whd_meta). *)
-let plain_instance sigma s c =
+let plain_instance sigma s c = match s with
+| None -> c
+| Some s ->
let rec irec n u = match EConstr.kind sigma u with
- | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
+ | Meta p -> (try lift n (s.sfun p) with Not_found -> u)
| App (f,l) when isCast sigma f ->
let (f,_,t) = destCast sigma f in
let l' = Array.Fun1.Smart.map irec n l in
@@ -1197,7 +1201,7 @@ let plain_instance sigma s c =
(* Don't flatten application nodes: this is used to extract a
proof-term from a proof-tree and we want to keep the structure
of the proof-tree *)
- (try let g = Metamap.find p s in
+ (try let g = s.sfun p in
match EConstr.kind sigma g with
| App _ ->
let l' = Array.Fun1.Smart.map lift 1 l' in
@@ -1208,12 +1212,11 @@ let plain_instance sigma s c =
with Not_found -> mkApp (f,l'))
| _ -> mkApp (irec n f,l'))
| Cast (m,_,_) when isMeta sigma m ->
- (try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
+ (try lift n (s.sfun (destMeta sigma m)) with Not_found -> u)
| _ ->
map_with_binders sigma succ irec n u
in
- if Metamap.is_empty s then c
- else irec 0 c
+ irec 0 c
(* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
has (unfortunately) different subtle side effects:
@@ -1415,23 +1418,41 @@ let is_arity env sigma c =
(*************************************)
(* Metas *)
-let meta_value env evd mv =
- let rec valrec mv =
- match meta_opt_fvalue evd mv with
- | Some (b,_) ->
- let metas = Metamap.bind valrec b.freemetas in
- instance env evd metas b.rebus
- | None -> mkMeta mv
+type meta_instance_subst = {
+ sigma : Evd.evar_map;
+ mutable cache : EConstr.t Metamap.t;
+}
+
+let create_meta_instance_subst sigma = {
+ sigma;
+ cache = Metamap.empty;
+}
+
+let eval_subst env subst =
+ let rec ans mv =
+ try Metamap.find mv subst.cache
+ with Not_found ->
+ match meta_opt_fvalue subst.sigma mv with
+ | None -> mkMeta mv
+ | Some (b, _) ->
+ let metas =
+ if Metaset.is_empty b.freemetas then None
+ else Some { sfun = ans }
+ in
+ let res = instance env subst.sigma metas b.rebus in
+ let () = subst.cache <- Metamap.add mv res subst.cache in
+ res
in
- valrec mv
+ { sfun = ans }
-let meta_instance env sigma b =
+let meta_instance env subst b =
let fm = b.freemetas in
if Metaset.is_empty fm then b.rebus
else
- let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in
- instance env sigma c_sigma b.rebus
+ let sfun = eval_subst env subst in
+ instance env subst.sigma (Some sfun) b.rebus
let nf_meta env sigma c =
+ let sigma = create_meta_instance_subst sigma in
let cl = mk_freelisted c in
meta_instance env sigma { cl with rebus = cl.rebus }
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 04dfc5ffe6..0b7f43f469 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -258,7 +258,11 @@ val whd_betaiota_deltazeta_for_iota_state :
TransparentState.t -> state_reduction_function
(** {6 Meta-related reduction functions } *)
-val meta_instance : env -> evar_map -> constr freelisted -> constr
+type meta_instance_subst
+
+val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst
+
+val meta_instance : env -> meta_instance_subst -> constr freelisted -> constr
val nf_meta : env -> evar_map -> constr -> constr
exception AnomalyInConversion of exn
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index aeb3873de7..e3e5244a8c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -33,7 +33,7 @@ let meta_type env evd mv =
let ty =
try Evd.meta_ftype evd mv
with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
- meta_instance env evd ty
+ meta_instance env (create_meta_instance_subst evd) ty
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 387f0f6f5f..00ac5a0624 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -37,15 +37,28 @@ type clausenv = {
env : env;
evd : evar_map;
templval : constr freelisted;
- templtyp : constr freelisted }
+ templtyp : constr freelisted;
+ cache : Reductionops.meta_instance_subst;
+}
+
+let mk_clausenv env evd templval templtyp = {
+ env; evd; templval; templtyp; cache = create_meta_instance_subst evd;
+}
+
+let update_clenv_evd clenv evd =
+ mk_clausenv clenv.env evd clenv.templval clenv.templtyp
let cl_env ce = ce.env
let cl_sigma ce = ce.evd
-let clenv_term clenv c = meta_instance clenv.env clenv.evd c
-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 clenv_term clenv c = meta_instance clenv.env clenv.cache c
+let clenv_meta_type clenv mv =
+ let ty =
+ try Evd.meta_ftype clenv.evd mv
+ with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
+ meta_instance clenv.env clenv.cache ty
+let clenv_value clenv = meta_instance clenv.env clenv.cache clenv.templval
+let clenv_type clenv = meta_instance clenv.env clenv.cache clenv.templtyp
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
@@ -67,7 +80,8 @@ let clenv_push_prod cl =
{ templval = mk_freelisted def;
templtyp = mk_freelisted concl;
evd = e';
- env = cl.env }
+ env = cl.env;
+ cache = create_meta_instance_subst e' }
| _ -> raise NotExtensibleClause
in clrec typ
@@ -109,7 +123,8 @@ let mk_clenv_from_env env sigma n (c,cty) =
{ templval = mk_freelisted (applist (c,args));
templtyp = mk_freelisted concl;
evd = evd;
- env = env }
+ env = env;
+ cache = create_meta_instance_subst evd }
let mk_clenv_from_n gls n (c,cty) =
let env = Proofview.Goal.env gls in
@@ -158,7 +173,7 @@ let clenv_assign mv rhs clenv =
clenv
else
let st = (Conv,TypeNotProcessed) in
- {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
+ update_clenv_evd clenv (meta_assign mv (rhs_fls.rebus,st) clenv.evd)
with Not_found ->
user_err Pp.(str "clenv_assign: undefined meta")
@@ -202,19 +217,19 @@ let clenv_assign mv rhs clenv =
In any case, we respect the order given in A.
*)
-let clenv_metas_in_type_of_meta env evd mv =
- (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas
+let clenv_metas_in_type_of_meta clenv mv =
+ (mk_freelisted (meta_instance clenv.env clenv.cache (meta_ftype clenv.evd mv))).freemetas
let dependent_in_type_of_metas clenv mvs =
List.fold_right
- (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.env clenv.evd mv))
+ (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv mv))
mvs Metaset.empty
let dependent_closure clenv mvs =
let rec aux mvs acc =
Metaset.fold
(fun mv deps ->
- let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.env clenv.evd mv in
+ let metas_of_meta_type = clenv_metas_in_type_of_meta clenv mv in
aux metas_of_meta_type (Metaset.union deps metas_of_meta_type))
mvs acc in
aux mvs mvs
@@ -297,11 +312,10 @@ let meta_reducible_instance env evd b =
else irec b.rebus
let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
- { clenv with
- evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
+ update_clenv_evd clenv (w_unify ~flags clenv.env clenv.evd cv_pb t1 t2)
let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
- { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
+ update_clenv_evd clenv (w_unify_meta_types ~flags:flags clenv.env clenv.evd)
let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then
@@ -414,11 +428,13 @@ let fchain_flags () =
let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv =
(* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
+ let evd = meta_merge ?with_univs nextclenv.evd clenv.evd in
let clenv' =
{ templval = clenv.templval;
templtyp = clenv.templtyp;
- evd = meta_merge ?with_univs nextclenv.evd clenv.evd;
- env = nextclenv.env } in
+ evd;
+ env = nextclenv.env;
+ cache = create_meta_instance_subst evd } in
(* unify the type of the template of [nextclenv] with the type of [mv] *)
let clenv'' =
clenv_unify ~flags CUMUL
@@ -538,7 +554,7 @@ let clenv_assign_binding clenv k c =
let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in
let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
- { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
+ update_clenv_evd clenv' (meta_assign k (c,(Conv,status)) clenv'.evd)
let clenv_match_args bl clenv =
if List.is_empty bl then
@@ -640,7 +656,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
Typeclasses.make_unresolvables (fun x -> true) evd'
else clenv.evd
in
- let clenv = { clenv with evd = evd' } in
+ let clenv = update_clenv_evd clenv evd' in
Proofview.tclTHEN
(Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
(refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index a72c8c5e1f..6e472da452 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -22,14 +22,18 @@ open Tactypes
(** {6 The Type of Constructions clausale environments.} *)
-type clausenv = {
+type clausenv = private {
env : env; (** the typing context *)
evd : evar_map; (** the mapping from metavar and evar numbers to their
types and values *)
templval : constr freelisted; (** the template which we are trying to fill
out *)
- templtyp : constr freelisted (** its type *)}
+ templtyp : constr freelisted; (** its type *)
+ cache : Reductionops.meta_instance_subst; (* Reductionops.create_meta_instance_subst evd) *)
+}
+val mk_clausenv : env -> evar_map -> constr freelisted -> types freelisted -> clausenv
+val update_clenv_evd : clausenv -> evar_map -> clausenv
(** subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fcdd23a9c1..633b9da053 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -154,7 +154,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let c1 = args.(arglen - 2) in
let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
- Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
+ let clenv = Clenv.update_clenv_evd eqclause evd' in
+ Clenv.clenv_pose_dependent_evars ~with_evars:true clenv
in
let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
let occs =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6fab111e6f..ace51c40d4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -340,10 +340,8 @@ let instantiate_hint env sigma p =
let mk_clenv (c, cty, ctx) =
let sigma = merge_context_set_opt 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
+ let templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus } in
+ let cl = mk_clausenv empty_env cl.evd templval cl.templtyp in
{ hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
in
let code = match p.code.obj with
@@ -1649,14 +1647,17 @@ let connect_hint_clenv h gl =
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;
- }
+ Clenv.mk_clausenv
+ (Proofview.Goal.env gl)
+ (Evd.map_metas emap evd)
+ (Evd.map_fl emap clenv.templval)
+ (Evd.map_fl emap clenv.templtyp)
| None ->
- { clenv with evd = evd ; env = Proofview.Goal.env gl }
+ Clenv.mk_clausenv
+ (Proofview.Goal.env gl)
+ evd
+ clenv.templval
+ clenv.templtyp
let fresh_hint env sigma h =
let { hint_term = c; hint_uctx = ctx } = h in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 130e0e97c2..39c5c9562f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1301,20 +1301,18 @@ let do_replace id = function
let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
- let clenv =
- { clenv with evd = Typeclasses.resolve_typeclasses
- ~fail:(not with_evars) clenv.env clenv.evd }
- in
+ let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in
+ let clenv = Clenv.update_clenv_evd clenv evd in
let new_hyp_typ = clenv_type clenv in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
- if not with_evars && occur_meta clenv.evd new_hyp_typ then
+ if not with_evars && occur_meta evd new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
let naming = NamingMustBe (CAst.make targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
+ (Proofview.Unsafe.tclEVARS (clear_metas evd))
(Tacticals.New.tclTHENLAST
(assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:54:46 +0000