diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 523 |
1 files changed, 310 insertions, 213 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 9e2af94b..f06b13d8 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,11 +19,12 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) +open Errors open Util open Pp -open Term open Names -open Declarations +open Term +open Vars open Environ open Esubst @@ -33,6 +34,7 @@ let share = ref true (* Profiling *) let beta = ref 0 let delta = ref 0 +let eta = ref 0 let zeta = ref 0 let evar = ref 0 let iota = ref 0 @@ -43,9 +45,10 @@ let reset () = prune := 0 let stop() = - msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ - str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++ - str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]") + msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ + str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ + int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ + str"]") let incr_cnt red cnt = if red then begin @@ -63,10 +66,10 @@ let with_stats c = end else Lazy.force c -let all_opaque = (Idpred.empty, Cpred.empty) -let all_transparent = (Idpred.full, Cpred.full) +let all_opaque = (Id.Pred.empty, Cpred.empty) +let all_transparent = (Id.Pred.full, Cpred.full) -let is_transparent_variable (ids, _) id = Idpred.mem id ids +let is_transparent_variable (ids, _) id = Id.Pred.mem id ids let is_transparent_constant (_, csts) cst = Cpred.mem cst csts module type RedFlagsSig = sig @@ -74,16 +77,18 @@ module type RedFlagsSig = sig type red_kind val fBETA : red_kind val fDELTA : red_kind + val fETA : red_kind val fIOTA : red_kind val fZETA : red_kind val fCONST : constant -> red_kind - val fVAR : identifier -> 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 mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool + val red_projection : reds -> projection -> bool end module RedFlags = (struct @@ -95,14 +100,16 @@ module RedFlags = (struct type reds = { r_beta : bool; r_delta : bool; + r_eta : bool; r_const : transparent_state; r_zeta : bool; r_iota : bool } - type red_kind = BETA | DELTA | IOTA | ZETA - | CONST of constant | VAR of identifier + type red_kind = BETA | DELTA | ETA | IOTA | ZETA + | CONST of constant | VAR of Id.t let fBETA = BETA let fDELTA = DELTA + let fETA = ETA let fIOTA = IOTA let fZETA = ZETA let fCONST kn = CONST kn @@ -110,12 +117,14 @@ module RedFlags = (struct let no_red = { r_beta = false; r_delta = false; + r_eta = false; r_const = all_opaque; r_zeta = false; r_iota = false } let red_add red = function | BETA -> { red with r_beta = true } + | 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 @@ -124,10 +133,11 @@ module RedFlags = (struct | ZETA -> { red with r_zeta = true } | VAR id -> let (l1,l2) = red.r_const in - { red with r_const = Idpred.add id l1, l2 } + { red with r_const = Id.Pred.add id l1, l2 } 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 @@ -136,7 +146,7 @@ module RedFlags = (struct | ZETA -> { red with r_zeta = false } | VAR id -> let (l1,l2) = red.r_const in - { red with r_const = Idpred.remove id l1, l2 } + { red with r_const = Id.Pred.remove id l1, l2 } let red_add_transparent red tr = { red with r_const = tr } @@ -145,19 +155,24 @@ module RedFlags = (struct let red_set red = function | 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 incr_cnt c delta | VAR id -> (* En attendant d'avoir des kn pour les Var *) let (l,_) = red.r_const in - let c = Idpred.mem id l in + let c = Id.Pred.mem id l in incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta | IOTA -> incr_cnt red.r_iota iota | DELTA -> (* Used for Rel/Var defined in context *) incr_cnt red.r_delta delta + let red_projection red p = + if Projection.unfolded p then true + else red_set red (fCONST (Projection.constant p)) + end : RedFlagsSig) open RedFlags @@ -185,9 +200,8 @@ let unfold_red kn = * * 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 = (4,[(1,c);(3,d)]) means there are 4 free rel variables - * and only those with index 1 and 3 have bodies which are c and d resp. - * * i_vars is the list of _defined_ named variables. + * * 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 @@ -197,72 +211,96 @@ let unfold_red kn = * instantiations (cbv or lazy) are. *) -type table_key = id_key +type table_key = constant puniverses tableKey + +let eq_pconstant_key (c,u) (c',u') = + eq_constant_key c c' && Univ.Instance.equal u u' + +module IdKeyHash = +struct + open Hashset.Combine + type t = table_key + let equal = Names.eq_table_key eq_pconstant_key + let hash = function + | ConstKey (c, _) -> combinesmall 1 (Constant.UserOrd.hash c) + | VarKey id -> combinesmall 2 (Id.hash id) + | RelKey i -> combinesmall 3 (Int.hash i) +end -let eq_table_key = Names.eq_id_key +module KeyTable = Hashtbl.Make(IdKeyHash) -type 'a infos = { - i_flags : reds; +let eq_table_key = IdKeyHash.equal + +type 'a infos_cache = { i_repr : 'a infos -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : int * (int * constr) list; - i_vars : (identifier * constr) list; - i_tab : (table_key, 'a) Hashtbl.t } + i_rels : constr option array; + i_tab : 'a KeyTable.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 -let ref_value_cache info ref = +let rec assoc_defined id = function +| [] -> raise Not_found +| (_, None, _) :: ctxt -> assoc_defined id ctxt +| (id', Some c, _) :: ctxt -> + if Id.equal id id' then c else assoc_defined id ctxt + +let ref_value_cache ({i_cache = cache} as infos) ref = try - Some (Hashtbl.find info.i_tab ref) + Some (KeyTable.find cache.i_tab ref) with Not_found -> try let body = match ref with | RelKey n -> - let (s,l) = info.i_rels in lift n (List.assoc (s-n) l) - | VarKey id -> List.assoc id info.i_vars - | ConstKey cst -> constant_value info.i_env cst + 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 + | VarKey id -> assoc_defined id (named_context cache.i_env) + | ConstKey cst -> constant_value_in cache.i_env cst in - let v = info.i_repr info body in - Hashtbl.add info.i_tab ref v; + let v = cache.i_repr infos body in + KeyTable.add cache.i_tab ref v; Some v with | Not_found (* List.assoc *) | NotEvaluableConst _ (* Const *) -> None -let evar_value info ev = - info.i_sigma ev - -let defined_vars flags env = -(* if red_local_const (snd flags) then*) - Sign.fold_named_context - (fun (id,b,_) e -> - match b with - | None -> e - | Some body -> (id, body)::e) - (named_context env) ~init:[] -(* else []*) +let evar_value cache ev = + cache.i_sigma ev let defined_rels flags env = (* if red_local_const (snd flags) then*) - Sign.fold_rel_context - (fun (id,b,t) (i,subs) -> - match b with - | None -> (i+1, subs) - | Some body -> (i+1, (i,body) :: subs)) - (rel_context env) ~init:(0,[]) + let ctx = rel_context env in + let len = List.length ctx in + let ans = Array.make len None in + let iter i (_, b, _) = match b with + | None -> () + | Some _ -> Array.unsafe_set ans i b + in + let () = List.iteri iter ctx in + ans (* else (0,[])*) let create mk_cl flgs env evars = - { i_flags = flgs; - i_repr = mk_cl; - i_env = env; - i_sigma = evars; - i_rels = defined_rels flgs env; - i_vars = defined_vars flgs env; - i_tab = Hashtbl.create 17 } + let cache = + { i_repr = mk_cl; + i_env = env; + i_sigma = evars; + i_rels = defined_rels flgs env; + i_tab = KeyTable.create 17 } + in { i_flags = flgs; i_cache = cache } (**********************************************************************) @@ -302,15 +340,17 @@ and fterm = | FAtom of constr (* Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive - | FConstruct of constructor + | FInd of pinductive + | FConstruct of pconstructor | FApp of fconstr * fconstr array + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCases of case_info * fconstr * fconstr * fconstr array - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FCase of case_info * fconstr * fconstr * fconstr array + | 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 + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential * fconstr subs | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -318,13 +358,13 @@ and fterm = let fterm_of v = v.term let set_norm v = v.norm <- Norm -let is_val v = v.norm = Norm +let is_val v = match v.norm with Norm -> true | _ -> false let mk_atom c = {norm=Norm;term=FAtom c} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) -let update v1 (no,t) = +let update v1 no t = if !share then (v1.norm <- no; v1.term <- t; @@ -337,6 +377,8 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array + | ZcaseT of case_info * constr * constr array * fconstr subs + | Zproj of int * int * constant | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -345,7 +387,7 @@ and stack = stack_member list let empty_stack = [] let append_stack v s = - if Array.length v = 0 then s else + 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 @@ -389,7 +431,7 @@ let rec stack_assign s p c = match s with Zapp nargs :: s) | _ -> s let rec stack_tail p s = - if p = 0 then s else + if Int.equal p 0 then s else match s with | Zapp args :: s -> let q = Array.length args in @@ -417,9 +459,9 @@ let rec lft_fconstr n ft = | FLOCKED -> assert false | _ -> {norm=ft.norm; term=FLIFT(n,ft)} let lift_fconstr k f = - if k=0 then f else lft_fconstr k f + if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = - if k=0 then v else Array.map (fun f -> lft_fconstr k f) v + if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v let clos_rel e i = match expand_rel i e with @@ -436,88 +478,21 @@ 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 + let _ = update 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 & m.norm = Red + if !share && begin match m.norm with Red -> true | _ -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in Zupdate(m)::s' else s -(* Closure optimization: *) -let rec compact_constr (lg, subs as s) c k = - match kind_of_term c with - Rel i -> - if i < k then c,s else - (try mkRel (k + lg - list_index (i-k+1) subs), (lg,subs) - with Not_found -> mkRel (k+lg), (lg+1, (i-k+1)::subs)) - | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s - | Evar(ev,v) -> - let (v',s) = compact_vect s v k in - if v==v' then c,s else mkEvar(ev,v'),s - | Cast(a,ck,b) -> - let (a',s) = compact_constr s a k in - let (b',s) = compact_constr s b k in - if a==a' && b==b' then c,s else mkCast(a', ck, b'), s - | App(f,v) -> - let (f',s) = compact_constr s f k in - let (v',s) = compact_vect s v k in - if f==f' && v==v' then c,s else mkApp(f',v'), s - | Lambda(n,a,b) -> - let (a',s) = compact_constr s a k in - let (b',s) = compact_constr s b (k+1) in - if a==a' && b==b' then c,s else mkLambda(n,a',b'), s - | Prod(n,a,b) -> - let (a',s) = compact_constr s a k in - let (b',s) = compact_constr s b (k+1) in - if a==a' && b==b' then c,s else mkProd(n,a',b'), s - | LetIn(n,a,ty,b) -> - let (a',s) = compact_constr s a k in - let (ty',s) = compact_constr s ty k in - let (b',s) = compact_constr s b (k+1) in - if a==a' && ty==ty' && b==b' then c,s else mkLetIn(n,a',ty',b'), s - | Fix(fi,(na,ty,bd)) -> - let (ty',s) = compact_vect s ty k in - let (bd',s) = compact_vect s bd (k+Array.length ty) in - if ty==ty' && bd==bd' then c,s else mkFix(fi,(na,ty',bd')), s - | CoFix(i,(na,ty,bd)) -> - let (ty',s) = compact_vect s ty k in - let (bd',s) = compact_vect s bd (k+Array.length ty) in - if ty==ty' && bd==bd' then c,s else mkCoFix(i,(na,ty',bd')), s - | Case(ci,p,a,br) -> - let (p',s) = compact_constr s p k in - let (a',s) = compact_constr s a k in - let (br',s) = compact_vect s br k in - if p==p' && a==a' && br==br' then c,s else mkCase(ci,p',a',br'),s -and compact_vect s v k = compact_v [] s v k (Array.length v - 1) -and compact_v acc s v k i = - if i < 0 then - let v' = Array.of_list acc in - if array_for_all2 (==) v v' then v,s else v',s - else - let (a',s') = compact_constr s v.(i) k in - compact_v (a'::acc) s' v k (i-1) - -(* Computes the minimal environment of a closure. - Idea: if the subs is not identity, the term will have to be - reallocated entirely (to propagate the substitution). So, - computing the set of free variables does not change the - complexity. *) -let optimise_closure env c = - if is_subs_id env then (env,c) else - let (c',(_,s)) = compact_constr (0,[]) c 1 in - let env' = - Array.map (fun i -> clos_rel env i) (Array.of_list s) in - (subs_cons (env', subs_id 0),c') - let mk_lambda env t = - let (env,t) = optimise_closure env t in let (rvars,t') = decompose_lam t in FLambda(List.length rvars, List.rev rvars, t', env) @@ -539,10 +514,10 @@ let mk_clos e t = | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } | Ind kn -> { norm = Norm; term = FInd kn } | Construct kn -> { norm = Cstr; term = FConstruct kn } - | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _) -> + | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} -let mk_clos_vect env v = Array.map (mk_clos env) v +let mk_clos_vect env 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 @@ -557,11 +532,13 @@ 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, Array.map (clos_fun env) v) } + 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 = FCases (ci, clos_fun env p, clos_fun env c, - Array.map (clos_fun env) v) } + term = FCaseT (ci, p, clos_fun env c, v, env) } | Fix fx -> { norm = Cstr; term = FFix (fx, env) } | CoFix cfx -> @@ -589,30 +566,37 @@ let rec to_constr constr_fun lfts v = | FAtom c -> exliftn lfts c | FCast (a,k,b) -> mkCast (constr_fun lfts a, k, constr_fun lfts b) - | FFlex (ConstKey op) -> mkConst op - | FInd op -> mkInd op - | FConstruct op -> mkConstruct op - | FCases (ci,p,c,ve) -> + | FFlex (ConstKey op) -> mkConstU op + | FInd op -> mkIndU op + | FConstruct op -> mkConstructU op + | FCase (ci,p,c,ve) -> mkCase (ci, constr_fun lfts p, constr_fun lfts c, - Array.map (constr_fun lfts) ve) + CArray.Fun1.map constr_fun lfts ve) + | 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) -> let n = Array.length bds in - let ftys = Array.map (mk_clos e) tys in - let fbds = Array.map (mk_clos (subs_liftn n e)) 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, Array.map (constr_fun lfts) ftys, - Array.map (constr_fun lfts') fbds)) + mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, + CArray.Fun1.map constr_fun lfts' fbds)) | FCoFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in - let ftys = Array.map (mk_clos e) tys in - let fbds = Array.map (mk_clos (subs_liftn n e)) 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, Array.map (constr_fun lfts) ftys, - Array.map (constr_fun lfts') fbds)) + mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, + CArray.Fun1.map constr_fun lfts' fbds)) | FApp (f,ve) -> mkApp (constr_fun lfts f, - Array.map (constr_fun lfts) ve) + CArray.Fun1.map constr_fun 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, @@ -630,9 +614,9 @@ let rec to_constr constr_fun lfts v = | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a | FCLOS (t,env) -> let fr = mk_clos2 env t in - let unfv = update v (fr.norm,fr.term) in + let unfv = update v fr.norm fr.term in to_constr constr_fun lfts unfv - | FLOCKED -> assert false (*mkVar(id_of_string"_LOCK_")*) + | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) (* This function defines the correspondance between constr and fconstr. When we find a closure whose substitution is the identity, @@ -641,11 +625,11 @@ let rec to_constr constr_fun lfts v = 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 -> + | 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 - | 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 + | 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 @@ -663,14 +647,19 @@ let rec zip m stk = | [] -> m | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s | Zcase(ci,p,br)::s -> - let t = FCases(ci, p, m, br) in + let t = FCase(ci, p, m, br) in + zip {norm=neutr m.norm; term=t} s + | 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 | 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 + zip (update rf m.norm m.term) s let fapp_stack (m,stk) = zip m stk @@ -682,8 +671,7 @@ let fapp_stack (m,stk) = zip m stk (strip_update_shift, through get_arg). *) (* optimised for the case where there are no shifts... *) -let strip_update_shift_app head stk = - assert (head.norm <> Red); +let strip_update_shift_app_red head stk = let rec strip_rec rstk h depth = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s @@ -691,13 +679,16 @@ let strip_update_shift_app 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 + strip_rec rstk (update m h.norm h.term) depth s | 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); + strip_update_shift_app_red head stack let get_nth_arg head n stk = - assert (head.norm <> Red); + assert (match head.norm with Red -> false | _ -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s @@ -710,10 +701,10 @@ let get_nth_arg head n stk = let bef = Array.sub args 0 n in let aft = Array.sub args (n+1) (q-n-1) in let stk' = - List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in + 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 + strip_rec rstk (update m h.norm h.term) n s | s -> (None, List.rev rstk @ s) in strip_rec [] head n stk @@ -722,7 +713,7 @@ 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 + let _hd = update 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 @@ -734,13 +725,14 @@ let rec get_args n tys f e stk = let eargs = Array.sub l n (na-n) in (Inl (subs_cons(args,e)), Zapp eargs :: s) else (* more lambdas *) - let etys = list_skipn na tys in + 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) (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s -> + | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ + | Zshift _ | Zupdate _ as e) :: s -> e :: eta_expand_stack s | [] -> [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] @@ -751,29 +743,88 @@ 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 k=depth then s else reloc_rargs_rec (depth-k) s + | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s | _ -> stk let reloc_rargs depth stk = - if depth = 0 then stk else reloc_rargs_rec depth stk + if Int.equal depth 0 then stk else reloc_rargs_rec depth stk -let rec drop_parameters depth n argstk = +let rec try_drop_parameters depth n argstk = match argstk with Zapp args::s -> let q = Array.length args in - if n > q then drop_parameters depth (n-q) s - else if n = q then reloc_rargs depth s + if n > q then try_drop_parameters depth (n-q) s + else if Int.equal n q then reloc_rargs depth s else let aft = Array.sub args n (q-n) in reloc_rargs depth (append_stack aft s) - | Zshift(k)::s -> drop_parameters (depth-k) n s + | Zshift(k)::s -> try_drop_parameters (depth-k) n s + | [] -> + if Int.equal n 0 then [] + else raise Not_found + | _ -> assert false + (* strip_update_shift_app only produces Zapp and Zshift items *) + +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") + + +let rec get_parameters depth n argstk = + match argstk with + Zapp args::s -> + let q = Array.length args in + if n > q then Array.append args (get_parameters depth (n-q) s) + else if Int.equal n q then [||] + else Array.sub args 0 n + | Zshift(k)::s -> + get_parameters (depth-k) n s | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - if n=0 then [] - else anomaly - "ill-typed term: found a match on a partially applied constructor" + if Int.equal n 0 then [||] + else raise Not_found (* Trying to eta-expand a partial application..., should do + eta expansion first? *) | _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) + +(** [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 + of ind, and the Constructor c of this inductive type applied to arguments + 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 + 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.CoFinite -> + (* (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 + | 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 + (* After drop_parameters we have a purely applicative stack *) + + (* Iota reduction: expansion of a fixpoint. * Given a fixpoint and a substitution, returns the corresponding * fixpoint body, and the substitution in which it should be @@ -798,39 +849,51 @@ let contract_fix_vect fix = in (subs_cons(Array.init nfix make_body, env), thisbody) - (*********************************************************************) (* A machine that inspects the head of a term until it finds an atom or a subterm that may produce a redex (abstraction, constructor, cofix, letin, constant), or a neutral term (product, inductive) *) -let rec knh m stk = +let rec knh info m stk = match m.term with - | FLIFT(k,a) -> knh a (zshift k stk) - | FCLOS(t,e) -> knht e t (zupdate m stk) + | FLIFT(k,a) -> knh info a (zshift k stk) + | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false - | FApp(a,b) -> knh a (append_stack b (zupdate m stk)) - | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk) + | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) + | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) + | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with - (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk') + (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') | (None, stk') -> (m,stk')) - | FCast(t,_,_) -> knh t 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) + (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> (m, stk) (* The same for pure terms *) -and knht e t stk = +and knht info e t stk = match kind_of_term t with | App(a,b) -> - knht e a (append_stack (mk_clos_vect e b) stk) + knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> - knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) - | Fix _ -> knh (mk_clos2 e t) stk - | Cast(a,_,_) -> knht e a stk - | Rel n -> knh (clos_rel e n) stk + knht info e t (ZcaseT(ci, p, br, e)::stk) + | Fix _ -> knh info (mk_clos2 e t) 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) @@ -845,8 +908,8 @@ let rec knr info m stk = (match get_args n tys f e stk with Inl e', s -> knit info e' f s | Inr lam, s -> (lam,s)) - | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) -> - (match ref_value_cache info (ConstKey kn) with + | 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 | None -> (set_norm m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> @@ -857,38 +920,46 @@ let rec knr info m stk = (match ref_value_cache info (RelKey k) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FConstruct(ind,c) when red_set info.i_flags fIOTA -> + | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with (depth, args, Zcase(ci,_,br)::s) -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in kni info br.(c-1) (rargs@s) + | (depth, args, ZcaseT(ci,_,br,e)::s) -> + assert (ci.ci_npar>=0); + let rargs = drop_parameters depth ci.ci_npar args in + knit info e br.(c-1) (rargs@s) | (_, cargs, Zfix(fx,par)::s) -> 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' + | (depth, args, Zproj (n, m, cst)::s) -> + let rargs = drop_parameters depth n args in + let rarg = project_nth_arg m rargs in + kni info rarg s | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, ((Zcase _::_) as stk')) -> + (_, args, (((Zcase _|ZcaseT _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info 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 | FEvar(ev,env) -> - (match evar_value info ev with + (match evar_value info.i_cache ev with Some c -> knit info env c stk | None -> (m,stk)) | _ -> (m,stk) (* Computes the weak head normal form of a term *) and kni info m stk = - let (hm,s) = knh m stk in + let (hm,s) = knh info m stk in knr info hm s and knit info e t stk = - let (ht,s) = knht e t stk in + let (ht,s) = knht info e t stk in knr info ht s let kh info v stk = fapp_stack(kni info v stk) @@ -903,6 +974,13 @@ let rec zip_term zfun m stk = | Zcase(ci,p,br)::s -> let t = mkCase(ci, zfun p, m, Array.map zfun br) in zip_term zfun t s + | ZcaseT(ci,p,br,e)::s -> + 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 -> + let t = mkProj (Projection.make p true, m) in + zip_term zfun t s | Zfix(fx,par)::s -> let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in zip_term zfun h s @@ -940,17 +1018,19 @@ and norm_head info m = | FProd(na,dom,rng) -> mkProd(na, kl info dom, kl info rng) | FCoFix((n,(na,tys,bds)),e) -> - let ftys = Array.map (mk_clos e) tys in + let ftys = CArray.Fun1.map mk_clos e tys in let fbds = - Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in - mkCoFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) 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)) | FFix((n,(na,tys,bds)),e) -> - let ftys = Array.map (mk_clos e) tys in + let ftys = CArray.Fun1.map mk_clos e tys in let fbds = - Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in - mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) 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)) | FEvar((i,args),env) -> mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args) + | FProj (p,c) -> + mkProj (p, kl info c) | t -> term_of_fconstr m (* Initialization and then normalization *) @@ -963,7 +1043,7 @@ let whd_val info v = let norm_val info v = with_stats (lazy (kl info v)) -let inject = mk_clos (subs_id 0) +let inject c = mk_clos (subs_id 0) c let whd_stack infos m stk = let k = kni infos m stk in @@ -975,5 +1055,22 @@ type clos_infos = fconstr infos let create_clos_infos ?(evars=fun _ -> None) flgs env = create (fun _ -> inject) flgs env evars - -let unfold_reference = ref_value_cache +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 } + +let unfold_reference info key = + match key with + | ConstKey (kn,_) -> + if red_set info.i_flags (fCONST kn) then + ref_value_cache info key + else None + | VarKey i -> + if red_set info.i_flags (fVAR i) then + ref_value_cache info key + else None + | _ -> ref_value_cache info key + |