diff options
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 146 |
1 files changed, 117 insertions, 29 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index d2256720c4..5613bf645e 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -34,6 +34,8 @@ open Environ open Vars open Esubst +module RelDecl = Context.Rel.Declaration + let stats = ref false (* Profiling *) @@ -342,8 +344,8 @@ and fterm = | 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 *) - | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs + | FCaseT of case_info * Univ.Instance.t * constr array * case_return * fconstr * case_branch array * fconstr subs (* predicate and branches are closures *) + | FCaseInvert of case_info * Univ.Instance.t * constr array * case_return * finvert * fconstr * case_branch array * fconstr subs | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs @@ -410,7 +412,7 @@ type 'a next_native_args = (CPrimitives.arg_kind * 'a) list type stack_member = | Zapp of fconstr array - | ZcaseT of case_info * constr * constr array * fconstr subs + | ZcaseT of case_info * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs | Zproj of Projection.Repr.t | Zfix of fconstr * stack | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args @@ -578,10 +580,11 @@ let rec to_constr lfts v = | FFlex (ConstKey op) -> mkConstU op | FInd op -> mkIndU op | FConstruct op -> mkConstructU op - | FCaseT (ci,p,c,ve,env) -> to_constr_case lfts ci p NoInvert c ve env - | FCaseInvert (ci,p,(univs,args),c,ve,env) -> + | FCaseT (ci, u, pms, p, c, ve, env) -> + to_constr_case lfts ci u pms p NoInvert c ve env + | FCaseInvert (ci, u, pms, p, (univs, args), c, ve, env) -> let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in - to_constr_case lfts ci p iv c ve env + to_constr_case lfts ci u pms p iv c ve env | FFix ((op,(lna,tys,bds)) as fx, e) -> if is_subs_id e && is_lift_id lfts then mkFix fx @@ -649,14 +652,20 @@ let rec to_constr lfts v = subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) -and to_constr_case lfts ci p iv c ve env = +and to_constr_case lfts ci u pms p iv c ve env = if is_subs_id env && is_lift_id lfts then - mkCase (ci, p, iv, to_constr lfts c, ve) + mkCase (ci, u, pms, p, iv, to_constr lfts c, ve) else let subs = comp_subs lfts env in - mkCase (ci, subst_constr subs p, iv, - to_constr lfts c, - Array.map (fun b -> subst_constr subs b) ve) + let f_ctx (nas, c) = + let c = subst_constr (Esubst.subs_liftn (Array.length nas) subs) c in + (nas, c) + in + mkCase (ci, u, Array.map (fun c -> subst_constr subs c) pms, + f_ctx p, + iv, + to_constr lfts c, + Array.map f_ctx ve) and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with | Rel i -> @@ -687,8 +696,8 @@ let rec zip m stk = match stk with | [] -> m | Zapp args :: s -> zip {mark=Mark.neutr m.mark; term=FApp(m, args)} s - | ZcaseT(ci,p,br,e)::s -> - let t = FCaseT(ci, p, m, br, e) in + | ZcaseT(ci, u, pms, p, br, e)::s -> + let t = FCaseT(ci, u, pms, p, m, br, e) in let mark = mark (neutr (Mark.red_state m.mark)) Unknown in zip {mark; term=t} s | Zproj p :: s -> @@ -763,6 +772,9 @@ let rec subs_consn v i n s = if Int.equal i n then s else subs_consn v (i + 1) n (subs_cons v.(i) s) +let subs_consv v s = + subs_consn v 0 (Array.length v) s + (* 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 = function @@ -870,6 +882,74 @@ let drop_parameters depth n argstk = (* 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 inductive_subst (ind, _) mib u pms e = + let rec self i accu = + if Int.equal i mib.mind_ntypes then accu + else + let c = inject (mkIndU ((ind, i), u)) in + self (i + 1) (subs_cons c accu) + in + let self = self 0 (subs_id 0) in + let rec mk_pms i ctx = match ctx with + | [] -> self + | RelDecl.LocalAssum _ :: ctx -> + let c = mk_clos e pms.(i) in + let subs = mk_pms (i - 1) ctx in + subs_cons c subs + | RelDecl.LocalDef (_, c, _) :: ctx -> + let c = Vars.subst_instance_constr u c in + let subs = mk_pms i ctx in + subs_cons (mk_clos subs c) subs + in + mk_pms (Array.length pms - 1) mib.mind_params_ctxt + +(* Iota-reduction: feed the arguments of the constructor to the branch *) +let get_branch infos depth ci u pms (ind, c) br e args = + let i = c - 1 in + let args = drop_parameters depth ci.ci_npar args in + let (_nas, br) = br.(i) in + if Int.equal ci.ci_cstr_ndecls.(i) ci.ci_cstr_nargs.(i) then + (* No let-bindings in the constructor, we don't have to fetch the + environment to know the value of the branch. *) + let rec push e stk = match stk with + | [] -> e + | Zapp v :: stk -> push (subs_consv v e) stk + | (Zshift _ | ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ -> + assert false + in + let e = push e args in + (br, e) + else + (* The constructor contains let-bindings, but they are not physically + present in the match, so we fetch them in the environment. *) + let env = info_env infos in + let mib = Environ.lookup_mind (fst ind) env in + let mip = mib.mind_packets.(snd ind) in + let (ctx, _) = mip.mind_nf_lc.(i) in + let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in + let map = function + | Zapp args -> args + | Zshift _ | ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _ -> + assert false + in + let ind_subst = inductive_subst ind mib u pms e in + let args = Array.concat (List.map map args) in + let rec push i e = function + | [] -> [] + | RelDecl.LocalAssum _ :: ctx -> + let ans = push (pred i) e ctx in + args.(i) :: ans + | RelDecl.LocalDef (_, b, _) :: ctx -> + let ans = push i e ctx in + let b = subst_instance_constr u b in + let s = Array.rev_of_list ans in + let e = subs_consv s ind_subst in + let v = mk_clos e b in + v :: ans + in + let ext = push (Array.length args - 1) [] ctx in + (br, subs_consv (Array.rev_of_list ext) e) + (** [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 of ind, and the Constructor c of this inductive type applied to arguments @@ -909,7 +989,6 @@ let rec project_nth_arg n = function | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> 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 @@ -1269,7 +1348,7 @@ let rec knh info 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 info m stk)) - | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) + | FCaseT(ci,u,pms,p,t,br,e) -> knh info t (ZcaseT(ci,u,pms,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') @@ -1289,10 +1368,10 @@ and knht info e t stk = match kind t with | App(a,b) -> knht info e a (append_stack (mk_clos_vect e b) stk) - | Case(ci,p,NoInvert,t,br) -> - knht info e t (ZcaseT(ci, p, br, e)::stk) - | Case(ci,p,CaseInvert{univs;args},t,br) -> - let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in + | Case(ci,u,pms,p,NoInvert,t,br) -> + knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk) + | Case(ci,u,pms,p,CaseInvert{univs;args},t,br) -> + let term = FCaseInvert (ci, u, pms, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in { mark = mark Red Unknown; term }, stk | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk @@ -1347,15 +1426,15 @@ let rec knr info tab m stk = | Def v -> kni info tab v stk | Primitive _ -> assert false | OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk))) - | FConstruct((_ind,c),_u) -> + | FConstruct(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 [@ocaml.warning "-4"] strip_update_shift_app m stk with - | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match -> + | (depth, args, ZcaseT(ci,u,pms,_,br,e)::s) when use_match -> assert (ci.ci_npar>=0); - let rargs = drop_parameters depth ci.ci_npar args in - knit info tab e br.(c-1) (rargs@s) + let (br, e) = get_branch info depth ci u pms c br e args in + knit info tab e br s | (_, cargs, Zfix(fx,par)::s) when use_fix -> let rarg = fapp_stack(m,cargs) in let stk' = par @ append_stack [|rarg|] s in @@ -1399,7 +1478,7 @@ let rec knr info tab m stk = kni info tab a (Zprimitive(op,c,rargs,nargs)::s) end | (_, _, s) -> (m, s)) - | FCaseInvert (ci,_p,iv,_c,v,env) when red_set info.i_flags fMATCH -> + | FCaseInvert (ci, _u, _pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH -> begin match case_inversion info tab ci iv v with | Some c -> knit info tab env c stk | None -> (m, stk) @@ -1419,7 +1498,12 @@ and knit info tab e t stk = and case_inversion info tab ci (univs,args) v = let open Declarations in - if Array.is_empty args then Some v.(0) + (* No binders / lets at all in the unique branch *) + let v = match v with + | [| [||], v |] -> v + | _ -> assert false + in + if Array.is_empty args then Some v else let env = info_env info in let ind = ci.ci_ind in @@ -1437,7 +1521,7 @@ and case_inversion info tab ci (univs,args) v = !conv {info with i_flags=all} tab expected index in if Array.for_all_i check_index 0 indices - then Some v.(0) else None + then Some v else None let kh info tab v stk = fapp_stack(kni info tab v stk) @@ -1448,9 +1532,13 @@ let rec zip_term zfun m stk = | [] -> m | Zapp args :: s -> zip_term zfun (mkApp(m, Array.map zfun args)) s - | ZcaseT(ci,p,br,e)::s -> - let t = mkCase(ci, zfun (mk_clos e p), NoInvert, m, - Array.map (fun b -> zfun (mk_clos e b)) br) in + | ZcaseT(ci, u, pms, p, br, e) :: s -> + let zip_ctx (nas, c) = + let e = Esubst.subs_liftn (Array.length nas) e in + (nas, zfun (mk_clos e c)) + in + let t = mkCase(ci, u, Array.map (fun c -> zfun (mk_clos e c)) pms, zip_ctx p, + NoInvert, m, Array.map zip_ctx br) in zip_term zfun t s | Zproj p::s -> let t = mkProj (Projection.make p true, m) in |