From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- kernel/cClosure.ml | 228 ++++++++++++++++++++++++++++------------------------- 1 file changed, 122 insertions(+), 106 deletions(-) (limited to 'kernel/cClosure.ml') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fe9ec579..08114abc 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* red_kind + val fCONST : Constant.t -> red_kind val fVAR : Id.t -> red_kind val no_red : reds val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds val red_add_transparent : reds -> transparent_state -> reds + val red_transparent : reds -> transparent_state val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool - val red_projection : reds -> projection -> bool + val red_projection : reds -> Projection.t -> bool end module RedFlags = (struct @@ -114,7 +117,7 @@ module RedFlags = (struct type red_kind = BETA | DELTA | ETA | MATCH | FIX | COFIX | ZETA - | CONST of constant | VAR of Id.t + | CONST of Constant.t | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fETA = ETA @@ -164,6 +167,8 @@ module RedFlags = (struct let (l1,l2) = red.r_const in { red with r_const = Id.Pred.remove id l1, l2 } + let red_transparent red = red.r_const + let red_add_transparent red tr = { red with r_const = tr } @@ -234,7 +239,7 @@ let unfold_red kn = * instantiations (cbv or lazy) are. *) -type table_key = constant puniverses tableKey +type table_key = Constant.t Univ.puniverses tableKey let eq_pconstant_key (c,u) (c',u') = eq_constant_key c c' && Univ.Instance.equal u u' @@ -254,12 +259,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 : constr option array; - i_tab : 'a KeyTable.t } + i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t; +} and 'a infos = { i_flags : reds; @@ -274,26 +281,29 @@ 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 = match ref with | RelKey n -> - let len = Array.length cache.i_rels in - let i = n - 1 in - let () = if i < 0 || len <= i then raise Not_found in - begin match Array.unsafe_get cache.i_rels i with - | None -> raise Not_found - | Some t -> lift n t - end + let open Context.Rel.Declaration in + let i = n - 1 in + let (d, _) = + try Range.get cache.i_rels i + with Invalid_argument _ -> raise Not_found + in + begin match d with + | LocalAssum _ -> raise Not_found + | LocalDef (_, t, _) -> lift n t + end | 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 *) @@ -303,27 +313,14 @@ let ref_value_cache ({i_cache = cache} as infos) ref = let evar_value cache ev = cache.i_sigma ev -let defined_rels flags env = -(* if red_local_const (snd flags) then*) - let ctx = rel_context env in - let len = List.length ctx in - let ans = Array.make len None in - let open Context.Rel.Declaration in - let iter i = function - | LocalAssum _ -> () - | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b) - in - let () = List.iteri iter ctx in - ans -(* else (0,[])*) - let create mk_cl flgs env evars = + let open Pre_env in let cache = { i_repr = mk_cl; i_env = env; i_sigma = evars; - i_rels = defined_rels flgs env; - i_tab = KeyTable.create 17 } + i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; + } in { i_flags = flgs; i_cache = cache } @@ -367,7 +364,7 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) @@ -401,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 + | Zproj of int * int * Constant.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -480,7 +477,8 @@ let rec lft_fconstr n ft = | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | _ -> {norm=ft.norm; term=FLIFT(n,ft)} + | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(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 = @@ -516,7 +514,7 @@ let zupdate m s = else s let mk_lambda env t = - let (rvars,t') = decompose_lam t in + let (rvars,t') = Term.decompose_lam t in FLambda(List.length rvars, List.rev rvars, t', env) let destFLambda clos_fun t = @@ -530,7 +528,7 @@ let destFLambda clos_fun t = (* Optimization: do not enclose variables in a closure. Makes variable access much faster *) let mk_clos e t = - match kind_of_term t with + match kind t with | Rel i -> clos_rel e i | Var x -> { norm = Red; term = FFlex (VarKey x) } | Const c -> { norm = Red; term = FFlex (ConstKey c) } @@ -540,14 +538,23 @@ let mk_clos e t = | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} -let mk_clos_vect env v = CArray.Fun1.map mk_clos env v +(** Hand-unrolling of the map function to bypass the call to the generic array + allocation *) +let mk_clos_vect env v = match v with +| [||] -> [||] +| [|v0|] -> [|mk_clos env v0|] +| [|v0; v1|] -> [|mk_clos env v0; mk_clos env v1|] +| [|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 (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct subterms. Could be used insted of mk_clos. *) let mk_clos_deep clos_fun env t = - match kind_of_term t with + match kind t with | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> mk_clos env t | Cast (a,k,b) -> @@ -646,7 +653,7 @@ let term_of_fconstr = 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 -> - compose_lam (List.rev tys) f + 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 @@ -785,7 +792,7 @@ let drop_parameters depth n argstk = try try_drop_parameters depth n argstk with Not_found -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") + anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor.") (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant @@ -793,14 +800,14 @@ let drop_parameters depth n argstk = s. @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (_,projs,pbs)) when - mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + mib.Declarations.mind_finite == Declarations.BiFinite -> (* (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 @@ -847,6 +854,14 @@ let contract_fix_vect fix = in (subs_cons(Array.init nfix make_body, env), thisbody) +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)) + else None + (*********************************************************************) (* A machine that inspects the head of a term until it finds an atom or a subterm that may produce a redex (abstraction, @@ -865,15 +880,9 @@ let rec knh info m stk = | (None, stk') -> (m,stk')) | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - let unf = Projection.unfolded p in - if unf || red_set info.i_flags (fCONST (Projection.constant p)) then - (match try Some (lookup_projection p (info_env info)) with Not_found -> None with - | None -> (m, stk) - | Some pb -> - knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, - Projection.constant p) - :: zupdate m stk)) - else (m,stk) + (match unfold_projection info p with + | None -> (m, stk) + | Some s -> knh info c (s :: zupdate m stk)) (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| @@ -882,7 +891,7 @@ let rec knh info m stk = (* The same for pure terms *) and knht info e t stk = - match kind_of_term t with + match kind t with | App(a,b) -> knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> @@ -899,23 +908,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 @@ -925,41 +934,44 @@ 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)) - | _ -> (m,stk) + | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _ + | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ + | FCLOS _ -> (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) (************************************************************************) @@ -987,68 +999,72 @@ 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 _ = fapp_stack(nm,s) in (* to unlock Zupdates! *) - zip_term (kl info) (norm_head info nm) s + 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 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) - | t -> term_of_fconstr m + 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 _ = fapp_stack k in (* to unlock Zupdates! *) +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 (* 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 _ -> 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 @@ -1056,14 +1072,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 -- cgit v1.2.3