diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 157 |
1 files changed, 120 insertions, 37 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cf40263f61..1e39756d47 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -56,7 +56,7 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj _p1::s1, Zproj _p2::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) -> + | (ZcaseT(_c1,_,_,_,_,_)::s1, ZcaseT(_c2,_,_,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -74,7 +74,7 @@ type lft_constr_stack_elt = Zlapp of (lift * fconstr) array | Zlproj of Projection.Repr.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack - | Zlcase of case_info * lift * constr * constr array * fconstr subs + | Zlcase of case_info * lift * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs | Zlprimitive of CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args and lft_constr_stack = lft_constr_stack_elt list @@ -109,8 +109,8 @@ let pure_stack lfts stk = | (Zfix(fx,a),(l,pstk)) -> let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) - | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,p,br,e)::pstk) + | (ZcaseT(ci,u,pms,p,br,e),(l,pstk)) -> + (l,Zlcase(ci,l,u,pms,p,br,e)::pstk) | (Zprimitive(op,c,rargs,kargs),(l,pstk)) -> (l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs, List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk)) @@ -233,6 +233,9 @@ let convert_instances ~flex u u' (s, check) = exception MustExpand +let convert_instances_cumul pb var u u' (s, check) = + (check.compare_cumul_instances pb var u u' s, check) + let get_cumulativity_constraints cv_pb variance u u' = match cv_pb with | CONV -> @@ -294,8 +297,6 @@ let conv_table_key infos ~nargs k1 k2 cuniv = | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible -exception IrregularPatternShape - let unfold_ref_with_args infos tab fl v = match unfold_reference infos tab fl with | Def def -> Some (def, v) @@ -327,17 +328,6 @@ let push_relevance infos r = let push_relevances infos nas = { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas } -let rec skip_pattern infos relevances n c1 c2 = - if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2 - else match kind c1, kind c2 with - | Lambda (x, _, c1), Lambda (_, _, c2) -> - skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2 - | _ -> raise IrregularPatternShape - -let skip_pattern infos n c1 c2 = - if Int.equal n 0 then infos, c1, c2 - else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2 - let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false @@ -364,6 +354,39 @@ let eta_expand_constructor env ((ind,ctor),u as pctor) = let c = Term.it_mkLambda_or_LetIn c ctx in inject c +let inductive_subst (mind, _) mib u pms = + let open Context.Rel.Declaration in + let ntypes = mib.mind_ntypes in + let rec self i accu = + if Int.equal i ntypes then accu + else self (i + 1) (subs_cons (inject (mkIndU ((mind, i), u))) accu) + in + let accu = self 0 (subs_id 0) in + let rec mk_pms pms ctx = match ctx, pms with + | [], [] -> accu + | LocalAssum _ :: ctx, c :: pms -> + let subs = mk_pms pms ctx in + subs_cons c subs + | LocalDef (_, c, _) :: ctx, pms -> + let c = Vars.subst_instance_constr u c in + let subs = mk_pms pms ctx in + subs_cons (mk_clos subs c) subs + | LocalAssum _ :: _, [] | [], _ :: _ -> assert false + in + mk_pms (List.rev pms) mib.mind_params_ctxt + +let esubst_of_rel_context_instance ctx u args e = + let open Context.Rel.Declaration in + let rec aux lft e args ctx = match ctx with + | [] -> lft, e + | LocalAssum _ :: ctx -> aux (lft + 1) (subs_lift e) (subs_lift args) ctx + | LocalDef (_, c, _) :: ctx -> + let c = Vars.subst_instance_constr u c in + let c = mk_clos args c in + aux lft (subs_cons c e) (subs_cons c args) ctx + in + aux 0 e args (List.rev ctx) + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv @@ -672,13 +695,23 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) -> + | FCaseInvert (ci1,u1,pms1,p1,_,_,br1,e1), FCaseInvert (ci2,u2,pms2,p2,_,_,br2,e2) -> (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible); let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in - let ccnv = ccnv CONV l2r infos el1 el2 in - let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in - Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv) - br1 br2 cuniv + let fold c1 c2 cuniv = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in + (** FIXME: cache the presence of let-bindings in the case_info *) + let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in + let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in + let cuniv = + let ind = (mind,snd ci1.ci_ind) in + let nargs = inductive_cumulativity_arguments ind in + convert_inductives CONV ind nargs u1 u2 cuniv + in + let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in + let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in + let cuniv = List.fold_right2 fold pms1 pms2 cuniv in + let cuniv = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 p1 p2 cuniv in + convert_branches ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 br1 br2 cuniv | FArray (u1,t1,ty1), FArray (u2,t2,ty2) -> let len = Parray.length_int t1 in @@ -714,11 +747,27 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> let cu2 = f fx1 fx2 cu1 in cmp_rec a1 a2 cu2 - | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> + | (Zlcase(ci1,l1,u1,pms1,p1,br1,e1),Zlcase(ci2,l2,u2,pms2,p2,br2,e2)) -> if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible; - let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in - convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 + let cu = cu1 in + (** FIXME: cache the presence of let-bindings in the case_info *) + let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in + let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in + let cu = + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + convert_instances ~flex:false u1 u2 cu + else + match mind.Declarations.mind_variance with + | None -> convert_instances ~flex:false u1 u2 cu + | Some variances -> convert_instances_cumul CONV variances u1 u2 cu + in + let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in + let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in + let fold_params c1 c2 accu = f (l1, c1) (l2, c2) accu in + let cu = List.fold_right2 fold_params pms1 pms2 cu in + let cu = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu in + convert_branches ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 br1 br2 cu | (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) -> if not (CPrimitives.equal op1 op2) then raise NotConvertible else let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in @@ -743,21 +792,55 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible -and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv = - (** Skip comparison of the pattern types. We know that the two terms are - living in a common type, thus this check is useless. *) - let fold n c1 c2 cuniv = match skip_pattern infos n c1 c2 with - | (infos, c1, c2) -> - let lft1 = el_liftn n lft1 in - let lft2 = el_liftn n lft2 in +and convert_under_context l2r infos e1 e2 lft1 lft2 ctx (nas1, c1) (nas2, c2) cu = + let n = Array.length nas1 in + let () = assert (Int.equal n (Array.length nas2)) in + let n, e1, e2 = match ctx with + | None -> (* nolet *) let e1 = subs_liftn n e1 in let e2 = subs_liftn n e2 in - ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv - | exception IrregularPatternShape -> - (** Might happen due to a shape invariant that is not enforced *) - ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv + (n, e1, e2) + | Some (ctx, u1, u2, args1, args2) -> + let n1, e1 = esubst_of_rel_context_instance ctx u1 args1 e1 in + let n2, e2 = esubst_of_rel_context_instance ctx u2 args2 e2 in + let () = assert (Int.equal n1 n2) in + n1, e1, e2 + in + let lft1 = el_liftn n lft1 in + let lft2 = el_liftn n lft2 in + let infos = push_relevances infos nas1 in + ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cu + +and convert_return_clause ind mib mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu = + let ctx = + if Int.equal mip.mind_nrealargs mip.mind_nrealdecls then None + else + let ctx, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in + let pms1 = inductive_subst ind mib u1 pms1 in + let pms2 = inductive_subst ind mib u1 pms2 in + let open Context.Rel.Declaration in + (* Add the inductive binder *) + let dummy = mkProp in + let ctx = LocalAssum (Context.anonR, dummy) :: ctx in + Some (ctx, u1, u2, pms1, pms2) + in + convert_under_context l2r infos e1 e2 l1 l2 ctx p1 p2 cu + +and convert_branches ind mib mip l2r infos e1 e2 lft1 lft2 u1 u2 pms1 pms2 br1 br2 cuniv = + let fold i (ctx, _) cuniv = + let ctx = + if Int.equal mip.mind_consnrealdecls.(i) mip.mind_consnrealargs.(i) then None + else + let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in + let pms1 = inductive_subst ind mib u1 pms1 in + let pms2 = inductive_subst ind mib u2 pms2 in + Some (ctx, u1, u2, pms1, pms2) + in + let c1 = br1.(i) in + let c2 = br2.(i) in + convert_under_context l2r infos e1 e2 lft1 lft2 ctx c1 c2 cuniv in - Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv + Array.fold_right_i fold mip.mind_nf_lc cuniv and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with | [], [] -> cuniv |