From b35bceb2848c94c3a38e85ba5cb66560ff204164 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 6 Mar 2019 16:44:52 -0500 Subject: Update .out files --- src/fancy_with_casts_rewrite_head.out | 3350 ++++++++++++++++----------------- 1 file changed, 1673 insertions(+), 1677 deletions(-) (limited to 'src/fancy_with_casts_rewrite_head.out') diff --git a/src/fancy_with_casts_rewrite_head.out b/src/fancy_with_casts_rewrite_head.out index 226df3d11..bef104fd0 100644 --- a/src/fancy_with_casts_rewrite_head.out +++ b/src/fancy_with_casts_rewrite_head.out @@ -214,43 +214,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - ((let (x8, _) := xv0 in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv0 in x8) / - 2) - 1) && - (ZRange.normalize args1 &' - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv0 in x8)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) - then - x8 <- invert_low + fv <- (if + negb + (option_beq Z.eqb + (invert_low + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)) + (let (x8, _) := xv in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + ((let (x8, _) := xv0 in x8) =? + 2 + ^ (2 * + Z.log2_up (let (x8, _) := xv0 in x8) / + 2) - 1) && + (ZRange.normalize args1 &' + ZRange.normalize + (ZRange.constant + (let (x8, _) := xv0 in x8)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)))%expr @ + ((##match + invert_low (2 * Z.log2_up (let (x8, _) := xv0 in x8)) - (let (x8, _) := xv in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x9, _) := xv0 in - x9)))%expr @ - ((##x8)%expr, - #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv in x8) + with + | Datatypes.Some x8 => x8 + | Datatypes.None => 0 + end)%expr, + #(Z_cast args1)%expr @ + v (Compile.reflect x6))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -283,43 +293,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); v <- type.try_make_transport_cps s6 ℤ; - fv <- (x8 <- (if - ((let (x8, _) := xv0 in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv0 in x8) / - 2) - 1) && - (ZRange.normalize - (ZRange.constant - (let (x8, _) := xv0 in x8)) &' - ZRange.normalize args0 <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args1) - then - x8 <- invert_low + fv <- (if + negb + (option_beq Z.eqb + (invert_low + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)) + (let (x8, _) := xv in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args1) && + ((let (x8, _) := xv0 in x8) =? + 2 + ^ (2 * + Z.log2_up (let (x8, _) := xv0 in x8) / + 2) - 1) && + (ZRange.normalize + (ZRange.constant + (let (x8, _) := xv0 in x8)) &' + ZRange.normalize args0 <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)))%expr @ + ((##match + invert_low (2 * Z.log2_up (let (x8, _) := xv0 in x8)) - (let (x8, _) := xv in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x9, _) := xv0 in - x9)))%expr @ - ((##x8)%expr, - #(Z_cast args0)%expr @ - v (Compile.reflect x7))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv in x8) + with + | Datatypes.Some x8 => x8 + | Datatypes.None => 0 + end)%expr, + #(Z_cast args0)%expr @ + v (Compile.reflect x7))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -348,43 +368,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); v <- type.try_make_transport_cps s6 ℤ; - fv <- (x8 <- (if - ((let (x8, _) := xv0 in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv0 in x8) / - 2) - 1) && - (ZRange.normalize - (ZRange.constant - (let (x8, _) := xv0 in x8)) &' - ZRange.normalize args0 <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args1) - then - x8 <- invert_high + fv <- (if + negb + (option_beq Z.eqb + (invert_high + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)) + (let (x8, _) := xv in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args1) && + ((let (x8, _) := xv0 in x8) =? + 2 + ^ (2 * + Z.log2_up (let (x8, _) := xv0 in x8) / + 2) - 1) && + (ZRange.normalize + (ZRange.constant + (let (x8, _) := xv0 in x8)) &' + ZRange.normalize args0 <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhl + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)))%expr @ + ((##match + invert_high (2 * Z.log2_up (let (x8, _) := xv0 in x8)) - (let (x8, _) := xv in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhl - (2 * - Z.log2_up - (let (x9, _) := xv0 in - x9)))%expr @ - ((##x8)%expr, - #(Z_cast args0)%expr @ - v (Compile.reflect x7))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv in x8) + with + | Datatypes.Some x8 => x8 + | Datatypes.None => 0 + end)%expr, + #(Z_cast args0)%expr @ + v (Compile.reflect x7))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -417,43 +447,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - ((let (x8, _) := xv0 in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv0 in x8) / - 2) - 1) && - (ZRange.normalize args1 &' - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv0 in x8)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) - then - x8 <- invert_high + fv <- (if + negb + (option_beq Z.eqb + (invert_high + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)) + (let (x8, _) := xv in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + ((let (x8, _) := xv0 in x8) =? + 2 + ^ (2 * + Z.log2_up (let (x8, _) := xv0 in x8) / + 2) - 1) && + (ZRange.normalize args1 &' + ZRange.normalize + (ZRange.constant + (let (x8, _) := xv0 in x8)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhl + (2 * + Z.log2_up + (let (x8, _) := xv0 in x8)))%expr @ + ((##match + invert_high (2 * Z.log2_up (let (x8, _) := xv0 in x8)) - (let (x8, _) := xv in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhl - (2 * - Z.log2_up - (let (x9, _) := xv0 in - x9)))%expr @ - ((##x8)%expr, - #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv in x8) + with + | Datatypes.Some x8 => x8 + | Datatypes.None => 0 + end)%expr, + #(Z_cast args1)%expr @ + v (Compile.reflect x6))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -500,33 +540,40 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - (ZRange.normalize args1 >> - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv0 in x8)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) - then - x8 <- invert_low + fv <- (if + negb + (option_beq Z.eqb + (invert_low + (2 * (let (x8, _) := xv0 in x8)) + (let (x8, _) := xv in x8)) + Datatypes.None) && + is_bounded_by_bool (let (x8, _) := xv in x8) + (ZRange.normalize args5) && + is_bounded_by_bool (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x8, _) := xv0 in x8)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mullh + (2 * (let (x8, _) := xv0 in x8)))%expr @ + ((##match + invert_low (2 * (let (x8, _) := xv0 in x8)) - (let (x8, _) := xv in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mullh - (2 * - (let (x9, _) := xv0 in x9)))%expr @ - ((##x8)%expr, - #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv in x8) + with + | Datatypes.Some x8 => x8 + | Datatypes.None => 0 + end)%expr, + #(Z_cast args1)%expr @ + v (Compile.reflect x6))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -555,31 +602,38 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - (ZRange.normalize args1 >> - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv0 in x8)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) - then - x8 <- invert_high + fv <- (if + negb + (option_beq Z.eqb + (invert_high + (2 * (let (x8, _) := xv0 in x8)) + (let (x8, _) := xv in x8)) + Datatypes.None) && + is_bounded_by_bool (let (x8, _) := xv in x8) + (ZRange.normalize args5) && + is_bounded_by_bool (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant (let (x8, _) := xv0 in x8)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhh + (2 * (let (x8, _) := xv0 in x8)))%expr @ + ((##match + invert_high (2 * (let (x8, _) := xv0 in x8)) - (let (x8, _) := xv in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhh - (2 * (let (x9, _) := xv0 in x9)))%expr @ - ((##x8)%expr, - #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv in x8) + with + | Datatypes.Some x8 => x8 + | Datatypes.None => 0 + end)%expr, + #(Z_cast args1)%expr @ + v (Compile.reflect x6))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -708,45 +762,55 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - ((let (x8, _) := xv in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv in x8) / - 2) - 1) && - (ZRange.normalize - (ZRange.constant - (let (x8, _) := xv in x8)) &' - ZRange.normalize args1 <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args3) - then - y <- invert_low + fv <- (if + negb + (option_beq Z.eqb + (invert_low + (2 * + Z.log2_up + (let (x8, _) := xv in x8)) + (let (x8, _) := xv0 in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args3) && + ((let (x8, _) := xv in x8) =? + 2 + ^ (2 * + Z.log2_up + (let (x8, _) := xv in x8) / 2) - + 1) && + (ZRange.normalize + (ZRange.constant + (let (x8, _) := xv in x8)) &' + ZRange.normalize args1 <=? + ZRange.normalize args5)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * + Z.log2_up + (let (x8, _) := xv in x8)))%expr @ + (#(Z_cast args1)%expr @ + v (Compile.reflect x6), + (##match + invert_low (2 * Z.log2_up (let (x8, _) := xv in x8)) (let (x8, _) := xv0 in - x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x8, _) := - xv in - x8)))%expr @ - (#(Z_cast args1)%expr @ - v (Compile.reflect x6), - (##y)%expr)))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + x8) + with + | Datatypes.Some y => y + | Datatypes.None => 0 + end)%expr)))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -799,45 +863,55 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - ((let (x8, _) := xv in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv in x8) / - 2) - 1) && - (ZRange.normalize args3 &' - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv in x8)) <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args2) - then - y <- invert_low + fv <- (if + negb + (option_beq Z.eqb + (invert_low + (2 * + Z.log2_up + (let (x8, _) := xv in x8)) + (let (x8, _) := xv0 in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args2) && + ((let (x8, _) := xv in x8) =? + 2 + ^ (2 * + Z.log2_up + (let (x8, _) := xv in x8) / 2) - + 1) && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x8, _) := xv in x8)) <=? + ZRange.normalize args5)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * + Z.log2_up + (let (x8, _) := xv in x8)))%expr @ + (#(Z_cast args3)%expr @ + v (Compile.reflect x5), + (##match + invert_low (2 * Z.log2_up (let (x8, _) := xv in x8)) (let (x8, _) := xv0 in - x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x8, _) := - xv in - x8)))%expr @ - (#(Z_cast args3)%expr @ - v (Compile.reflect x5), - (##y)%expr)))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + x8) + with + | Datatypes.Some y => y + | Datatypes.None => 0 + end)%expr)))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -882,45 +956,55 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - ((let (x8, _) := xv in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv in x8) / - 2) - 1) && - (ZRange.normalize - (ZRange.constant - (let (x8, _) := xv in x8)) &' - ZRange.normalize args2 <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args3) - then - y <- invert_high + fv <- (if + negb + (option_beq Z.eqb + (invert_high + (2 * + Z.log2_up + (let (x8, _) := xv in x8)) + (let (x8, _) := xv0 in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args3) && + ((let (x8, _) := xv in x8) =? + 2 + ^ (2 * + Z.log2_up + (let (x8, _) := xv in x8) / 2) - + 1) && + (ZRange.normalize + (ZRange.constant + (let (x8, _) := xv in x8)) &' + ZRange.normalize args2 <=? + ZRange.normalize args5)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mullh + (2 * + Z.log2_up + (let (x8, _) := xv in x8)))%expr @ + (#(Z_cast args2)%expr @ + v (Compile.reflect x6), + (##match + invert_high (2 * Z.log2_up (let (x8, _) := xv in x8)) (let (x8, _) := xv0 in - x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mullh - (2 * - Z.log2_up - (let (x8, _) := - xv in - x8)))%expr @ - (#(Z_cast args2)%expr @ - v (Compile.reflect x6), - (##y)%expr)))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + x8) + with + | Datatypes.Some y => y + | Datatypes.None => 0 + end)%expr)))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -965,45 +1049,55 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - ((let (x8, _) := xv in x8) =? - 2 - ^ (2 * - Z.log2_up - (let (x8, _) := xv in x8) / - 2) - 1) && - (ZRange.normalize args3 &' - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv in x8)) <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args2) - then - y <- invert_high + fv <- (if + negb + (option_beq Z.eqb + (invert_high + (2 * + Z.log2_up + (let (x8, _) := xv in x8)) + (let (x8, _) := xv0 in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args2) && + ((let (x8, _) := xv in x8) =? + 2 + ^ (2 * + Z.log2_up + (let (x8, _) := xv in x8) / 2) - + 1) && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x8, _) := xv in x8)) <=? + ZRange.normalize args5)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mullh + (2 * + Z.log2_up + (let (x8, _) := xv in x8)))%expr @ + (#(Z_cast args3)%expr @ + v (Compile.reflect x5), + (##match + invert_high (2 * Z.log2_up (let (x8, _) := xv in x8)) (let (x8, _) := xv0 in - x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mullh - (2 * - Z.log2_up - (let (x8, _) := - xv in - x8)))%expr @ - (#(Z_cast args3)%expr @ - v (Compile.reflect x5), - (##y)%expr)))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + x8) + with + | Datatypes.Some y => y + | Datatypes.None => 0 + end)%expr)))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1057,52 +1151,49 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); v0 <- type.try_make_transport_cps s10 ℤ; - fv <- (x12 <- (if - ((let (x12, _) := xv in x12) =? - 2 - ^ (2 * - Z.log2_up - (let (x12, _) := xv in - x12) / 2) - 1) && - ((let (x12, _) := xv0 in x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args6) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args1) && + ((let (x12, _) := xv in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + ((let (x12, _) := xv0 in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + (ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) &' + ZRange.normalize args5 <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) &' + ZRange.normalize args <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * Z.log2_up (let (x12, _) := xv in - x12) / 2) - 1) && - (ZRange.normalize - (ZRange.constant - (let (x12, _) := xv in - x12)) &' - ZRange.normalize args5 <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize - (ZRange.constant - (let (x12, _) := xv0 in - x12)) &' - ZRange.normalize args <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv in x12) - (ZRange.normalize args6) && - is_bounded_by_bool - (let (x12, _) := xv0 in x12) - (ZRange.normalize args1) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x12, _) := - xv in - x12)))%expr @ - (#(Z_cast args5)%expr @ - v (Compile.reflect x6), - #(Z_cast args)%expr @ - v0 (Compile.reflect x11))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args5)%expr @ + v (Compile.reflect x6), + #(Z_cast args)%expr @ + v0 (Compile.reflect x11))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1238,52 +1329,49 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); v0 <- type.try_make_transport_cps s10 ℤ; - fv <- (x12 <- (if - ((let (x12, _) := xv in x12) =? - 2 - ^ (2 * - Z.log2_up - (let (x12, _) := xv in - x12) / 2) - 1) && - ((let (x12, _) := xv0 in x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args1) && + ((let (x12, _) := xv in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + ((let (x12, _) := xv0 in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + (ZRange.normalize args6 &' + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) &' + ZRange.normalize args <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * Z.log2_up (let (x12, _) := xv in - x12) / 2) - 1) && - (ZRange.normalize args6 &' - ZRange.normalize - (ZRange.constant - (let (x12, _) := xv in - x12)) <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize - (ZRange.constant - (let (x12, _) := xv0 in - x12)) &' - ZRange.normalize args <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv in x12) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x12, _) := xv0 in x12) - (ZRange.normalize args1) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x12, _) := - xv in - x12)))%expr @ - (#(Z_cast args6)%expr @ - v (Compile.reflect x5), - #(Z_cast args)%expr @ - v0 (Compile.reflect x11))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args6)%expr @ + v (Compile.reflect x5), + #(Z_cast args)%expr @ + v0 (Compile.reflect x11))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1418,52 +1506,49 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (if - ((let (x12, _) := xv in x12) =? - 2 - ^ (2 * - Z.log2_up - (let (x12, _) := xv in - x12) / 2) - 1) && - ((let (x12, _) := xv0 in x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args6) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + ((let (x12, _) := xv0 in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + (ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) &' + ZRange.normalize args5 <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args1 &' + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * Z.log2_up (let (x12, _) := xv in - x12) / 2) - 1) && - (ZRange.normalize - (ZRange.constant - (let (x12, _) := xv in - x12)) &' - ZRange.normalize args5 <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize args1 &' - ZRange.normalize - (ZRange.constant - (let (x12, _) := xv0 in - x12)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv in x12) - (ZRange.normalize args6) && - is_bounded_by_bool - (let (x12, _) := xv0 in x12) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x12, _) := - xv in - x12)))%expr @ - (#(Z_cast args5)%expr @ - v (Compile.reflect x6), - #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args5)%expr @ + v (Compile.reflect x6), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1596,52 +1681,49 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (if - ((let (x12, _) := xv in x12) =? - 2 - ^ (2 * - Z.log2_up - (let (x12, _) := xv in - x12) / 2) - 1) && - ((let (x12, _) := xv0 in x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + ((let (x12, _) := xv0 in x12) =? + 2 + ^ (2 * + Z.log2_up + (let (x12, _) := xv in x12) / 2) - + 1) && + (ZRange.normalize args6 &' + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args1 &' + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulll + (2 * Z.log2_up (let (x12, _) := xv in - x12) / 2) - 1) && - (ZRange.normalize args6 &' - ZRange.normalize - (ZRange.constant - (let (x12, _) := xv in - x12)) <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize args1 &' - ZRange.normalize - (ZRange.constant - (let (x12, _) := xv0 in - x12)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv in x12) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x12, _) := xv0 in x12) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulll - (2 * - Z.log2_up - (let (x12, _) := - xv in - x12)))%expr @ - (#(Z_cast args6)%expr @ - v (Compile.reflect x5), - #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args6)%expr @ + v (Compile.reflect x5), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1774,44 +1856,40 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (if - ((let (x12, _) := xv in x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args6) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in x12) =? + 2 + ^ (2 * (let (x12, _) := xv0 in x12) / + 2) - 1) && + (ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) &' + ZRange.normalize args5 <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mullh + (2 * (let (x12, _) := xv0 in - x12) / 2) - 1) && - (ZRange.normalize - (ZRange.constant - (let (x12, _) := xv in - x12)) &' - ZRange.normalize args5 <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize args1 >> - ZRange.normalize - (ZRange.constant - (let (x12, _) := xv0 in - x12)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv in x12) - (ZRange.normalize args6) && - is_bounded_by_bool - (let (x12, _) := xv0 in x12) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mullh - (2 * - (let (x12, _) := - xv0 in - x12)))%expr @ - (#(Z_cast args5)%expr @ - v (Compile.reflect x6), - #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args5)%expr @ + v (Compile.reflect x6), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1944,44 +2022,40 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (if - ((let (x12, _) := xv in x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in x12) =? + 2 + ^ (2 * (let (x12, _) := xv0 in x12) / + 2) - 1) && + (ZRange.normalize args6 &' + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mullh + (2 * (let (x12, _) := xv0 in - x12) / 2) - 1) && - (ZRange.normalize args6 &' - ZRange.normalize - (ZRange.constant - (let (x12, _) := xv in - x12)) <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize args1 >> - ZRange.normalize - (ZRange.constant - (let (x12, _) := xv0 in - x12)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv in x12) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x12, _) := xv0 in x12) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mullh - (2 * - (let (x12, _) := - xv0 in - x12)))%expr @ - (#(Z_cast args6)%expr @ - v (Compile.reflect x5), - #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args6)%expr @ + v (Compile.reflect x5), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2118,33 +2192,42 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - (ZRange.normalize args3 >> - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv in x8)) <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args2) - then - y <- invert_low + fv <- (if + negb + (option_beq Z.eqb + (invert_low + (2 * (let (x8, _) := xv in x8)) + (let (x8, _) := xv0 in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args2) && + (ZRange.normalize args3 >> + ZRange.normalize + (ZRange.constant + (let (x8, _) := xv in x8)) <=? + ZRange.normalize args5)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhl + (2 * (let (x8, _) := xv in x8)))%expr @ + (#(Z_cast args3)%expr @ + v (Compile.reflect x5), + (##match + invert_low (2 * (let (x8, _) := xv in x8)) - (let (x8, _) := xv0 in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhl - (2 * - (let (x8, _) := xv in x8)))%expr @ - (#(Z_cast args3)%expr @ - v (Compile.reflect x5), - (##y)%expr)))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv0 in x8) + with + | Datatypes.Some y => y + | Datatypes.None => 0 + end)%expr)))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -2173,33 +2256,42 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - (ZRange.normalize args3 >> - ZRange.normalize - (ZRange.constant - (let (x8, _) := xv in x8)) <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args2) - then - y <- invert_high + fv <- (if + negb + (option_beq Z.eqb + (invert_high + (2 * (let (x8, _) := xv in x8)) + (let (x8, _) := xv0 in x8)) + Datatypes.None) && + is_bounded_by_bool + (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args2) && + (ZRange.normalize args3 >> + ZRange.normalize + (ZRange.constant + (let (x8, _) := xv in x8)) <=? + ZRange.normalize args5)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhh + (2 * (let (x8, _) := xv in x8)))%expr @ + (#(Z_cast args3)%expr @ + v (Compile.reflect x5), + (##match + invert_high (2 * (let (x8, _) := xv in x8)) - (let (x8, _) := xv0 in x8); - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhh - (2 * - (let (x8, _) := xv in x8)))%expr @ - (#(Z_cast args3)%expr @ - v (Compile.reflect x5), - (##y)%expr)))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + (let (x8, _) := xv0 in x8) + with + | Datatypes.Some y => y + | Datatypes.None => 0 + end)%expr)))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -2257,64 +2349,45 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.ident.Literal ##(projT2 args0); v0 <- type.try_make_transport_cps s10 ℤ; - fv <- (x12 <- (if - ((let (x12, _) := - xv0 in - x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args1) && + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args5) && + ((let (x12, _) := xv0 in x12) =? + 2 + ^ (2 * + (let (x12, _) := xv in x12) / + 2) - 1) && + (ZRange.normalize args6 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in + x12)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in + x12)) &' + ZRange.normalize args <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhl + (2 * (let (x12, _) := xv in - x12) / 2) - 1) && - (ZRange.normalize - args6 >> - ZRange.normalize - (ZRange.constant - (let (x12, _) := - xv in - x12)) <=? - ZRange.normalize - args8)%zrange && - (ZRange.normalize - (ZRange.constant - (let (x12, _) := - xv0 in - x12)) &' - ZRange.normalize args <=? - ZRange.normalize - args3)%zrange && - is_bounded_by_bool - (let (x12, _) := - xv0 in - x12) - (ZRange.normalize - args1) && - is_bounded_by_bool - (let (x12, _) := - xv in - x12) - (ZRange.normalize - args5) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhl - (2 * - (let - (x12, - _) := - xv in - x12)))%expr @ - (#(Z_cast args6)%expr @ - v - (Compile.reflect - x5), - #(Z_cast args)%expr @ - v0 - (Compile.reflect - x11))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args6)%expr @ + v (Compile.reflect x5), + #(Z_cast args)%expr @ + v0 + (Compile.reflect x11))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2365,51 +2438,41 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (if - ((let (x12, _) := xv0 in - x12) =? - 2 - ^ (2 * + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args5) && + ((let (x12, _) := xv0 in x12) =? + 2 + ^ (2 * + (let (x12, _) := xv in x12) / + 2) - 1) && + (ZRange.normalize args6 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args1 &' + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhl + (2 * (let (x12, _) := xv in - x12) / 2) - 1) && - (ZRange.normalize args6 >> - ZRange.normalize - (ZRange.constant - (let (x12, _) := - xv in - x12)) <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize args1 &' - ZRange.normalize - (ZRange.constant - (let (x12, _) := - xv0 in - x12)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv0 in - x12) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x12, _) := xv in - x12) - (ZRange.normalize args5) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhl - (2 * - (let (x12, _) := - xv in - x12)))%expr @ - (#(Z_cast args6)%expr @ - v - (Compile.reflect x5), - #(Z_cast args1)%expr @ - v0 - (Compile.reflect x10))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + x12)))%expr @ + (#(Z_cast args6)%expr @ + v (Compile.reflect x5), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2467,49 +2530,38 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (if - ((let (x12, _) := xv in - x12) =? - (let (x12, _) := xv0 in - x12)) && - (ZRange.normalize args6 >> - ZRange.normalize - (ZRange.constant - (let (x12, _) := - xv in - x12)) <=? - ZRange.normalize args8)%zrange && - (ZRange.normalize args1 >> - ZRange.normalize - (ZRange.constant - (let (x12, _) := - xv0 in - x12)) <=? - ZRange.normalize args3)%zrange && - is_bounded_by_bool - (let (x12, _) := xv in - x12) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x12, _) := xv0 in - x12) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_mulhh - (2 * - (let (x12, _) := - xv in - x12)))%expr @ - (#(Z_cast args6)%expr @ - v - (Compile.reflect x5), - #(Z_cast args1)%expr @ - v0 - (Compile.reflect x10))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x12)); + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args5) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in x12) =? + (let (x12, _) := xv0 in x12)) && + (ZRange.normalize args6 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv in x12)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args3)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_mulhh + (2 * + (let (x12, _) := xv in + x12)))%expr @ + (#(Z_cast args6)%expr @ + v (Compile.reflect x5), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2645,50 +2697,41 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with if type.type_beq base.type base.type.type_beq (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args2) -> s6) -> s7) -> s8)%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args2); - v <- type.try_make_transport_cps s6 ℤ; - v0 <- type.try_make_transport_cps s7 ℤ; - v1 <- type.try_make_transport_cps s8 ℤ; - fv <- (x10 <- (if - ((let (x10, _) := xv in - x10) =? - 2 - ^ Z.log2 - (let (x10, _) := - xv in - x10)) && - ((ZRange.cc_m - (let (x10, _) := xv in - x10)) - (ZRange.normalize args1) <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x10, _) := xv in - x10) - (ZRange.normalize args3) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_selm - (Z.log2 - (let - (x10, _) := - xv in - x10)))%expr @ - (#(Z_cast args1)%expr @ - v - (Compile.reflect x7), - #(Z_cast args0)%expr @ - v0 - (Compile.reflect x8), - #(Z_cast args)%expr @ - v1 - (Compile.reflect x9))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x10)); + ((((projT1 args2) -> s6) -> s7) -> s8)%ptype + then + xv <- ident.unify pattern.ident.Literal + ##(projT2 args2); + v <- type.try_make_transport_cps s6 ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; + v1 <- type.try_make_transport_cps s8 ℤ; + fv <- (if + is_bounded_by_bool + (let (x10, _) := xv in x10) + (ZRange.normalize args3) && + ((let (x10, _) := xv in x10) =? + 2 + ^ Z.log2 + (let (x10, _) := xv in x10)) && + ((ZRange.cc_m + (let (x10, _) := xv in x10)) + (ZRange.normalize args1) <=? + ZRange.normalize args5)%zrange + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_selm + (Z.log2 + (let (x10, _) := + xv in + x10)))%expr @ + (#(Z_cast args1)%expr @ + v (Compile.reflect x7), + #(Z_cast args0)%expr @ + v0 (Compile.reflect x8), + #(Z_cast args)%expr @ + v1 (Compile.reflect x9))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2767,43 +2810,27 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s6 ℤ; v0 <- type.try_make_transport_cps s7 ℤ; v1 <- type.try_make_transport_cps s8 ℤ; - fv <- (x10 <- (if - ((let (x10, _) := - xv in - x10) =? 1) && - (ZRange.normalize - (ZRange.constant - (let (x10, _) := - xv in - x10)) &' - ZRange.normalize - args1 <=? - ZRange.normalize - args5)%zrange && - is_bounded_by_bool - (let (x10, _) := - xv in - x10) - (ZRange.normalize - args3) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_sell)%expr @ - (#(Z_cast args1)%expr @ - v - (Compile.reflect - x7), - #(Z_cast args0)%expr @ - v0 - (Compile.reflect - x8), - #(Z_cast args)%expr @ - v1 - (Compile.reflect - x9))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x10)); + fv <- (if + is_bounded_by_bool 1 + (ZRange.normalize args3) && + (ZRange.normalize + (ZRange.constant 1) &' + ZRange.normalize args1 <=? + ZRange.normalize args5)%zrange && + ((let (x10, _) := xv in x10) =? + 1) + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_sell)%expr @ + (#(Z_cast args1)%expr @ + v (Compile.reflect x7), + #(Z_cast args0)%expr @ + v0 (Compile.reflect x8), + #(Z_cast args)%expr @ + v1 (Compile.reflect x9))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2865,35 +2892,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); v0 <- type.try_make_transport_cps s7 ℤ; v1 <- type.try_make_transport_cps s8 ℤ; - fv <- (x10 <- (if - ((let (x10, _) := xv in - x10) =? 1) && - (ZRange.normalize args3 &' - ZRange.normalize - (ZRange.constant - (let (x10, _) := - xv in - x10)) <=? - ZRange.normalize args5)%zrange && - is_bounded_by_bool - (let (x10, _) := xv in - x10) - (ZRange.normalize args2) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_sell)%expr @ - (#(Z_cast args3)%expr @ - v - (Compile.reflect x6), - #(Z_cast args0)%expr @ - v0 - (Compile.reflect x8), - #(Z_cast args)%expr @ - v1 - (Compile.reflect x9))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x10)); + fv <- (if + is_bounded_by_bool 1 + (ZRange.normalize args2) && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant 1) <=? + ZRange.normalize args5)%zrange && + ((let (x10, _) := xv in x10) =? 1) + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_sell)%expr @ + (#(Z_cast args3)%expr @ + v (Compile.reflect x6), + #(Z_cast args0)%expr @ + v0 (Compile.reflect x8), + #(Z_cast args)%expr @ + v1 (Compile.reflect x9))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2991,25 +3009,22 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s4 ℤ; v0 <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (if - ((let (x8, _) := xv in x8) =? - 2 ^ Z.log2 (let (x8, _) := xv in x8)) && - is_bounded_by_bool (let (x8, _) := xv in x8) - (ZRange.normalize args4) && - is_bounded_by_bool (let (x8, _) := xv0 in x8) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast range)%expr @ - (#(fancy_rshi - (Z.log2 (let (x8, _) := xv in x8)) - (let (x8, _) := xv0 in x8))%expr @ - (#(Z_cast args2)%expr @ - v (Compile.reflect x5), - #(Z_cast args1)%expr @ - v0 (Compile.reflect x6))))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x8)); + fv <- (if + is_bounded_by_bool (let (x8, _) := xv in x8) + (ZRange.normalize args4) && + is_bounded_by_bool (let (x8, _) := xv0 in x8) + (ZRange.normalize args0) && + ((let (x8, _) := xv in x8) =? + 2 ^ Z.log2 (let (x8, _) := xv in x8)) + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ + (#(fancy_rshi (Z.log2 (let (x8, _) := xv in x8)) + (let (x8, _) := xv0 in x8))%expr @ + (#(Z_cast args2)%expr @ v (Compile.reflect x5), + #(Z_cast args1)%expr @ v0 (Compile.reflect x6))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -3285,13 +3300,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Datatypes.Some _ => if type.type_beq base.type base.type.type_beq ℤ ℤ then - fv <- (x0 <- (if - (range <=? value_range)%zrange - || (range <=? flag_range)%zrange - then - Datatypes.Some (#(Z_cast range)%expr @ x)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x0)); + fv <- (if + (range <=? value_range)%zrange + || (range <=? flag_range)%zrange + then + Datatypes.Some (Base (#(Z_cast range)%expr @ x)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -3317,6 +3331,96 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with idc9))) @ (@expr.Ident _ _ _ t10 idc10 @ @expr.Ident _ _ _ t11 idc11))%expr_pat => + (args <- invert_bind_args idc11 Raw.ident.Literal; + args0 <- invert_bind_args idc10 Raw.ident.Z_cast; + args1 <- invert_bind_args idc9 Raw.ident.Literal; + args2 <- invert_bind_args idc8 Raw.ident.Z_cast; + args3 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args5 <- invert_bind_args idc5 Raw.ident.Z_cast; + _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; + args7 <- invert_bind_args idc3 Raw.ident.Z_cast; + args8 <- invert_bind_args idc2 Raw.ident.Z_cast; + args9 <- invert_bind_args idc1 Raw.ident.Literal; + args10 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc + Raw.ident.Z_add_get_carry; + match + pattern.type.unify_extracted + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args9) -> s3) -> + (s10 -> (projT1 args1)) -> (projT1 args))%ptype + with + | Datatypes.Some (_, _, (_, _, _))%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args9) -> s3) -> + (s10 -> (projT1 args1)) -> (projT1 args))%ptype + then + xv <- ident.unify pattern.ident.Literal + ##(projT2 args9); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s10 ℤ; + xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args1); + xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args); + fv <- (if + ((let (x14, _) := xv in x14) =? + 2 + ^ Z.log2 (let (x14, _) := xv in x14)) && + is_bounded_by_bool + (let (x14, _) := xv in x14) + (ZRange.normalize args10) && + is_bounded_by_bool + (let (x14, _) := xv1 in x14) + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x14, _) := xv0 in x14) + (ZRange.normalize args2) && + (ZRange.normalize args5 << + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv1 in x14)) <=? + ZRange.normalize args7)%zrange && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv0 in x14)) <=? + ZRange.normalize args5)%zrange && + (ZRange.normalize args7 <=? + r[0 ~> (let (x14, _) := xv in x14) - + 1])%zrange && + ((let (x14, _) := xv0 in x14) =? + Z.ones + (Z.log2 + (let (x14, _) := xv in x14) - + (let (x14, _) := xv1 in x14))) && + ((0 <=? (let (x14, _) := xv1 in x14)) && + ((let (x14, _) := xv1 in x14) <=? + Z.log2 (let (x14, _) := xv in x14))) + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_add + (Z.log2 + (let (x14, _) := xv in + x14)) + (let (x14, _) := xv1 in + x14))%expr @ + (#(Z_cast args8)%expr @ + v (Compile.reflect x4), + #(Z_cast args3)%expr @ + v0 (Compile.reflect x11))))%expr_pat) + else Datatypes.None); + Datatypes.Some + (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end);; args <- invert_bind_args idc11 Raw.ident.Literal; args0 <- invert_bind_args idc10 Raw.ident.Z_cast; args1 <- invert_bind_args idc9 Raw.ident.Literal; @@ -3351,54 +3455,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x14 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s13 : Z) - (rx : zrange) (x14 : expr ℤ) - (rshiftl rland ry : zrange) - (y : expr ℤ) - (rmask : zrange) (mask : Z) - (roffset : zrange) - (offset : Z) => - if - (s13 =? 2 ^ Z.log2 s13) && - (ZRange.normalize rland << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize ry &' - ZRange.normalize - (ZRange.constant mask) <=? - ZRange.normalize rland)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s13 - 1])%zrange && - (mask =? - Z.ones (Z.log2 s13 - offset)) && - (0 <=? offset) && - (offset <=? Z.log2 s13) && - is_bounded_by_bool s13 - (ZRange.normalize rs) && - is_bounded_by_bool mask - (ZRange.normalize rmask) && - is_bounded_by_bool offset - (ZRange.normalize roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s13) - offset)%expr @ - (#(Z_cast rx)%expr @ x14, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args10 - (let (x14, _) := xv in x14) - args8 (v (Compile.reflect x4)) - args7 args5 args3 - (v0 (Compile.reflect x11)) - args2 - (let (x14, _) := xv0 in x14) - args0 - (let (x14, _) := xv1 in x14); - Datatypes.Some (Base x14)); + fv <- (if + ((let (x14, _) := xv in x14) =? + 2 + ^ Z.log2 (let (x14, _) := xv in x14)) && + ((let (x14, _) := xv0 in x14) =? + Z.ones + (Z.log2 (let (x14, _) := xv in x14) - + (let (x14, _) := xv1 in x14))) && + ((0 <=? (let (x14, _) := xv1 in x14)) && + ((let (x14, _) := xv1 in x14) <=? + Z.log2 (let (x14, _) := xv in x14))) && + is_bounded_by_bool + (let (x14, _) := xv in x14) + (ZRange.normalize args10) && + is_bounded_by_bool + (let (x14, _) := xv0 in x14) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x14, _) := xv1 in x14) + (ZRange.normalize args0) && + (ZRange.normalize args5 << + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv1 in x14)) <=? + ZRange.normalize args7)%zrange && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv0 in x14)) <=? + ZRange.normalize args5)%zrange && + (ZRange.normalize args7 <=? + r[0 ~> (let (x14, _) := xv in x14) - + 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_add + (Z.log2 + (let (x14, _) := xv in + x14)) + (let (x14, _) := xv1 in x14))%expr @ + (#(Z_cast args8)%expr @ + v (Compile.reflect x4), + #(Z_cast args3)%expr @ + v0 (Compile.reflect x11))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -3663,55 +3766,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); v0 <- type.try_make_transport_cps s4 ℤ; - fv <- (x14 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s13 : Z) - (rshiftl rland ry : zrange) - (y : expr ℤ) - (rmask : zrange) (mask : Z) - (roffset : zrange) - (offset : Z) (rx : zrange) - (x14 : expr ℤ) => - if - (s13 =? 2 ^ Z.log2 s13) && - (ZRange.normalize rland << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize ry &' - ZRange.normalize - (ZRange.constant mask) <=? - ZRange.normalize rland)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s13 - 1])%zrange && - (mask =? - Z.ones (Z.log2 s13 - offset)) && - (0 <=? offset) && - (offset <=? Z.log2 s13) && - is_bounded_by_bool s13 - (ZRange.normalize rs) && - is_bounded_by_bool mask - (ZRange.normalize rmask) && - is_bounded_by_bool offset - (ZRange.normalize roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s13) - offset)%expr @ - (#(Z_cast rx)%expr @ x14, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args10 - (let (x14, _) := xv in x14) - args8 args5 args3 - (v (Compile.reflect x11)) - args2 - (let (x14, _) := xv0 in x14) - args0 - (let (x14, _) := xv1 in x14) - args7 - (v0 (Compile.reflect x5)); - Datatypes.Some (Base x14)); + fv <- (if + is_bounded_by_bool + (let (x14, _) := xv in x14) + (ZRange.normalize args10) && + is_bounded_by_bool + (let (x14, _) := xv0 in x14) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x14, _) := xv1 in x14) + (ZRange.normalize args0) && + ((let (x14, _) := xv in x14) =? + 2 + ^ Z.log2 (let (x14, _) := xv in x14)) && + (ZRange.normalize args5 << + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv1 in x14)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv0 in x14)) <=? + ZRange.normalize args5)%zrange && + (ZRange.normalize args8 <=? + r[0 ~> (let (x14, _) := xv in x14) - + 1])%zrange && + ((let (x14, _) := xv0 in x14) =? + Z.ones + (Z.log2 (let (x14, _) := xv in x14) - + (let (x14, _) := xv1 in x14))) && + ((0 <=? (let (x14, _) := xv1 in x14)) && + ((let (x14, _) := xv1 in x14) <=? + Z.log2 (let (x14, _) := xv in x14))) + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_add + (Z.log2 + (let (x14, _) := xv in + x14)) + (let (x14, _) := xv1 in x14))%expr @ + (#(Z_cast args7)%expr @ + v0 (Compile.reflect x5), + #(Z_cast args3)%expr @ + v (Compile.reflect x11))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -3963,41 +4064,40 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s7 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x10 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s9 : Z) - (rx : zrange) (x10 : expr ℤ) - (rshiftr ry : zrange) - (y : expr ℤ) - (roffset : zrange) - (offset : Z) => - if - (s9 =? 2 ^ Z.log2 s9) && - (ZRange.normalize ry >> - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftr)%zrange && - (ZRange.normalize rshiftr <=? - r[0 ~> s9 - 1])%zrange && - is_bounded_by_bool s9 - (ZRange.normalize rs) && - is_bounded_by_bool offset - (ZRange.normalize roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s9) - (- offset))%expr @ - (#(Z_cast rx)%expr @ x10, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args6 - (let (x10, _) := xv in x10) - args4 (v (Compile.reflect x4)) - args3 args1 - (v0 (Compile.reflect x8)) - args0 - (let (x10, _) := xv0 in x10); - Datatypes.Some (Base x10)); + fv <- (if + is_bounded_by_bool + (let (x10, _) := xv in x10) + (ZRange.normalize args6) && + is_bounded_by_bool + (let (x10, _) := xv0 in x10) + (ZRange.normalize args0) && + ((let (x10, _) := xv in x10) =? + 2 + ^ Z.log2 (let (x10, _) := xv in x10)) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x10, _) := xv0 in x10)) <=? + ZRange.normalize args3)%zrange && + (ZRange.normalize args3 <=? + r[0 ~> (let (x10, _) := xv in x10) - + 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_add + (Z.log2 + (let (x10, _) := xv in + x10)) + (- + (let (x10, _) := xv0 in + x10)))%expr @ + (#(Z_cast args4)%expr @ + v (Compile.reflect x4), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x8))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -4086,41 +4186,40 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); v0 <- type.try_make_transport_cps s4 ℤ; - fv <- (x10 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s9 : Z) - (rshiftr ry : zrange) - (y : expr ℤ) - (roffset : zrange) - (offset : Z) (rx : zrange) - (x10 : expr ℤ) => - if - (s9 =? 2 ^ Z.log2 s9) && - (ZRange.normalize ry >> - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftr)%zrange && - (ZRange.normalize rshiftr <=? - r[0 ~> s9 - 1])%zrange && - is_bounded_by_bool s9 - (ZRange.normalize rs) && - is_bounded_by_bool offset - (ZRange.normalize roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s9) - (- offset))%expr @ - (#(Z_cast rx)%expr @ x10, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args6 - (let (x10, _) := xv in x10) - args4 args1 - (v (Compile.reflect x8)) args0 - (let (x10, _) := xv0 in x10) - args3 - (v0 (Compile.reflect x5)); - Datatypes.Some (Base x10)); + fv <- (if + is_bounded_by_bool + (let (x10, _) := xv in x10) + (ZRange.normalize args6) && + is_bounded_by_bool + (let (x10, _) := xv0 in x10) + (ZRange.normalize args0) && + ((let (x10, _) := xv in x10) =? + 2 + ^ Z.log2 (let (x10, _) := xv in x10)) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x10, _) := xv0 in x10)) <=? + ZRange.normalize args4)%zrange && + (ZRange.normalize args4 <=? + r[0 ~> (let (x10, _) := xv in x10) - + 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_add + (Z.log2 + (let (x10, _) := xv in + x10)) + (- + (let (x10, _) := xv0 in + x10)))%expr @ + (#(Z_cast args3)%expr @ + v0 (Compile.reflect x5), + #(Z_cast args1)%expr @ + v (Compile.reflect x8))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -4196,28 +4295,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); v <- type.try_make_transport_cps s3 ℤ; v0 <- type.try_make_transport_cps s4 ℤ; - fv <- (x6 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s5 : Z) - (rx : zrange) (x6 : expr ℤ) - (ry : zrange) (y : expr ℤ) => - if - (s5 =? 2 ^ Z.log2 s5) && - (ZRange.normalize ry <=? - r[0 ~> s5 - 1])%zrange && - is_bounded_by_bool s5 - (ZRange.normalize rs) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s5) 0)%expr @ - (#(Z_cast rx)%expr @ x6, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args2 - (let (x6, _) := xv in x6) args0 - (v (Compile.reflect x4)) args - (v0 (Compile.reflect x5)); - Datatypes.Some (Base x6)); + fv <- (if + is_bounded_by_bool + (let (x6, _) := xv in x6) + (ZRange.normalize args2) && + ((let (x6, _) := xv in x6) =? + 2 ^ Z.log2 (let (x6, _) := xv in x6)) && + (ZRange.normalize args <=? + r[0 ~> (let (x6, _) := xv in x6) - 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_add + (Z.log2 + (let (x6, _) := xv in x6)) 0)%expr @ + (#(Z_cast args0)%expr @ + v (Compile.reflect x4), + #(Z_cast args)%expr @ + v0 (Compile.reflect x5))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -4312,85 +4409,66 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x14 <- (let - '(r1, r2)%zrange := - range in - fun (rs : zrange) - (s13 : Z) - (rx : zrange) - (x14 : expr ℤ) - (rshiftl rland - ry : zrange) - (y : expr ℤ) - (rmask : zrange) - (mask : Z) - (roffset : zrange) - (offset : Z) => - if - (s13 =? - 2 ^ Z.log2 s13) && - (ZRange.normalize - rland << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s13 - 1])%zrange && - (ZRange.normalize ry &' - ZRange.normalize - (ZRange.constant - mask) <=? - ZRange.normalize - rland)%zrange && - (mask =? - Z.ones - (Z.log2 s13 - - offset)) && - (0 <=? offset) && - (offset <=? - Z.log2 s13) && - is_bounded_by_bool - s13 - (ZRange.normalize - rs) && - is_bounded_by_bool - mask - (ZRange.normalize - rmask) && - is_bounded_by_bool - offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_sub - (Z.log2 s13) - offset)%expr @ - (#(Z_cast rx)%expr @ - x14, - #(Z_cast ry)%expr @ - y)))%expr_pat - else Datatypes.None) - args10 - (let (x14, _) := xv in - x14) args8 - (v - (Compile.reflect x4)) - args7 args5 args3 - (v0 - (Compile.reflect - x11)) args2 - (let (x14, _) := - xv0 in - x14) args0 - (let (x14, _) := - xv1 in - x14); - Datatypes.Some (Base x14)); + fv <- (if + is_bounded_by_bool + (let (x14, _) := xv in x14) + (ZRange.normalize args10) && + is_bounded_by_bool + (let (x14, _) := xv0 in x14) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x14, _) := xv1 in x14) + (ZRange.normalize args0) && + ((let (x14, _) := xv in x14) =? + 2 + ^ Z.log2 + (let (x14, _) := xv in + x14)) && + (ZRange.normalize args5 << + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv1 in + x14)) <=? + ZRange.normalize args7)%zrange && + (ZRange.normalize args7 <=? + r[0 ~> (let (x14, _) := xv in + x14) - 1])%zrange && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x14, _) := xv0 in + x14)) <=? + ZRange.normalize args5)%zrange && + ((let (x14, _) := xv0 in x14) =? + Z.ones + (Z.log2 + (let (x14, _) := xv in + x14) - + (let (x14, _) := xv1 in + x14))) && + ((0 <=? + (let (x14, _) := xv1 in x14)) && + ((let (x14, _) := xv1 in x14) <=? + Z.log2 + (let (x14, _) := xv in x14))) + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_sub + (Z.log2 + (let (x14, _) := + xv in + x14)) + (let (x14, _) := + xv1 in + x14))%expr @ + (#(Z_cast args8)%expr @ + v (Compile.reflect x4), + #(Z_cast args3)%expr @ + v0 + (Compile.reflect x11))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -4541,60 +4619,45 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x10 <- (let - '(r1, r2)%zrange := - range in - fun (rs : zrange) - (s9 : Z) - (rx : zrange) - (x10 : expr ℤ) - (rshiftr - ry : zrange) - (y : expr ℤ) - (roffset : zrange) - (offset : Z) => - if - (s9 =? 2 ^ Z.log2 s9) && - (ZRange.normalize ry >> - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftr)%zrange && - (ZRange.normalize - rshiftr <=? - r[0 ~> s9 - 1])%zrange && - is_bounded_by_bool s9 - (ZRange.normalize - rs) && - is_bounded_by_bool - offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_sub - (Z.log2 s9) - (- offset))%expr @ - (#(Z_cast rx)%expr @ - x10, - #(Z_cast ry)%expr @ - y)))%expr_pat - else Datatypes.None) - args6 - (let (x10, _) := xv in - x10) args4 - (v - (Compile.reflect x4)) - args3 args1 - (v0 - (Compile.reflect x8)) - args0 - (let (x10, _) := - xv0 in - x10); - Datatypes.Some (Base x10)); + fv <- (if + is_bounded_by_bool + (let (x10, _) := xv in x10) + (ZRange.normalize args6) && + is_bounded_by_bool + (let (x10, _) := xv0 in x10) + (ZRange.normalize args0) && + ((let (x10, _) := xv in x10) =? + 2 + ^ Z.log2 + (let (x10, _) := xv in + x10)) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x10, _) := xv0 in + x10)) <=? + ZRange.normalize args3)%zrange && + (ZRange.normalize args3 <=? + r[0 ~> (let (x10, _) := xv in + x10) - 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_sub + (Z.log2 + (let (x10, _) := + xv in + x10)) + (- + (let (x10, _) := + xv0 in + x10)))%expr @ + (#(Z_cast args4)%expr @ + v (Compile.reflect x4), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x8))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -4636,28 +4699,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); v <- type.try_make_transport_cps s3 ℤ; v0 <- type.try_make_transport_cps s4 ℤ; - fv <- (x6 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s5 : Z) - (rx : zrange) (x6 : expr ℤ) - (ry : zrange) (y : expr ℤ) => - if - (s5 =? 2 ^ Z.log2 s5) && - (ZRange.normalize ry <=? - r[0 ~> s5 - 1])%zrange && - is_bounded_by_bool s5 - (ZRange.normalize rs) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_sub (Z.log2 s5) 0)%expr @ - (#(Z_cast rx)%expr @ x6, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args2 - (let (x6, _) := xv in x6) args0 - (v (Compile.reflect x4)) args - (v0 (Compile.reflect x5)); - Datatypes.Some (Base x6)); + fv <- (if + is_bounded_by_bool + (let (x6, _) := xv in x6) + (ZRange.normalize args2) && + ((let (x6, _) := xv in x6) =? + 2 ^ Z.log2 (let (x6, _) := xv in x6)) && + (ZRange.normalize args <=? + r[0 ~> (let (x6, _) := xv in x6) - 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_sub + (Z.log2 + (let (x6, _) := xv in x6)) 0)%expr @ + (#(Z_cast args0)%expr @ + v (Compile.reflect x4), + #(Z_cast args)%expr @ + v0 (Compile.reflect x5))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -4744,72 +4805,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x16 <- (let - '(r1, r2)%zrange := range - in - fun (rs : zrange) - (s15 : Z) (rc : zrange) - (c : expr ℤ) - (rx : zrange) - (x16 : expr ℤ) - (rshiftl rland - ry : zrange) - (y : expr ℤ) - (rmask : zrange) - (mask : Z) - (roffset : zrange) - (offset : Z) => - if - (s15 =? 2 ^ Z.log2 s15) && - (ZRange.normalize rland << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize ry &' - ZRange.normalize - (ZRange.constant mask) <=? - ZRange.normalize rland)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s15 - 1])%zrange && - (mask =? - Z.ones - (Z.log2 s15 - offset)) && - (0 <=? offset) && - (offset <=? Z.log2 s15) && - is_bounded_by_bool s15 - (ZRange.normalize rs) && - is_bounded_by_bool mask - (ZRange.normalize rmask) && - is_bounded_by_bool offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s15) - offset)%expr @ - (#(Z_cast rc)%expr @ - c, - #(Z_cast rx)%expr @ - x16, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) - args11 - (let (x16, _) := xv in x16) - args9 - (v (Compile.reflect x5)) - args8 - (v0 (Compile.reflect x6)) - args7 args5 args3 - (v1 (Compile.reflect x13)) - args2 - (let (x16, _) := xv0 in - x16) args0 - (let (x16, _) := xv1 in - x16); - Datatypes.Some (Base x16)); + fv <- (if + is_bounded_by_bool + (let (x16, _) := xv in x16) + (ZRange.normalize args11) && + is_bounded_by_bool + (let (x16, _) := xv0 in x16) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x16, _) := xv1 in x16) + (ZRange.normalize args0) && + ((let (x16, _) := xv in x16) =? + 2 + ^ Z.log2 + (let (x16, _) := xv in x16)) && + (ZRange.normalize args5 << + ZRange.normalize + (ZRange.constant + (let (x16, _) := xv1 in x16)) <=? + ZRange.normalize args7)%zrange && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x16, _) := xv0 in x16)) <=? + ZRange.normalize args5)%zrange && + (ZRange.normalize args7 <=? + r[0 ~> (let (x16, _) := xv in x16) - + 1])%zrange && + ((let (x16, _) := xv0 in x16) =? + Z.ones + (Z.log2 + (let (x16, _) := xv in x16) - + (let (x16, _) := xv1 in x16))) && + ((0 <=? + (let (x16, _) := xv1 in x16)) && + ((let (x16, _) := xv1 in x16) <=? + Z.log2 + (let (x16, _) := xv in x16))) + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_addc + (Z.log2 + (let (x16, _) := + xv in + x16)) + (let (x16, _) := xv1 in + x16))%expr @ + (#(Z_cast args9)%expr @ + v (Compile.reflect x5), + #(Z_cast args8)%expr @ + v0 (Compile.reflect x6), + #(Z_cast args3)%expr @ + v1 (Compile.reflect x13))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -5091,71 +5141,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); v1 <- type.try_make_transport_cps s6 ℤ; - fv <- (x16 <- (let - '(r1, r2)%zrange := range - in - fun (rs : zrange) - (s15 : Z) (rc : zrange) - (c : expr ℤ) - (rshiftl rland - ry : zrange) - (y : expr ℤ) - (rmask : zrange) - (mask : Z) - (roffset : zrange) - (offset : Z) - (rx : zrange) - (x16 : expr ℤ) => - if - (s15 =? 2 ^ Z.log2 s15) && - (ZRange.normalize rland << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s15 - 1])%zrange && - (ZRange.normalize ry &' - ZRange.normalize - (ZRange.constant mask) <=? - ZRange.normalize rland)%zrange && - (mask =? - Z.ones - (Z.log2 s15 - offset)) && - (0 <=? offset) && - (offset <=? Z.log2 s15) && - is_bounded_by_bool s15 - (ZRange.normalize rs) && - is_bounded_by_bool mask - (ZRange.normalize rmask) && - is_bounded_by_bool offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s15) - offset)%expr @ - (#(Z_cast rc)%expr @ - c, - #(Z_cast rx)%expr @ - x16, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) - args11 - (let (x16, _) := xv in x16) - args9 - (v (Compile.reflect x5)) - args8 args5 args3 - (v0 (Compile.reflect x13)) - args2 - (let (x16, _) := xv0 in - x16) args0 - (let (x16, _) := xv1 in - x16) args7 - (v1 (Compile.reflect x7)); - Datatypes.Some (Base x16)); + fv <- (if + is_bounded_by_bool + (let (x16, _) := xv in x16) + (ZRange.normalize args11) && + is_bounded_by_bool + (let (x16, _) := xv0 in x16) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x16, _) := xv1 in x16) + (ZRange.normalize args0) && + ((let (x16, _) := xv in x16) =? + 2 + ^ Z.log2 + (let (x16, _) := xv in x16)) && + (ZRange.normalize args5 << + ZRange.normalize + (ZRange.constant + (let (x16, _) := xv1 in x16)) <=? + ZRange.normalize args8)%zrange && + (ZRange.normalize args8 <=? + r[0 ~> (let (x16, _) := xv in x16) - + 1])%zrange && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x16, _) := xv0 in x16)) <=? + ZRange.normalize args5)%zrange && + ((let (x16, _) := xv0 in x16) =? + Z.ones + (Z.log2 + (let (x16, _) := xv in x16) - + (let (x16, _) := xv1 in x16))) && + ((0 <=? + (let (x16, _) := xv1 in x16)) && + ((let (x16, _) := xv1 in x16) <=? + Z.log2 + (let (x16, _) := xv in x16))) + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_addc + (Z.log2 + (let (x16, _) := + xv in + x16)) + (let (x16, _) := xv1 in + x16))%expr @ + (#(Z_cast args9)%expr @ + v (Compile.reflect x5), + #(Z_cast args7)%expr @ + v1 (Compile.reflect x7), + #(Z_cast args3)%expr @ + v0 (Compile.reflect x13))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -5421,55 +5461,45 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (let - '(r1, r2)%zrange := range - in - fun (rs : zrange) - (s11 : Z) (rc : zrange) - (c : expr ℤ) - (rx : zrange) - (x12 : expr ℤ) - (rshiftr ry : zrange) - (y : expr ℤ) - (roffset : zrange) - (offset : Z) => - if - (s11 =? 2 ^ Z.log2 s11) && - (ZRange.normalize ry >> - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize rshiftr)%zrange && - (ZRange.normalize rshiftr <=? - r[0 ~> s11 - 1])%zrange && - is_bounded_by_bool s11 - (ZRange.normalize rs) && - is_bounded_by_bool offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s11) - (- offset))%expr @ - (#(Z_cast rc)%expr @ - c, - #(Z_cast rx)%expr @ - x12, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args7 - (let (x12, _) := xv in x12) - args5 - (v (Compile.reflect x5)) - args4 - (v0 (Compile.reflect x6)) - args3 args1 - (v1 (Compile.reflect x10)) - args0 - (let (x12, _) := xv0 in - x12); - Datatypes.Some (Base x12)); + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args7) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in x12) =? + 2 + ^ Z.log2 + (let (x12, _) := xv in x12)) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args3)%zrange && + (ZRange.normalize args3 <=? + r[0 ~> (let (x12, _) := xv in x12) - + 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_addc + (Z.log2 + (let (x12, _) := + xv in + x12)) + (- + (let (x12, _) := + xv0 in + x12)))%expr @ + (#(Z_cast args5)%expr @ + v (Compile.reflect x5), + #(Z_cast args4)%expr @ + v0 (Compile.reflect x6), + #(Z_cast args1)%expr @ + v1 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -5565,54 +5595,45 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); v1 <- type.try_make_transport_cps s6 ℤ; - fv <- (x12 <- (let - '(r1, r2)%zrange := range - in - fun (rs : zrange) - (s11 : Z) (rc : zrange) - (c : expr ℤ) - (rshiftr ry : zrange) - (y : expr ℤ) - (roffset : zrange) - (offset : Z) - (rx : zrange) - (x12 : expr ℤ) => - if - (s11 =? 2 ^ Z.log2 s11) && - (ZRange.normalize ry >> - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize rshiftr)%zrange && - (ZRange.normalize rshiftr <=? - r[0 ~> s11 - 1])%zrange && - is_bounded_by_bool s11 - (ZRange.normalize rs) && - is_bounded_by_bool offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s11) - (- offset))%expr @ - (#(Z_cast rc)%expr @ - c, - #(Z_cast rx)%expr @ - x12, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args7 - (let (x12, _) := xv in x12) - args5 - (v (Compile.reflect x5)) - args4 args1 - (v0 (Compile.reflect x10)) - args0 - (let (x12, _) := xv0 in - x12) args3 - (v1 (Compile.reflect x7)); - Datatypes.Some (Base x12)); + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in x12) + (ZRange.normalize args7) && + is_bounded_by_bool + (let (x12, _) := xv0 in x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in x12) =? + 2 + ^ Z.log2 + (let (x12, _) := xv in x12)) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := xv0 in x12)) <=? + ZRange.normalize args4)%zrange && + (ZRange.normalize args4 <=? + r[0 ~> (let (x12, _) := xv in x12) - + 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_addc + (Z.log2 + (let (x12, _) := + xv in + x12)) + (- + (let (x12, _) := + xv0 in + x12)))%expr @ + (#(Z_cast args5)%expr @ + v (Compile.reflect x5), + #(Z_cast args3)%expr @ + v1 (Compile.reflect x7), + #(Z_cast args1)%expr @ + v0 (Compile.reflect x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -5694,31 +5715,29 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s4 ℤ; v0 <- type.try_make_transport_cps s5 ℤ; v1 <- type.try_make_transport_cps s6 ℤ; - fv <- (x8 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s7 : Z) - (rc : zrange) (c : expr ℤ) - (rx : zrange) (x8 : expr ℤ) - (ry : zrange) (y : expr ℤ) => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry <=? - r[0 ~> s7 - 1])%zrange && - is_bounded_by_bool s7 - (ZRange.normalize rs) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc (Z.log2 s7) 0)%expr @ - (#(Z_cast rc)%expr @ c, - #(Z_cast rx)%expr @ x8, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args3 - (let (x8, _) := xv in x8) args1 - (v (Compile.reflect x5)) args0 - (v0 (Compile.reflect x6)) args - (v1 (Compile.reflect x7)); - Datatypes.Some (Base x8)); + fv <- (if + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args3) && + ((let (x8, _) := xv in x8) =? + 2 ^ Z.log2 (let (x8, _) := xv in x8)) && + (ZRange.normalize args <=? + r[0 ~> (let (x8, _) := xv in x8) - 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_addc + (Z.log2 + (let (x8, _) := xv in x8)) + 0)%expr @ + (#(Z_cast args1)%expr @ + v (Compile.reflect x5), + #(Z_cast args0)%expr @ + v0 (Compile.reflect x6), + #(Z_cast args)%expr @ + v1 (Compile.reflect x7))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -5828,98 +5847,90 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x16 <- (let - '(r1, r2)%zrange := - range in - fun (rs : zrange) - (s15 : Z) - (rb : zrange) - (b4 : expr ℤ) - (rx : zrange) - (x16 : expr ℤ) - (rshiftl rland - ry : zrange) - (y : expr ℤ) - (rmask : zrange) - (mask : Z) - (roffset : zrange) - (offset : Z) => - if - (s15 =? - 2 ^ Z.log2 s15) && - (ZRange.normalize - rland << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s15 - 1])%zrange && - (ZRange.normalize - ry &' - ZRange.normalize - (ZRange.constant - mask) <=? - ZRange.normalize - rland)%zrange && - (mask =? - Z.ones - (Z.log2 s15 - - offset)) && - (0 <=? offset) && - (offset <=? - Z.log2 s15) && - is_bounded_by_bool - s15 - (ZRange.normalize - rs) && - is_bounded_by_bool - mask - (ZRange.normalize - rmask) && - is_bounded_by_bool - offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 - s15) - offset)%expr @ - (#(Z_cast rb)%expr @ - b4, - #(Z_cast rx)%expr @ - x16, - #(Z_cast ry)%expr @ - y)))%expr_pat - else - Datatypes.None) - args11 - (let (x16, _) := + fv <- (if + is_bounded_by_bool + (let (x16, _) := xv in + x16) + (ZRange.normalize args11) && + is_bounded_by_bool + (let (x16, _) := xv0 in + x16) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x16, _) := xv1 in + x16) + (ZRange.normalize args0) && + ((let (x16, _) := xv in + x16) =? + 2 + ^ Z.log2 + (let (x16, _) := + xv in + x16)) && + (ZRange.normalize args5 << + ZRange.normalize + (ZRange.constant + (let (x16, _) := + xv1 in + x16)) <=? + ZRange.normalize args7)%zrange && + (ZRange.normalize args7 <=? + r[0 ~> (let (x16, _) := xv in - x16) args9 - (v - (Compile.reflect - x5)) args8 - (v0 - (Compile.reflect - x6)) args7 - args5 args3 - (v1 - (Compile.reflect - x13)) args2 - (let (x16, _) := - xv0 in - x16) args0 - (let (x16, _) := - xv1 in - x16); - Datatypes.Some (Base x16)); + x16) - 1])%zrange && + (ZRange.normalize args3 &' + ZRange.normalize + (ZRange.constant + (let (x16, _) := + xv0 in + x16)) <=? + ZRange.normalize args5)%zrange && + ((let (x16, _) := xv0 in + x16) =? + Z.ones + (Z.log2 + (let (x16, _) := + xv in + x16) - + (let (x16, _) := + xv1 in + x16))) && + ((0 <=? + (let (x16, _) := xv1 in + x16)) && + ((let (x16, _) := xv1 in + x16) <=? + Z.log2 + (let (x16, _) := xv in + x16))) + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_subb + (Z.log2 + (let + (x16, + _) := + xv in + x16)) + (let + (x16, _) := + xv1 in + x16))%expr @ + (#(Z_cast args9)%expr @ + v + (Compile.reflect + x5), + #(Z_cast args8)%expr @ + v0 + (Compile.reflect + x6), + #(Z_cast args3)%expr @ + v1 + (Compile.reflect + x13))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -6080,75 +6091,62 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x12 <- (let - '(r1, r2)%zrange := - range in - fun (rs : zrange) - (s11 : Z) - (rb : zrange) - (b3 : expr ℤ) - (rx : zrange) - (x12 : expr ℤ) - (rshiftr - ry : zrange) - (y : expr ℤ) - (roffset : zrange) - (offset : Z) => - if - (s11 =? - 2 ^ Z.log2 s11) && - (ZRange.normalize - ry >> - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftr)%zrange && - (ZRange.normalize - rshiftr <=? - r[0 ~> s11 - 1])%zrange && - is_bounded_by_bool - s11 - (ZRange.normalize - rs) && - is_bounded_by_bool - offset - (ZRange.normalize - roffset) - then - Datatypes.Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 - s11) - (- offset))%expr @ - (#(Z_cast rb)%expr @ - b3, - #(Z_cast rx)%expr @ - x12, - #(Z_cast ry)%expr @ - y)))%expr_pat - else - Datatypes.None) - args7 - (let (x12, _) := + fv <- (if + is_bounded_by_bool + (let (x12, _) := xv in + x12) + (ZRange.normalize args7) && + is_bounded_by_bool + (let (x12, _) := xv0 in + x12) + (ZRange.normalize args0) && + ((let (x12, _) := xv in + x12) =? + 2 + ^ Z.log2 + (let (x12, _) := + xv in + x12)) && + (ZRange.normalize args1 >> + ZRange.normalize + (ZRange.constant + (let (x12, _) := + xv0 in + x12)) <=? + ZRange.normalize args3)%zrange && + (ZRange.normalize args3 <=? + r[0 ~> (let (x12, _) := xv in - x12) args5 - (v - (Compile.reflect - x5)) args4 - (v0 - (Compile.reflect - x6)) args3 - args1 - (v1 - (Compile.reflect - x10)) args0 - (let (x12, _) := - xv0 in - x12); - Datatypes.Some (Base x12)); + x12) - 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_subb + (Z.log2 + (let + (x12, + _) := + xv in + x12)) + (- + (let + (x12, _) := + xv0 in + x12)))%expr @ + (#(Z_cast args5)%expr @ + v + (Compile.reflect + x5), + #(Z_cast args4)%expr @ + v0 + (Compile.reflect + x6), + #(Z_cast args1)%expr @ + v1 + (Compile.reflect + x10))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -6197,31 +6195,29 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s4 ℤ; v0 <- type.try_make_transport_cps s5 ℤ; v1 <- type.try_make_transport_cps s6 ℤ; - fv <- (x8 <- (let - '(r1, r2)%zrange := range in - fun (rs : zrange) (s7 : Z) - (rb : zrange) (b2 : expr ℤ) - (rx : zrange) (x8 : expr ℤ) - (ry : zrange) (y : expr ℤ) => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry <=? - r[0 ~> s7 - 1])%zrange && - is_bounded_by_bool s7 - (ZRange.normalize rs) - then - Datatypes.Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_subb (Z.log2 s7) 0)%expr @ - (#(Z_cast rb)%expr @ b2, - #(Z_cast rx)%expr @ x8, - #(Z_cast ry)%expr @ y)))%expr_pat - else Datatypes.None) args3 - (let (x8, _) := xv in x8) args1 - (v (Compile.reflect x5)) args0 - (v0 (Compile.reflect x6)) args - (v1 (Compile.reflect x7)); - Datatypes.Some (Base x8)); + fv <- (if + is_bounded_by_bool + (let (x8, _) := xv in x8) + (ZRange.normalize args3) && + ((let (x8, _) := xv in x8) =? + 2 ^ Z.log2 (let (x8, _) := xv in x8)) && + (ZRange.normalize args <=? + r[0 ~> (let (x8, _) := xv in x8) - 1])%zrange + then + Datatypes.Some + (Base + (#(Z_cast2 range)%expr @ + (#(fancy_subb + (Z.log2 + (let (x8, _) := xv in x8)) + 0)%expr @ + (#(Z_cast args1)%expr @ + v (Compile.reflect x5), + #(Z_cast args0)%expr @ + v0 (Compile.reflect x6), + #(Z_cast args)%expr @ + v1 (Compile.reflect x7))))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets -- cgit v1.2.3