diff options
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 560 |
1 files changed, 269 insertions, 291 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5f683790c1..1f61bcae2e 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -21,6 +21,8 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) +[@@@ocaml.warning "+4"] + open CErrors open Util open Pp @@ -31,7 +33,6 @@ open Environ open Esubst let stats = ref false -let share = ref true (* Profiling *) let beta = ref 0 @@ -71,11 +72,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = (Id.Pred.empty, Cpred.empty) -let all_transparent = (Id.Pred.full, Cpred.full) - -let is_transparent_variable (ids, _) id = Id.Pred.mem id ids -let is_transparent_constant (_, csts) cst = Cpred.mem cst csts +let all_opaque = TransparentState.empty +let all_transparent = TransparentState.full module type RedFlagsSig = sig type reds @@ -92,11 +90,11 @@ module type RedFlagsSig = sig 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 red_add_transparent : reds -> TransparentState.t -> reds + val red_transparent : reds -> TransparentState.t 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 @@ -105,11 +103,13 @@ module RedFlags = (struct (* [r_const=(false,cl)] means only those in [cl] *) (* [r_delta=true] just mean [r_const=(true,[])] *) + open TransparentState + type reds = { r_beta : bool; r_delta : bool; r_eta : bool; - r_const : transparent_state; + r_const : TransparentState.t; r_zeta : bool; r_match : bool; r_fix : bool; @@ -142,30 +142,30 @@ module RedFlags = (struct | ETA -> { red with r_eta = true } | DELTA -> { red with r_delta = true; r_const = all_transparent } | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.add kn l2 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } } | MATCH -> { red with r_match = true } | FIX -> { red with r_fix = true } | COFIX -> { red with r_cofix = true } | ZETA -> { red with r_zeta = true } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.add id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } } let red_sub red = function | BETA -> { red with r_beta = false } | ETA -> { red with r_eta = false } | DELTA -> { red with r_delta = false } | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.remove kn l2 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } } | MATCH -> { red with r_match = false } | FIX -> { red with r_fix = false } | COFIX -> { red with r_cofix = false } | ZETA -> { red with r_zeta = false } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.remove id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } } let red_transparent red = red.r_const @@ -178,12 +178,10 @@ module RedFlags = (struct | BETA -> incr_cnt red.r_beta beta | ETA -> incr_cnt red.r_eta eta | CONST kn -> - let (_,l) = red.r_const in - let c = Cpred.mem kn l in + let c = is_transparent_constant red.r_const kn in incr_cnt c delta | VAR id -> (* En attendant d'avoir des kn pour les Var *) - let (l,_) = red.r_const in - let c = Id.Pred.mem id l in + let c = is_transparent_variable red.r_const id in incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta | MATCH -> incr_cnt red.r_match nb_match @@ -225,11 +223,6 @@ let unfold_red kn = * abstractions, storing a representation (of type 'a) of the body of * this constant or abstraction. * * i_tab is the cache table of the results - * * i_repr is the function to get the representation from the current - * state of the cache and the body of the constant. The result - * is stored in the table. - * * i_rels is the array of free rel variables together with their optional - * body * * ref_value_cache searchs in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't @@ -257,72 +250,11 @@ end 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 -> '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; -} - -and 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -let info_flags info = info.i_flags -let info_env info = info.i_cache.i_env - open Context.Named.Declaration 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) tab ref = - try - Some (KeyTable.find tab ref) - with Not_found -> - try - let body = - match ref with - | RelKey n -> - 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 tab body in - KeyTable.add tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - -let evar_value cache ev = - cache.i_sigma ev - -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 = (Environ.pre_env env).env_rel_context.env_rel_map; - } - in { i_flags = flgs; i_cache = cache } - +| LocalAssum _ -> raise Not_found (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -359,17 +291,16 @@ type fconstr = { and fterm = | FRel of int | FAtom of constr (* Metas and Sorts *) - | FCast of fconstr * cast_kind * fconstr | FFlex of table_key | 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 *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs - | FProd of Name.t * fconstr * fconstr + | FProd of Name.t * fconstr * constr * fconstr subs | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr @@ -378,27 +309,44 @@ and fterm = let fterm_of v = v.term let set_norm v = v.norm <- Norm -let is_val v = match v.norm with Norm -> true | _ -> false +let is_val v = match v.norm with Norm -> true | Cstr | Whnf | Red -> false let mk_atom c = {norm=Norm;term=FAtom c} 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) else {norm=no;term=t} +(** Reduction cache *) + +type infos_cache = { + i_env : env; + i_sigma : existential -> constr option; + i_share : bool; +} + +type clos_infos = { + i_flags : reds; + i_cache : infos_cache } + +type clos_tab = fconstr KeyTable.t + +let info_flags info = info.i_flags +let info_env info = info.i_cache.i_env + (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) 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 @@ -410,20 +358,21 @@ let append_stack v s = if Int.equal (Array.length v) 0 then s else match s with | Zapp l :: s -> Zapp (Array.append v l) :: s - | _ -> Zapp v :: s + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> + Zapp v :: s (* Collapse the shifts in the stack *) let zshift n s = match (n,s) with (0,_) -> s | (_,Zshift(k)::s) -> Zshift(n+k)::s - | _ -> Zshift(n)::s + | (_,(ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zupdate _) :: _) | _,[] -> Zshift(n)::s let rec stack_args_size = function | Zapp v :: s -> Array.length v + stack_args_size s | Zshift(_)::s -> stack_args_size s | Zupdate(_)::s -> stack_args_size s - | _ -> 0 + | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0 (* When used as an argument stack (only Zapp can appear) *) let rec decomp_stack = function @@ -433,12 +382,12 @@ let rec decomp_stack = function | 1 -> Some (v.(0), s) | _ -> Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) - | _ -> None + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> None let array_of_stack s = let rec stackrec = function | [] -> [] | Zapp args :: s -> args :: (stackrec s) - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ -> assert false in Array.concat (stackrec s) let rec stack_assign s p c = match s with | Zapp args :: s -> @@ -449,7 +398,7 @@ let rec stack_assign s p c = match s with (let nargs = Array.copy args in nargs.(p) <- c; Zapp nargs :: s) - | _ -> s + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> s let rec stack_tail p s = if Int.equal p 0 then s else match s with @@ -457,13 +406,13 @@ let rec stack_tail p s = let q = Array.length args in if p >= q then stack_tail (p-q) s else Zapp (Array.sub args p (q-p)) :: s - | _ -> failwith "stack_tail" + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> failwith "stack_tail" let rec stack_nth s p = match s with | Zapp args :: s -> let q = Array.length args in if p >= q then stack_nth s (p-q) else args.(p) - | _ -> raise Not_found + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> raise Not_found (* Lifting. Preserves sharing (useful only for cell with norm=Red). lft_fconstr always create a new cell, while lift_fconstr avoids it @@ -477,12 +426,12 @@ 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 - | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FFlex (RelKey _) | FAtom _ | 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 = - 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 +448,17 @@ 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 + | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _) :: _ | []) as 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 | Norm | Whnf | Cstr -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -518,12 +470,12 @@ let mk_lambda env t = FLambda(List.length rvars, List.rev rvars, t', env) let destFLambda clos_fun t = - match t.term with - FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) - | FLambda(n,(na,ty)::tys,b,e) -> - (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) - | _ -> assert false - (* t must be a FLambda and binding list cannot be empty *) + match [@ocaml.warning "-4"] t.term with + | FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) + | FLambda(n,(na,ty)::tys,b,e) -> + (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) + | _ -> assert false +(* t must be a FLambda and binding list cannot be empty *) (* Optimization: do not enclose variables in a closure. Makes variable access much faster *) @@ -538,6 +490,8 @@ let mk_clos e t = | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} +let inject c = mk_clos (subs_id 0) c + (** Hand-unrolling of the map function to bypass the call to the generic array allocation *) let mk_clos_vect env v = match v with @@ -547,119 +501,128 @@ 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 - subterms. - Could be used insted of mk_clos. *) -let mk_clos_deep clos_fun env t = - match kind t with - | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> - mk_clos env t - | Cast (a,k,b) -> - { norm = Red; - 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) } - | Proj (p,c) -> - { norm = Red; - term = FProj (p, clos_fun env c) } - | Case (ci,p,c,v) -> - { norm = Red; - term = FCaseT (ci, p, clos_fun env c, v, env) } - | Fix fx -> - { norm = Cstr; term = FFix (fx, env) } - | CoFix cfx -> - { norm = Cstr; term = FCoFix(cfx,env) } - | Lambda _ -> - { norm = Cstr; term = mk_lambda env t } - | Prod (n,t,c) -> - { norm = Whnf; - term = FProd (n, clos_fun env t, clos_fun (subs_lift env) c) } - | LetIn (n,b,t,c) -> - { norm = Red; - term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } - | Evar ev -> - { norm = Red; term = FEvar(ev,env) } - -(* A better mk_clos? *) -let mk_clos2 = mk_clos_deep mk_clos +let ref_value_cache ({ i_cache = cache; _ }) tab ref = + try + Some (KeyTable.find tab ref) + with Not_found -> + try + let body = + match ref with + | RelKey n -> + let open! Context.Rel.Declaration in + let i = n - 1 in + let (d, _) = + try Range.get cache.i_env.env_rel_context.env_rel_map 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 = inject body in + KeyTable.add tab ref v; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None -(* The inverse of mk_clos_deep: move back to constr *) -let rec to_constr constr_fun lfts v = +(* The inverse of mk_clos: move back to constr *) +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) | 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) - - | FLambda _ -> - let (na,ty,bd) = destFLambda mk_clos2 v in - mkLambda (na, constr_fun lfts ty, - constr_fun (el_lift lfts) bd) - | FProd (n,t,c) -> - mkProd (n, constr_fun lfts t, - constr_fun (el_lift lfts) c) + mkProj (p,to_constr lfts c) + + | 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, e) -> + if is_subs_id e && is_lift_id lfts then + mkProd (n, to_constr lfts t, c) + else + let subs' = comp_subs lfts e in + mkProd (n, to_constr lfts t, subst_constr (subs_lift subs') 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 [@ocaml.warning "-4"] 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 +638,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,16 +666,19 @@ 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 - | stk -> (depth,List.rev rstk, stk) in + (** The stack contains [Zupdate] marks only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) depth s + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + (depth,List.rev rstk, stk) + in strip_rec [] head 0 stk let strip_update_shift_app head stack = - assert (match head.norm with Red -> false | _ -> true); + assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true); strip_update_shift_app_red head stack let get_nth_arg head n stk = - assert (match head.norm with Red -> false | _ -> true); + assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s @@ -727,16 +694,17 @@ 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 - | s -> (None, List.rev rstk @ s) in + (** The stack contains [Zupdate] mark only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) n s + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as s -> (None, List.rev rstk @ s) in strip_rec [] head n stk (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) -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 +let rec get_args n tys f e = function + | Zupdate r :: s -> + (** 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 @@ -750,7 +718,8 @@ let rec get_args n tys f e stk = else (* more lambdas *) let etys = List.skipn na tys in get_args (n-na) etys f (subs_cons(l,e)) s - | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function @@ -762,19 +731,17 @@ let rec eta_expand_stack = function (* Iota reduction: extract the arguments to be passed to the Case branches *) -let rec reloc_rargs_rec depth stk = - match stk with - Zapp args :: s -> - Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s - | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s - | _ -> stk +let rec reloc_rargs_rec depth = function + | Zapp args :: s -> + Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s + | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s + | ((ZcaseT _ | Zproj _ | Zfix _ | Zupdate _) :: _ | []) as stk -> stk let reloc_rargs depth stk = if Int.equal depth 0 then stk else reloc_rargs_rec depth stk -let rec try_drop_parameters depth n argstk = - match argstk with - Zapp args::s -> +let rec try_drop_parameters depth n = function + | Zapp args::s -> let q = Array.length args in if n > q then try_drop_parameters depth (n-q) s else if Int.equal n q then reloc_rargs depth s @@ -785,7 +752,7 @@ let rec try_drop_parameters depth n argstk = | [] -> if Int.equal n 0 then [] else raise Not_found - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _) :: _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) let drop_parameters depth n argstk = @@ -804,29 +771,33 @@ 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 rec project_nth_arg n argstk = - match argstk with + 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 = function | Zapp args :: s -> let q = Array.length args in if n >= q then project_nth_arg (n - q) s else (* n < q *) args.(n) - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _) :: _ | [] -> assert false (* After drop_parameters we have a purely applicative stack *) @@ -841,7 +812,7 @@ let rec project_nth_arg n argstk = (* does not deal with FLIFT *) let contract_fix_vect fix = let (thisbody, make_body, env, nfix) = - match fix with + match [@ocaml.warning "-4"] fix with | FFix (((reci,i),(_,_,bds as rdcl)),env) -> (bds.(i), (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), @@ -857,9 +828,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,19 +839,18 @@ 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') | (None, stk') -> (m,stk')) - | FCast(t,_,_) -> knh info t 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 _| @@ -896,13 +864,18 @@ and knht info e t stk = knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk) - | Fix _ -> knh info (mk_clos2 e t) stk + | Fix fx -> knh info { norm = Cstr; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (p,c) -> knh info (mk_clos2 e t) stk - | (Lambda _|Prod _|Construct _|CoFix _|Ind _| - LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> - (mk_clos2 e t, stk) + | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> (mk_clos e t, stk) + | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk + | Prod (n, t, c) -> + { norm = Whnf; term = FProd (n, mk_clos e t, c, e) }, stk + | LetIn (n,b,t,c) -> + { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk (************************************************************************) @@ -926,11 +899,11 @@ let rec knr info tab m 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) -> + | FConstruct((_ind,c),_u) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in if use_match || use_fix then - (match strip_update_shift_app m stk with + (match [@ocaml.warning "-4"] strip_update_shift_app m stk with | (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 @@ -940,25 +913,25 @@ 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) | FCoFix _ when red_set info.i_flags fCOFIX -> (match strip_update_shift_app m stk with - (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> + | (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info tab fxe fxbd (args@stk') - | (_,args,s) -> (m,args@s)) + | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] as s)) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info tab (subs_cons([|v|],e)) bd stk | FEvar(ev,env) -> - (match evar_value info.i_cache ev with + (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) - | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _ + | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ | FCLOS _ -> (m, stk) @@ -984,7 +957,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 -> @@ -992,7 +965,7 @@ let rec zip_term zfun m stk = zip_term zfun h s | Zshift(n)::s -> zip_term zfun (lift n m) s - | Zupdate(rf)::s -> + | Zupdate(_rf)::s -> zip_term zfun m s (* Computes the strong normal form of a term. @@ -1000,10 +973,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 @@ -1011,7 +985,7 @@ let rec kl info tab 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) -> + | FLambda(_n,tys,f,e) -> let (e',rvtys) = List.fold_left (fun (e,ctxt) (na,ty) -> (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) @@ -1021,23 +995,23 @@ and norm_head info tab m = | FLetIn(na,a,b,f,e) -> let c = mk_clos (subs_lift e) f in mkLetIn(na, kl info tab a, kl info tab b, kl info tab c) - | FProd(na,dom,rng) -> - mkProd(na, kl info tab dom, kl info tab rng) + | FProd(na,dom,rng,e) -> + mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) 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) | FProj (p,c) -> mkProj (p, kl info tab c) - | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _ + | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _ | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m (* Initialization and then normalization *) @@ -1050,25 +1024,29 @@ let whd_val info tab 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 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 + let cache = { + i_env = env; + i_sigma = evars; + i_share = share; + } in + { i_flags = flgs; i_cache = cache } 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 - let infos_with_reds infos reds = { infos with i_flags = reds } @@ -1082,4 +1060,4 @@ let unfold_reference info tab key = if red_set info.i_flags (fVAR i) then ref_value_cache info tab key else None - | _ -> ref_value_cache info tab key + | RelKey _ -> ref_value_cache info tab key |