aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/cClosure.ml103
-rw-r--r--kernel/cClosure.mli20
-rw-r--r--kernel/reduction.ml87
-rw-r--r--plugins/setoid_ring/newring.ml2
-rw-r--r--pretyping/cbv.ml8
-rw-r--r--pretyping/inferCumulativity.ml10
-rw-r--r--pretyping/reductionops.ml2
7 files changed, 128 insertions, 104 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 219ea5b24..5e1b81adc 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -257,12 +257,14 @@ module KeyTable = Hashtbl.Make(IdKeyHash)
let eq_table_key = IdKeyHash.equal
+type 'a infos_tab = 'a KeyTable.t
+
type 'a infos_cache = {
- i_repr : 'a infos -> constr -> 'a;
+ i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
i_env : env;
i_sigma : existential -> constr option;
i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t;
- i_tab : 'a KeyTable.t }
+}
and 'a infos = {
i_flags : reds;
@@ -277,9 +279,9 @@ let assoc_defined id env = match Environ.lookup_named id env with
| LocalDef (_, c, _) -> c
| _ -> raise Not_found
-let ref_value_cache ({i_cache = cache} as infos) ref =
+let ref_value_cache ({i_cache = cache} as infos) tab ref =
try
- Some (KeyTable.find cache.i_tab ref)
+ Some (KeyTable.find tab ref)
with Not_found ->
try
let body =
@@ -298,8 +300,8 @@ let ref_value_cache ({i_cache = cache} as infos) ref =
| VarKey id -> assoc_defined id cache.i_env
| ConstKey cst -> constant_value_in cache.i_env cst
in
- let v = cache.i_repr infos body in
- KeyTable.add cache.i_tab ref v;
+ let v = cache.i_repr infos tab body in
+ KeyTable.add tab ref v;
Some v
with
| Not_found (* List.assoc *)
@@ -316,7 +318,7 @@ let create mk_cl flgs env evars =
i_env = env;
i_sigma = evars;
i_rels = (Environ.pre_env env).env_rel_context.env_rel_map;
- i_tab = KeyTable.create 17 }
+ }
in { i_flags = flgs; i_cache = cache }
@@ -904,23 +906,23 @@ and knht info e t stk =
(************************************************************************)
(* Computes a weak head normal form from the result of knh. *)
-let rec knr info m stk =
+let rec knr info tab m stk =
match m.term with
| FLambda(n,tys,f,e) when red_set info.i_flags fBETA ->
(match get_args n tys f e stk with
- Inl e', s -> knit info e' f s
+ Inl e', s -> knit info tab e' f s
| Inr lam, s -> (lam,s))
| FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) ->
- (match ref_value_cache info (ConstKey c) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (ConstKey c) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
- (match ref_value_cache info (VarKey id) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (VarKey id) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FFlex(RelKey k) when red_set info.i_flags fDELTA ->
- (match ref_value_cache info (RelKey k) with
- Some v -> kni info v stk
+ (match ref_value_cache info tab (RelKey k) with
+ Some v -> kni info tab v stk
| None -> (set_norm m; (m,stk)))
| FConstruct((ind,c),u) ->
let use_match = red_set info.i_flags fMATCH in
@@ -930,29 +932,29 @@ let rec knr info m stk =
| (depth, args, ZcaseT(ci,_,br,e)::s) when use_match ->
assert (ci.ci_npar>=0);
let rargs = drop_parameters depth ci.ci_npar args in
- knit info e br.(c-1) (rargs@s)
+ knit info tab e br.(c-1) (rargs@s)
| (_, cargs, Zfix(fx,par)::s) when use_fix ->
let rarg = fapp_stack(m,cargs) in
let stk' = par @ append_stack [|rarg|] s in
let (fxe,fxbd) = contract_fix_vect fx.term in
- knit info fxe fxbd stk'
+ knit info tab fxe fxbd stk'
| (depth, args, Zproj (n, m, cst)::s) when use_match ->
let rargs = drop_parameters depth n args in
let rarg = project_nth_arg m rargs in
- kni info rarg s
+ kni info tab rarg s
| (_,args,s) -> (m,args@s))
else (m,stk)
| FCoFix _ when red_set info.i_flags fCOFIX ->
(match strip_update_shift_app m stk with
(_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
let (fxe,fxbd) = contract_fix_vect m.term in
- knit info fxe fxbd (args@stk')
+ knit info tab fxe fxbd (args@stk')
| (_,args,s) -> (m,args@s))
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
- knit info (subs_cons([|v|],e)) bd stk
+ knit info tab (subs_cons([|v|],e)) bd stk
| FEvar(ev,env) ->
(match evar_value info.i_cache ev with
- Some c -> knit info env c stk
+ Some c -> knit info tab env c stk
| None -> (m,stk))
| FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
| FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
@@ -960,14 +962,14 @@ let rec knr info m stk =
(* Computes the weak head normal form of a term *)
-and kni info m stk =
+and kni info tab m stk =
let (hm,s) = knh info m stk in
- knr info hm s
-and knit info e t stk =
+ knr info tab hm s
+and knit info tab e t stk =
let (ht,s) = knht info e t stk in
- knr info ht s
+ knr info tab ht s
-let kh info v stk = fapp_stack(kni info v stk)
+let kh info tab v stk = fapp_stack(kni info tab v stk)
(************************************************************************)
@@ -995,61 +997,61 @@ let rec zip_term zfun m stk =
1- Calls kni
2- tries to rebuild the term. If a closure still has to be computed,
calls itself recursively. *)
-let rec kl info m =
+let rec kl info tab m =
if is_val m then (incr prune; term_of_fconstr m)
else
- let (nm,s) = kni info m [] in
+ let (nm,s) = kni info tab m [] in
let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
- zip_term (kl info) (norm_head info nm) s
+ zip_term (kl info tab) (norm_head info tab nm) s
(* no redex: go up for atoms and already normalized terms, go down
otherwise. *)
-and norm_head info m =
+and norm_head info tab m =
if is_val m then (incr prune; term_of_fconstr m) else
match m.term with
| FLambda(n,tys,f,e) ->
let (e',rvtys) =
List.fold_left (fun (e,ctxt) (na,ty) ->
- (subs_lift e, (na,kl info (mk_clos e ty))::ctxt))
+ (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt))
(e,[]) tys in
- let bd = kl info (mk_clos e' f) in
+ let bd = kl info tab (mk_clos e' f) in
List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys
| FLetIn(na,a,b,f,e) ->
let c = mk_clos (subs_lift e) f in
- mkLetIn(na, kl info a, kl info b, kl info c)
+ mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
| FProd(na,dom,rng) ->
- mkProd(na, kl info dom, kl info rng)
+ mkProd(na, kl info tab dom, kl info tab rng)
| FCoFix((n,(na,tys,bds)),e) ->
let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
- mkCoFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+ mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FFix((n,(na,tys,bds)),e) ->
let ftys = CArray.Fun1.map mk_clos e tys in
let fbds =
CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
- mkFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+ mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FEvar((i,args),env) ->
- mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
+ mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
| FProj (p,c) ->
- mkProj (p, kl info c)
+ mkProj (p, kl info tab c)
| FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
| FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
(* Initialization and then normalization *)
(* weak reduction *)
-let whd_val info v =
- with_stats (lazy (term_of_fconstr (kh info v [])))
+let whd_val info tab v =
+ with_stats (lazy (term_of_fconstr (kh info tab v [])))
(* strong reduction *)
-let norm_val info v =
- with_stats (lazy (kl info v))
+let norm_val info tab v =
+ with_stats (lazy (kl info tab v))
let inject c = mk_clos (subs_id 0) c
-let whd_stack infos m stk =
- let k = kni infos m stk in
+let whd_stack infos tab m stk =
+ let k = kni infos tab m stk in
let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
k
@@ -1057,7 +1059,10 @@ let whd_stack infos m stk =
type clos_infos = fconstr infos
let create_clos_infos ?(evars=fun _ -> None) flgs env =
- create (fun _ -> inject) flgs env evars
+ create (fun _ _ c -> inject c) flgs env evars
+
+let create_tab () = KeyTable.create 17
+
let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
let env_of_infos infos = infos.i_cache.i_env
@@ -1065,14 +1070,14 @@ let env_of_infos infos = infos.i_cache.i_env
let infos_with_reds infos reds =
{ infos with i_flags = reds }
-let unfold_reference info key =
+let unfold_reference info tab key =
match key with
| ConstKey (kn,_) ->
if red_set info.i_flags (fCONST kn) then
- ref_value_cache info key
+ ref_value_cache info tab key
else None
| VarKey i ->
if red_set info.i_flags (fVAR i) then
- ref_value_cache info key
+ ref_value_cache info tab key
else None
- | _ -> ref_value_cache info key
+ | _ -> ref_value_cache info tab key
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index c43fc4623..da14ff165 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -98,13 +98,15 @@ val unfold_red : evaluable_global_reference -> reds
type table_key = Constant.t Univ.puniverses tableKey
type 'a infos_cache
+type 'a infos_tab
type 'a infos = {
i_flags : reds;
i_cache : 'a infos_cache }
-val ref_value_cache: 'a infos -> table_key -> 'a option
-val create: ('a infos -> constr -> 'a) -> reds -> env ->
+val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
+val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env ->
(existential -> constr option) -> 'a infos
+val create_tab : unit -> 'a infos_tab
val evar_value : 'a infos_cache -> existential -> constr option
val info_env : 'a infos -> env
@@ -198,15 +200,15 @@ val infos_with_reds : clos_infos -> reds -> clos_infos
(** Reduction function *)
(** [norm_val] is for strong normalization *)
-val norm_val : clos_infos -> fconstr -> constr
+val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
(** [whd_val] is for weak head normalization *)
-val whd_val : clos_infos -> fconstr -> constr
+val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
(** [whd_stack] performs weak head normalization in a given stack. It
stops whenever a reduction is blocked. *)
val whd_stack :
- clos_infos -> fconstr -> stack -> fconstr * stack
+ clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
to the conversion of the eta expansion of t, considered as an inhabitant
@@ -223,7 +225,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
(** Conversion auxiliary functions to do step by step normalisation *)
(** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> table_key -> fconstr option
+val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option
val eq_table_key : table_key -> table_key -> bool
@@ -239,9 +241,9 @@ val mk_clos_deep :
(fconstr subs -> constr -> fconstr) ->
fconstr subs -> constr -> fconstr
-val kni: clos_infos -> fconstr -> stack -> fconstr * stack
-val knr: clos_infos -> fconstr -> stack -> fconstr * stack
-val kl : clos_infos -> fconstr -> constr
+val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 68f53c355..ea17b2559 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -115,12 +115,12 @@ let whd_betaiota env t =
| App (c, _) ->
begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t
- | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+ | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
end
- | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+ | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
let nf_betaiota env t =
- norm_val (create_clos_infos betaiota env) (inject t)
+ norm_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
let whd_betaiotazeta env x =
match kind x with
@@ -131,10 +131,10 @@ let whd_betaiotazeta env x =
| Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
| Case _ | Fix _ | CoFix _ | Proj _ ->
- whd_val (create_clos_infos betaiotazeta env) (inject x)
+ whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
end
| Rel _ | Cast _ | LetIn _ | Case _ | Proj _ ->
- whd_val (create_clos_infos betaiotazeta env) (inject x)
+ whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
let whd_all env t =
match kind t with
@@ -145,10 +145,10 @@ let whd_all env t =
| Ind _ | Construct _ | Evar _ | Meta _ -> t
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
| Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
- whd_val (create_clos_infos all env) (inject t)
+ whd_val (create_clos_infos all env) (create_tab ()) (inject t)
end
| Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ ->
- whd_val (create_clos_infos all env) (inject t)
+ whd_val (create_clos_infos all env) (create_tab ()) (inject t)
let whd_allnolet env t =
match kind t with
@@ -159,10 +159,10 @@ let whd_allnolet env t =
| Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
| Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
| Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
- whd_val (create_clos_infos allnolet env) (inject t)
+ whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
end
| Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ ->
- whd_val (create_clos_infos allnolet env) (inject t)
+ whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
(********************************************************************)
(* Conversion *)
@@ -354,6 +354,14 @@ let in_whnf (t,stk) =
| (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
| FLOCKED -> assert false
+type conv_tab = {
+ cnv_inf : clos_infos;
+ lft_tab : fconstr infos_tab;
+ rgt_tab : fconstr infos_tab;
+}
+(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
+ location contained both in tl and in tr. *)
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -362,10 +370,10 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Control.check_for_interrupt ();
(* First head reduce both terms *)
- let whd = whd_stack (infos_with_reds infos betaiotazeta) in
+ let ninfos = infos_with_reds infos.cnv_inf betaiotazeta in
let rec whd_both (t1,stk1) (t2,stk2) =
- let st1' = whd t1 stk1 in
- let st2' = whd t2 stk2 in
+ let st1' = whd_stack ninfos infos.lft_tab t1 stk1 in
+ let st2' = whd_stack ninfos infos.rgt_tab t2 stk2 in
(* Now, whd_stack on term2 might have modified st1 (due to sharing),
and st1 might not be in whnf anymore. If so, we iterate ccnv. *)
if in_whnf st1' then (st1',st2') else whd_both st1' st2' in
@@ -380,7 +388,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (Sort s1, Sort s2) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
- sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
+ sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -407,24 +415,24 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try
- let cuniv = conv_table_key infos fl1 fl2 cuniv in
+ let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with NotConvertible | Univ.UniverseInconsistency _ ->
(* else the oracle tells which constant is to be expanded *)
- let oracle = CClosure.oracle_of_infos infos in
+ let oracle = CClosure.oracle_of_infos infos.cnv_inf in
let (app1,app2) =
if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
- match unfold_reference infos fl1 with
+ match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 -> ((lft1, (def1, v1)), appr2)
| None ->
- (match unfold_reference infos fl2 with
+ (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 -> (appr1, (lft2, (def2, v2)))
| None -> raise NotConvertible)
else
- match unfold_reference infos fl2 with
+ match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 -> (appr1, (lft2, (def2, v2)))
| None ->
- (match unfold_reference infos fl1 with
+ (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 -> ((lft1, (def1, v1)), appr2)
| None -> raise NotConvertible)
in
@@ -434,11 +442,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* Projections: prefer unfolding to first-order unification,
which will happen naturally if the terms c1, c2 are not in constructor
form *)
- (match unfold_projection infos p1 with
+ (match unfold_projection infos.cnv_inf p1 with
| Some s1 ->
eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
| None ->
- match unfold_projection infos p2 with
+ match unfold_projection infos.cnv_inf p2 with
| Some s2 ->
eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
| None ->
@@ -452,26 +460,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
raise NotConvertible)
| (FProj (p1,c1), t2) ->
- (match unfold_projection infos p1 with
+ (match unfold_projection infos.cnv_inf p1 with
| Some s1 ->
eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
| None ->
(match t2 with
| FFlex fl2 ->
- (match unfold_reference infos fl2 with
+ (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 ->
eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
| None -> raise NotConvertible)
| _ -> raise NotConvertible))
| (t1, FProj (p2,c2)) ->
- (match unfold_projection infos p2 with
+ (match unfold_projection infos.cnv_inf p2 with
| Some s2 ->
eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
| None ->
(match t1 with
| FFlex fl1 ->
- (match unfold_reference infos fl1 with
+ (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 ->
eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
| None -> raise NotConvertible)
@@ -521,37 +529,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* only one constant, defined var or defined rel *)
| (FFlex fl1, c2) ->
- (match unfold_reference infos fl1 with
+ (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
| Some def1 ->
(** By virtue of the previous case analyses, we know [c2] is rigid.
Conversion check to rigid terms eventually implies full weak-head
reduction, so instead of repeatedly performing small-step
unfoldings, we perform reduction with all flags on. *)
- let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
- let r1 = whd_stack (infos_with_reds infos all) def1 v1 in
+ let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
+ let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in
eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
| None ->
match c2 with
| FConstruct ((ind2,j2),u2) ->
(try
let v2, v1 =
- eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
| (c1, FFlex fl2) ->
- (match unfold_reference infos fl2 with
+ (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
| Some def2 ->
(** Symmetrical case of above. *)
- let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
- let r2 = whd_stack (infos_with_reds infos all) def2 v2 in
+ let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
+ let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in
eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
| None ->
match c1 with
| FConstruct ((ind1,j1),u1) ->
(try let v1, v2 =
- eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
@@ -563,7 +571,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
- let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
+ let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
let nargs = CClosure.stack_args_size v1 in
if not (Int.equal nargs (CClosure.stack_args_size v2))
then raise NotConvertible
@@ -578,7 +586,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
- let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
+ let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
let nargs = CClosure.stack_args_size v1 in
if not (Int.equal nargs (CClosure.stack_args_size v2))
then raise NotConvertible
@@ -591,14 +599,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| (FConstruct ((ind1,j1),u1), _) ->
(try
let v1, v2 =
- eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| (_, FConstruct ((ind2,j2),u2)) ->
(try
let v2, v1 =
- eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+ eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
@@ -666,6 +674,11 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
let infos = create_clos_infos ~evars reds env in
+ let infos = {
+ cnv_inf = infos;
+ lft_tab = create_tab ();
+ rgt_tab = create_tab ();
+ } in
ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 125afb1a0..0fb79ff25 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -88,7 +88,7 @@ let lookup_map map =
let protect_red map env sigma c0 =
let evars ev = Evarutil.safe_evar_value sigma ev in
let c = EConstr.Unsafe.to_constr c0 in
- EConstr.of_constr (kl (create_clos_infos ~evars all env)
+ EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ())
(mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));;
let protect_tac map =
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index e42576d95..1718269b4 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -132,7 +132,7 @@ let mkSTACK = function
| STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk)
| v,stk -> STACK(0,v,stk)
-type cbv_infos = { infos : cbv_value infos; sigma : Evd.evar_map }
+type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map }
(* Change: zeta reduction cannot be avoided in CBV *)
@@ -316,7 +316,7 @@ let rec norm_head info env t stack =
and norm_head_ref k info env stack normt =
if red_set_ref (info_flags info.infos) normt then
- match ref_value_cache info.infos normt with
+ match ref_value_cache info.infos info.tab normt with
| Some body ->
if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
strip_appl (shift_value k body) stack
@@ -453,8 +453,8 @@ let cbv_norm infos constr =
(* constant bodies are normalized at the first expansion *)
let create_cbv_infos flgs env sigma =
let infos = create
- (fun old_info c -> cbv_stack_term { infos = old_info; sigma } TOP (subs_id 0) c)
+ (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c)
flgs
env
(Reductionops.safe_evar_value sigma) in
- { infos; sigma }
+ { tab = CClosure.create_tab (); infos; sigma }
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index a4097237f..33cbbc091 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -81,10 +81,12 @@ let infer_table_key infos variances c =
infer_generic_instance_eq variances u
| VarKey _ | RelKey _ -> variances
+let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk
+
let rec infer_fterm cv_pb infos variances hd stk =
Control.check_for_interrupt ();
- let open CClosure in
let hd,stk = whd_stack infos hd stk in
+ let open CClosure in
match fterm_of hd with
| FAtom a ->
begin match kind a with
@@ -114,7 +116,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
if Instance.is_empty u then variances
else
let nargs = stack_args_size stk in
- infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
+ infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u
in
infer_stack infos variances stk
| FConstruct (ctor,u) ->
@@ -122,7 +124,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
if Instance.is_empty u then variances
else
let nargs = stack_args_size stk in
- infer_constructor_instance_eq (info_env infos) variances ctor nargs u
+ infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u
in
infer_stack infos variances stk
| FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
@@ -159,7 +161,7 @@ and infer_vect infos variances v =
let infer_term cv_pb env variances c =
let open CClosure in
- let infos = create_clos_infos all env in
+ let infos = (create_clos_infos all env, create_tab ()) in
infer_fterm cv_pb infos variances (CClosure.inject c) []
let infer_arity_constructor is_arity env variances arcn =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 418ea271c..1e53faccd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1230,6 +1230,7 @@ let clos_norm_flags flgs env sigma t =
let evars ev = safe_evar_value sigma ev in
EConstr.of_constr (CClosure.norm_val
(CClosure.create_clos_infos ~evars flgs env)
+ (CClosure.create_tab ())
(CClosure.inject (EConstr.Unsafe.to_constr t)))
with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
@@ -1238,6 +1239,7 @@ let clos_whd_flags flgs env sigma t =
let evars ev = safe_evar_value sigma ev in
EConstr.of_constr (CClosure.whd_val
(CClosure.create_clos_infos ~evars flgs env)
+ (CClosure.create_tab ())
(CClosure.inject (EConstr.Unsafe.to_constr t)))
with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 22:14:52 +0000