aboutsummaryrefslogtreecommitdiff
path: root/src/fancy_with_casts_rewrite_head.out
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-06 16:44:52 -0500
committerGravatar Jason Gross <jasongross9@gmail.com>2019-03-07 13:33:20 -0500
commitb35bceb2848c94c3a38e85ba5cb66560ff204164 (patch)
tree791a426b537b3557de43b83a482af62f703381f5 /src/fancy_with_casts_rewrite_head.out
parent0774eb4535eff89d0fd4eba3bc4c4f89864812b1 (diff)
Update .out files
Diffstat (limited to 'src/fancy_with_casts_rewrite_head.out')
-rw-r--r--src/fancy_with_casts_rewrite_head.out3336
1 files changed, 1666 insertions, 1670 deletions
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
@@ -2652,43 +2704,34 @@ 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) =?
- 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));
+ 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 23:52:50 +0000