From c7e32090dc4f2b940a54ff9aa64a63fda6e24c50 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 23 Oct 2018 13:56:34 +0200 Subject: Integrate convert_shape into convert_stack. No reason to split the code, this function is only used once. --- kernel/reduction.ml | 55 ++++++++++++++++++++++++----------------------------- 1 file changed, 25 insertions(+), 30 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 18697d07e5..09d65e1640 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -288,32 +288,6 @@ let conv_table_key infos k1 k2 cuniv = | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible -let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = - let rec cmp_rec pstk1 pstk2 cuniv = - match (pstk1,pstk2) with - | (z1::s1, z2::s2) -> - let cu1 = cmp_rec s1 s2 cuniv in - (match (z1,z2) with - | (Zlapp a1,Zlapp a2) -> - Array.fold_right2 f a1 a2 cu1 - | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> - if not (Projection.Repr.equal c1 c2) then - raise NotConvertible - else cu1 - | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> - let cu2 = f fx1 fx2 cu1 in - cmp_rec a1 a2 cu2 - | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> - if not (fmind ci1.ci_ind ci2.ci_ind) then - raise NotConvertible; - let cu2 = f (l1,p1) (l2,p2) cu1 in - Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 - | _ -> assert false) - | _ -> cuniv in - if compare_stack_shape stk1 stk2 then - cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv - else raise NotConvertible - type conv_tab = { cnv_inf : clos_infos; lft_tab : clos_tab; @@ -611,10 +585,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | FProd _ | FEvar _), _ -> raise NotConvertible and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = - compare_stacks - (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) - (eq_ind) - lft1 stk1 lft2 stk2 cuniv + let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in + let rec cmp_rec pstk1 pstk2 cuniv = + match (pstk1,pstk2) with + | (z1::s1, z2::s2) -> + let cu1 = cmp_rec s1 s2 cuniv in + (match (z1,z2) with + | (Zlapp a1,Zlapp a2) -> + Array.fold_right2 f a1 a2 cu1 + | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> + if not (Projection.Repr.equal c1 c2) then + raise NotConvertible + else cu1 + | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> + let cu2 = f fx1 fx2 cu1 in + cmp_rec a1 a2 cu2 + | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> + if not (eq_ind ci1.ci_ind ci2.ci_ind) then + raise NotConvertible; + let cu2 = f (l1,p1) (l2,p2) cu1 in + Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 + | _ -> assert false) + | _ -> cuniv in + if compare_stack_shape stk1 stk2 then + cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv + else raise NotConvertible and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in -- cgit v1.2.3 From 9ead21a38feae29fdde11344de326de86bfe8ad9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 23 Oct 2018 14:06:37 +0200 Subject: Do not box fconstr closures in pattern-match branches. They are only used once, thus it is completely useless to reallocate arrays that are going to be destructed immediately. --- kernel/reduction.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 09d65e1640..7c8b1193ab 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -68,7 +68,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 * fconstr * fconstr array + | Zlcase of case_info * lift * constr * constr array * fconstr subs and lft_constr_stack = lft_constr_stack_elt list let rec zlapp v = function @@ -102,7 +102,7 @@ let pure_stack lfts stk = 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,mk_clos e p,Array.map (mk_clos e) br)::pstk)) + (l,Zlcase(ci,l,p,br,e)::pstk)) in snd (pure_rec lfts stk) @@ -600,11 +600,11 @@ 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),Zlcase(ci2,l2,p2,br2)) -> + | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible; - let cu2 = f (l1,p1) (l2,p2) cu1 in - Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 + 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 | _ -> assert false) | _ -> cuniv in if compare_stack_shape stk1 stk2 then @@ -624,6 +624,10 @@ 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 = + let fold c1 c2 cuniv = ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv in + Array.fold_right2 fold br1 br2 cuniv + let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in -- cgit v1.2.3 From d5e762723bca7cb9297183e4332e0a9c7c0932f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 25 Oct 2018 13:31:53 +0200 Subject: Do not compare the type arguments in pattern-match branches. We know that the two are living in a common type, so that it is useless to perform the comparison check. Note that we only use this fast-path when the branches are only made of lambda-abstractions, but this covers all actual cases. --- kernel/reduction.ml | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7c8b1193ab..5515ff9767 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -288,6 +288,14 @@ let conv_table_key infos k1 k2 cuniv = | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible +exception IrregularPatternShape + +let rec skip_pattern n c = + if Int.equal n 0 then c + else match kind c with + | Lambda (_, _, c) -> skip_pattern (pred n) c + | _ -> raise IrregularPatternShape + type conv_tab = { cnv_inf : clos_infos; lft_tab : clos_tab; @@ -624,9 +632,21 @@ 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 = - let fold c1 c2 cuniv = ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv in - Array.fold_right2 fold br1 br2 cuniv +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 n c1, skip_pattern n c2 with + | (c1, c2) -> + let lft1 = el_liftn n lft1 in + let lft2 = el_liftn n lft2 in + 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 + in + Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in -- cgit v1.2.3