From 981146bbc716494ba9ced0d6b403923b293cdec1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 4 Apr 2020 17:04:30 +0200 Subject: Cache meta access in meta_instance. --- proofs/clenv.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 387f0f6f5f..f47ed0fc4b 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -42,10 +42,10 @@ type clausenv = { 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_term clenv c = meta_instance clenv.env (create_meta_instance_subst 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_value clenv = meta_instance clenv.env (create_meta_instance_subst clenv.evd) clenv.templval +let clenv_type clenv = meta_instance clenv.env (create_meta_instance_subst clenv.evd) clenv.templtyp let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t @@ -203,7 +203,7 @@ let clenv_assign mv rhs clenv = *) let clenv_metas_in_type_of_meta env evd mv = - (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas + (mk_freelisted (meta_instance env (create_meta_instance_subst evd) (meta_ftype evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right -- cgit v1.2.3 From 161b7b47f7f87c33f1fa6269248d5f8b6b4926d9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Dec 2020 21:09:11 +0100 Subject: Make the clenv type private and provide a creation function. --- proofs/clenv.ml | 7 +++++++ proofs/clenv.mli | 4 +++- 2 files changed, 10 insertions(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f47ed0fc4b..23ae9d04c4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -39,6 +39,13 @@ type clausenv = { templval : constr freelisted; templtyp : constr freelisted } +let mk_clausenv env evd templval templtyp = { + env; evd; templval; templtyp; +} + +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 diff --git a/proofs/clenv.mli b/proofs/clenv.mli index a72c8c5e1f..bfdc5cdd8c 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -22,7 +22,7 @@ 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 *) @@ -30,6 +30,8 @@ type clausenv = { out *) templtyp : constr freelisted (** its type *)} +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 -- cgit v1.2.3 From bc9a22fff77c192dce477ab4d668713c6792b6c4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Dec 2020 21:19:17 +0100 Subject: Store the metasubst cache in clenvs. --- proofs/clenv.ml | 29 +++++++++++++++++------------ proofs/clenv.mli | 4 +++- 2 files changed, 20 insertions(+), 13 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 23ae9d04c4..48755ab2db 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -37,10 +37,12 @@ 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; + env; evd; templval; templtyp; cache = create_meta_instance_subst evd; } let update_clenv_evd clenv evd = @@ -74,7 +76,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 @@ -116,7 +119,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 @@ -165,7 +169,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") @@ -304,11 +308,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 @@ -421,11 +424,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 @@ -545,7 +550,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 @@ -647,7 +652,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 bfdc5cdd8c..6e472da452 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -28,7 +28,9 @@ type clausenv = private { 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 -- cgit v1.2.3 From 7a8761b0ca9c503592c14ee98402e530cde28846 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Dec 2020 21:33:42 +0100 Subject: Reuse the cache everywhere possible in Clenv. --- proofs/clenv.ml | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 48755ab2db..00ac5a0624 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -51,10 +51,14 @@ let update_clenv_evd clenv evd = let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_term clenv c = meta_instance clenv.env (create_meta_instance_subst 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 (create_meta_instance_subst clenv.evd) clenv.templval -let clenv_type clenv = meta_instance clenv.env (create_meta_instance_subst 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 @@ -213,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 (create_meta_instance_subst 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 -- cgit v1.2.3