From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/cClosure.ml | 233 ++++++++++++++++++++++++++++++----------------------- 1 file changed, 133 insertions(+), 100 deletions(-) (limited to 'kernel/cClosure.ml') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 08114abc..fd939402 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -31,7 +31,6 @@ open Environ open Esubst let stats = ref false -let share = ref true (* Profiling *) let beta = ref 0 @@ -265,7 +264,8 @@ type 'a infos_cache = { 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_rels : (Constr.rel_declaration * lazy_val) Range.t; + i_share : bool; } and 'a infos = { @@ -313,13 +313,13 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref = let evar_value cache ev = cache.i_sigma ev -let create mk_cl flgs env evars = - let open Pre_env in +let create ~repr ~share flgs env evars = let cache = - { i_repr = mk_cl; + { i_repr = repr; i_env = env; i_sigma = evars; - i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; + i_rels = env.env_rel_context.env_rel_map; + i_share = share; } in { i_flags = flgs; i_cache = cache } @@ -385,8 +385,8 @@ let mk_red f = {norm=Red;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) -let update v1 no t = - if !share then +let update ~share v1 no t = + if share then (v1.norm <- no; v1.term <- t; v1) @@ -398,7 +398,7 @@ let update v1 no t = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * Constant.t + | Zproj of Projection.Repr.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -482,7 +482,7 @@ let rec lft_fconstr n ft = let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = - if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v + if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v let clos_rel e i = match expand_rel i e with @@ -499,14 +499,16 @@ let compact_stack head stk = (* Be sure to create a new cell otherwise sharing would be lost by the update operation *) let h' = lft_fconstr depth head in - let _ = update m h'.norm h'.term in + (** The stack contains [Zupdate] marks only if in sharing mode *) + let _ = update ~share:true m h'.norm h'.term in strip_rec depth s | stk -> zshift depth stk in strip_rec 0 stk (* Put an update mark in the stack, only if needed *) -let zupdate m s = - if !share && begin match m.norm with Red -> true | _ -> false end +let zupdate info m s = + let share = info.i_cache.i_share in + if share && begin match m.norm with Red -> true | _ -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -547,7 +549,7 @@ let mk_clos_vect env v = match v with | [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|] | [|v0; v1; v2; v3|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] -| v -> CArray.Fun1.map mk_clos env v +| v -> Array.Fun1.map mk_clos env v (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct @@ -562,7 +564,7 @@ let mk_clos_deep clos_fun env t = term = FCast (clos_fun env a, k, clos_fun env b)} | App (f,v) -> { norm = Red; - term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) } + term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) } | Proj (p,c) -> { norm = Red; term = FProj (p, clos_fun env c) } @@ -588,78 +590,95 @@ let mk_clos_deep clos_fun env t = let mk_clos2 = mk_clos_deep mk_clos (* The inverse of mk_clos_deep: move back to constr *) -let rec to_constr constr_fun lfts v = +let rec to_constr lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) | FFlex (VarKey x) -> mkVar x | FAtom c -> exliftn lfts c | FCast (a,k,b) -> - mkCast (constr_fun lfts a, k, constr_fun lfts b) + mkCast (to_constr lfts a, k, to_constr lfts b) | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op | FCaseT (ci,p,c,ve,env) -> - mkCase (ci, constr_fun lfts (mk_clos env p), - constr_fun lfts c, - Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve) - | FFix ((op,(lna,tys,bds)),e) -> + if is_subs_id env && is_lift_id lfts then + mkCase (ci, p, to_constr lfts c, ve) + else + let subs = comp_subs lfts env in + mkCase (ci, subst_constr subs p, + to_constr lfts c, + Array.map (fun b -> subst_constr subs b) ve) + | FFix ((op,(lna,tys,bds)) as fx, e) -> + if is_subs_id e && is_lift_id lfts then + mkFix fx + else let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn n lfts in - mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) - | FCoFix ((op,(lna,tys,bds)),e) -> + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkFix (op, (lna, tys, bds)) + | FCoFix ((op,(lna,tys,bds)) as cfx, e) -> + if is_subs_id e && is_lift_id lfts then + mkCoFix cfx + else let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in - let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) + let subs_ty = comp_subs lfts e in + let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in + let tys = Array.Fun1.map subst_constr subs_ty tys in + let bds = Array.Fun1.map subst_constr subs_bd bds in + mkCoFix (op, (lna, tys, bds)) | FApp (f,ve) -> - mkApp (constr_fun lfts f, - CArray.Fun1.map constr_fun lfts ve) + mkApp (to_constr lfts f, + Array.Fun1.map to_constr lfts ve) | FProj (p,c) -> - mkProj (p,constr_fun lfts c) + mkProj (p,to_constr lfts c) - | FLambda _ -> - let (na,ty,bd) = destFLambda mk_clos2 v in - mkLambda (na, constr_fun lfts ty, - constr_fun (el_lift lfts) bd) + | FLambda (len, tys, f, e) -> + if is_subs_id e && is_lift_id lfts then + Term.compose_lam (List.rev tys) f + else + let subs = comp_subs lfts e in + let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in + let f = subst_constr (subs_liftn len subs) f in + Term.compose_lam (List.rev tys) f | FProd (n,t,c) -> - mkProd (n, constr_fun lfts t, - constr_fun (el_lift lfts) c) + mkProd (n, to_constr lfts t, + to_constr (el_lift lfts) c) | FLetIn (n,b,t,f,e) -> - let fc = mk_clos2 (subs_lift e) f in - mkLetIn (n, constr_fun lfts b, - constr_fun lfts t, - constr_fun (el_lift lfts) fc) + let subs = comp_subs (el_lift lfts) (subs_lift e) in + mkLetIn (n, to_constr lfts b, + to_constr lfts t, + subst_constr subs f) | FEvar ((ev,args),env) -> - mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args) - | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a + let subs = comp_subs lfts env in + mkEvar(ev,Array.map (fun a -> subst_constr subs a) args) + | FLIFT (k,a) -> to_constr (el_shft k lfts) a | FCLOS (t,env) -> - let fr = mk_clos2 env t in - let unfv = update v fr.norm fr.term in - to_constr constr_fun lfts unfv + if is_subs_id env && is_lift_id lfts then t + else + let subs = comp_subs lfts env in + subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) +and subst_constr subst c = match Constr.kind c with +| Rel i -> + begin match expand_rel i subst with + | Inl (k, lazy v) -> Vars.lift k v + | Inr (m, _) -> mkRel m + end +| _ -> + Constr.map_with_binders Esubst.subs_lift subst_constr subst c + +and comp_subs el s = + Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s + (* This function defines the correspondance between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) -let term_of_fconstr = - let rec term_of_fconstr_lift lfts v = - match v.term with - | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t - | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts -> - Term.compose_lam (List.rev tys) f - | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx - | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx - | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift el_id - - +let term_of_fconstr c = to_constr el_id c (* fstrong applies unfreeze_fun recursively on the (freeze) term and * yields a term. Assumes that the unfreeze_fun never returns a @@ -675,14 +694,15 @@ let rec zip m stk = | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s - | Zproj (i,j,cst) :: s -> - zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s + | Zproj p :: s -> + zip {norm=neutr m.norm; term=FProj(Projection.make p true,m)} s | Zfix(fx,par)::s -> zip fx (par @ append_stack [|m|] s) | Zshift(n)::s -> zip (lift_fconstr n m) s | Zupdate(rf)::s -> - zip (update rf m.norm m.term) s + (** The stack contains [Zupdate] marks only if in sharing mode *) + zip (update ~share:true rf m.norm m.term) s let fapp_stack (m,stk) = zip m stk @@ -702,7 +722,8 @@ let strip_update_shift_app_red head stk = strip_rec (Zapp args :: rstk) {norm=h.norm;term=FApp(h,args)} depth s | Zupdate(m)::s -> - strip_rec rstk (update m h.norm h.term) depth s + (** The stack contains [Zupdate] marks only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) depth s | stk -> (depth,List.rev rstk, stk) in strip_rec [] head 0 stk @@ -727,7 +748,8 @@ let get_nth_arg head n stk = List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> - strip_rec rstk (update m h.norm h.term) n s + (** The stack contains [Zupdate] mark only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) n s | s -> (None, List.rev rstk @ s) in strip_rec [] head n stk @@ -736,7 +758,8 @@ let get_nth_arg head n stk = let rec get_args n tys f e stk = match stk with Zupdate r :: s -> - let _hd = update r Cstr (FLambda(n,tys,f,e)) in + (** The stack contains [Zupdate] mark only if in sharing mode *) + let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in get_args n tys f e s | Zshift k :: s -> get_args n tys f (subs_shft (k,e)) s @@ -804,21 +827,26 @@ let drop_parameters depth n argstk = constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = + let open Declarations in let mib = lookup_mind (fst ind) env in - match mib.Declarations.mind_record with - | Some (Some (_,projs,pbs)) when - mib.Declarations.mind_finite == Declarations.BiFinite -> - (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> + (* disallow eta-exp for non-primitive records *) + if not (mib.mind_finite == BiFinite) then raise Not_found; + match Declareops.inductive_make_projections ind mib with + | Some projs -> + (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) - let pars = mib.Declarations.mind_nparams in - let right = fapp_stack (f, s') in - let (depth, args, s) = strip_update_shift_app m s in - (** Try to drop the params, might fail on partially applied constructors. *) - let argss = try_drop_parameters depth pars args in - let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) - term = FProj (Projection.make p true, right) }) projs in - argss, [Zapp hstack] - | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) + let pars = mib.Declarations.mind_nparams in + let right = fapp_stack (f, s') in + let (depth, args, s) = strip_update_shift_app m s in + (** Try to drop the params, might fail on partially applied constructors. *) + let argss = try_drop_parameters depth pars args in + let hstack = Array.map (fun p -> + { norm = Red; (* right can't be a constructor though *) + term = FProj (Projection.make p true, right) }) + projs + in + argss, [Zapp hstack] + | None -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with @@ -857,9 +885,7 @@ let contract_fix_vect fix = let unfold_projection info p = if red_projection info.i_flags p then - let open Declarations in - let pb = lookup_projection p (info_env info) in - Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p)) + Some (Zproj (Projection.repr p)) else None (*********************************************************************) @@ -870,10 +896,10 @@ let unfold_projection info p = let rec knh info m stk = match m.term with | FLIFT(k,a) -> knh info a (zshift k stk) - | FCLOS(t,e) -> knht info e t (zupdate m stk) + | FCLOS(t,e) -> knht info e t (zupdate info m stk) | FLOCKED -> assert false - | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk) + | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk)) + | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') @@ -882,7 +908,7 @@ let rec knh info m stk = | FProj (p,c) -> (match unfold_projection info p with | None -> (m, stk) - | Some s -> knh info c (s :: zupdate m stk)) + | Some s -> knh info c (s :: zupdate info m stk)) (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| @@ -940,9 +966,9 @@ let rec knr info tab m stk = let stk' = par @ append_stack [|rarg|] s in let (fxe,fxbd) = contract_fix_vect fx.term in 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 + | (depth, args, Zproj p::s) when use_match -> + let rargs = drop_parameters depth (Projection.Repr.npars p) args in + let rarg = project_nth_arg (Projection.Repr.arg p) rargs in kni info tab rarg s | (_,args,s) -> (m,args@s)) else (m,stk) @@ -984,7 +1010,7 @@ let rec zip_term zfun m stk = let t = mkCase(ci, zfun (mk_clos e p), m, Array.map (fun b -> zfun (mk_clos e b)) br) in zip_term zfun t s - | Zproj(_,_,p)::s -> + | Zproj p::s -> let t = mkProj (Projection.make p true, m) in zip_term zfun t s | Zfix(fx,par)::s -> @@ -1000,10 +1026,11 @@ let rec zip_term zfun m stk = 2- tries to rebuild the term. If a closure still has to be computed, calls itself recursively. *) let rec kl info tab m = + let share = info.i_cache.i_share in if is_val m then (incr prune; term_of_fconstr m) else let (nm,s) = kni info tab m [] in - let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) + let () = if share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) zip_term (kl info tab) (norm_head info tab nm) s (* no redex: go up for atoms and already normalized terms, go down @@ -1024,14 +1051,14 @@ and norm_head info tab m = | FProd(na,dom,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 ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in 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 ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in 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 tab (mk_clos env a)) args) @@ -1052,16 +1079,22 @@ let norm_val info tab v = let inject c = mk_clos (subs_id 0) c -let whd_stack infos tab m stk = +let whd_stack infos tab m stk = match m.norm with +| Whnf | Norm -> + (** No need to perform [kni] nor to unlock updates because + every head subterm of [m] is [Whnf] or [Norm] *) + knh infos m stk +| Red | Cstr -> let k = kni infos tab m stk in - let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) + let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos let create_clos_infos ?(evars=fun _ -> None) flgs env = - create (fun _ _ c -> inject c) flgs env evars + let share = (Environ.typing_flags env).Declarations.share_reduction in + create ~share ~repr:(fun _ _ c -> inject c) flgs env evars let create_tab () = KeyTable.create 17 -- cgit v1.2.3