diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-06 16:44:52 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-03-07 13:33:20 -0500 |
| commit | b35bceb2848c94c3a38e85ba5cb66560ff204164 (patch) | |
| tree | 791a426b537b3557de43b83a482af62f703381f5 /src | |
| parent | 0774eb4535eff89d0fd4eba3bc4c4f89864812b1 (diff) | |
Update .out files
Diffstat (limited to 'src')
| -rw-r--r-- | src/arith_rewrite_head.out | 959 | ||||
| -rw-r--r-- | src/arith_with_casts_rewrite_head.out | 712 | ||||
| -rw-r--r-- | src/fancy_with_casts_rewrite_head.out | 3336 | ||||
| -rw-r--r-- | src/nbe_rewrite_head.out | 83 | ||||
| -rw-r--r-- | src/strip_literal_casts_rewrite_head.out | 15 |
5 files changed, 2541 insertions, 2564 deletions
diff --git a/src/arith_rewrite_head.out b/src/arith_rewrite_head.out index a7a804263..e2755de01 100644 --- a/src/arith_rewrite_head.out +++ b/src/arith_rewrite_head.out @@ -233,10 +233,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some x0 - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 0 + then Datatypes.Some (Base x0) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -246,26 +245,81 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end;; match x0 with | @expr.Ident _ _ _ t idc => - (args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some x - else Datatypes.None); - Datatypes.Some (Base x1)); - Datatypes.Some (fv0 <-- fv; - Base fv0)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end);; + args <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype + (ℤ -> (projT1 args))%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (ℤ -> (projT1 args))%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (if (let (x1, _) := xv in x1) =? 0 + then Datatypes.Some (Base x) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => + match x with + | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 => + _ <- invert_bind_args idc0 Raw.ident.Z_opp; + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (s0 -> s)%ptype + then + v <- type.try_make_transport_cps s0 ℤ; + v0 <- type.try_make_transport_cps s ℤ; + Datatypes.Some + (Base + (- + (v (Compile.reflect x2) + v0 (Compile.reflect x1)))%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ + (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ + (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;; + match x with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (s -> ℤ)%ptype + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some (Base (x0 - v (Compile.reflect x1))%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;; + match x0 with + | @expr.Ident _ _ _ t idc => match x with | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x1 => (_ <- invert_bind_args idc0 Raw.ident.Z_opp; @@ -281,13 +335,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then v <- type.try_make_transport_cps s ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - fv <- (x2 <- (if (let (x2, _) := xv in x2) >? 0 - then - Datatypes.Some - (##(let (x2, _) := xv in x2) - - v (Compile.reflect x1))%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) >? 0 + then + Datatypes.Some + (Base + (##(let (x2, _) := xv in x2) - + v (Compile.reflect x1))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -306,14 +360,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then v <- type.try_make_transport_cps s ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - fv <- (x2 <- (if (let (x2, _) := xv in x2) <? 0 - then - Datatypes.Some - (- - (v (Compile.reflect x1) + - ##(- (let (x2, _) := xv in x2))%Z))%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) <? 0 + then + Datatypes.Some + (Base + (- + (v (Compile.reflect x1) + + ##(- (let (x2, _) := xv in x2))%Z))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -326,6 +380,20 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | _ => Datatypes.None end | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => + (_ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (ℤ -> s)%ptype + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some (Base (x - v (Compile.reflect x1))%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end);; match x with | @expr.Ident _ _ _ t0 idc0 => (args <- invert_bind_args idc0 Raw.ident.Literal; @@ -341,13 +409,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); v <- type.try_make_transport_cps s ℤ; - fv <- (x2 <- (if (let (x2, _) := xv in x2) >? 0 - then - Datatypes.Some - (##(let (x2, _) := xv in x2) - - v (Compile.reflect x1))%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) >? 0 + then + Datatypes.Some + (Base + (##(let (x2, _) := xv in x2) - + v (Compile.reflect x1))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -366,91 +434,25 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); v <- type.try_make_transport_cps s ℤ; - fv <- (x2 <- (if (let (x2, _) := xv in x2) <? 0 - then - Datatypes.Some - (- - (##(- (let (x2, _) := xv in x2))%Z + - v (Compile.reflect x1)))%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) <? 0 + then + Datatypes.Some + (Base + (- + (##(- (let (x2, _) := xv in x2))%Z + + v (Compile.reflect x1)))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end - | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 => - _ <- invert_bind_args idc0 Raw.ident.Z_opp; - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (s0 -> s)%ptype - then - v <- type.try_make_transport_cps s0 ℤ; - v0 <- type.try_make_transport_cps s ℤ; - Datatypes.Some - (Base - (- - (v (Compile.reflect x2) + v0 (Compile.reflect x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ - (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None | _ => Datatypes.None end | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None | _ => Datatypes.None - end;; - match x with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (s -> ℤ)%ptype - then - v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (x0 - v (Compile.reflect x1))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - match x0 with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (ℤ -> s)%ptype - then - v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (x - v (Compile.reflect x1))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None end);; Datatypes.None);;; Base (x + x0)%expr)%option @@ -458,30 +460,6 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 : expr ℤ => (((match x with | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) * - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted (ℤ -> ℤ)%ptype @@ -493,10 +471,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (##0)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 0 + then Datatypes.Some (Base (##0)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -517,10 +494,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (##0)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 0 + then Datatypes.Some (Base (##0)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -541,10 +517,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some x0 - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 1 + then Datatypes.Some (Base x0) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -565,10 +540,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some x - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 1 + then Datatypes.Some (Base x) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -589,11 +563,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then v <- type.try_make_transport_cps s ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - fv <- (x2 <- (if (let (x2, _) := xv in x2) =? -1 - then - Datatypes.Some (v (Compile.reflect x1)) - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) =? -1 + then + Datatypes.Some (Base (v (Compile.reflect x1))) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -621,11 +594,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); v <- type.try_make_transport_cps s ℤ; - fv <- (x2 <- (if (let (x2, _) := xv in x2) =? -1 - then - Datatypes.Some (v (Compile.reflect x1)) - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) =? -1 + then + Datatypes.Some (Base (v (Compile.reflect x1))) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -651,60 +623,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? -1 - then Datatypes.Some (- x0)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); - Datatypes.Some (fv0 <-- fv; - Base fv0)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - match x0 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? -1 - then Datatypes.Some (- x)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); - Datatypes.Some (fv0 <-- fv; - Base fv0)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args) -> ℤ)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args) -> ℤ)%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) <? 0 - then - Datatypes.Some - (- (##(- (let (x1, _) := xv in x1))%Z * x0))%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? -1 + then Datatypes.Some (Base (- x0)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -725,12 +646,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) <? 0 - then - Datatypes.Some - (- (x * ##(- (let (x1, _) := xv in x1))%Z))%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? -1 + then Datatypes.Some (Base (- x)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -791,49 +709,125 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end;; match x0 with | @expr.Ident _ _ _ t idc => + match x with + | @expr.Ident _ _ _ t0 idc0 => + args <- invert_bind_args idc0 Raw.ident.Literal; + args0 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype + ((projT1 args) -> (projT1 args0))%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + ((projT1 args) -> (projT1 args0))%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); + Datatypes.Some + (Base + (##((let (x1, _) := xv in x1) * + (let (x1, _) := xv0 in x1))%Z)%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | _ => Datatypes.None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (ℤ -> s)%ptype + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some (Base (- (x * v (Compile.reflect x1)))%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;; + match x with + | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype + ((projT1 args) -> ℤ)%ptype with | Datatypes.Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype + ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if - ((let (x1, _) := xv in x1) =? - 2 ^ Z.log2 (let (x1, _) := xv in x1)) && - negb ((let (x1, _) := xv in x1) =? 2) - then - Datatypes.Some - (x << ##(Z.log2 (let (x1, _) := xv in x1)))%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) <? 0 + then + Datatypes.Some + (Base + (- (##(- (let (x1, _) := xv in x1))%Z * x0))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => - _ <- invert_bind_args idc Raw.ident.Z_opp; + | _ => Datatypes.None + end;; + match x0 with + | @expr.Ident _ _ _ t idc => + (args <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype + (ℤ -> (projT1 args))%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (ℤ -> (projT1 args))%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (if (let (x1, _) := xv in x1) <? 0 + then + Datatypes.Some + (Base + (- (x * ##(- (let (x1, _) := xv in x1))%Z))%expr) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end);; + args <- invert_bind_args idc Raw.ident.Literal; match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype + pattern.type.unify_extracted (ℤ -> ℤ)%ptype + (ℤ -> (projT1 args))%ptype with | Datatypes.Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (ℤ -> s)%ptype + (ℤ -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (- (x * v (Compile.reflect x1)))%expr) + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (if + ((let (x1, _) := xv in x1) =? + 2 ^ Z.log2 (let (x1, _) := xv in x1)) && + negb ((let (x1, _) := xv in x1) =? 2) + then + Datatypes.Some + (Base + (x << ##(Z.log2 (let (x1, _) := xv in x1)))%expr) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None | _ => Datatypes.None end;; match x with @@ -849,15 +843,15 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if - ((let (x1, _) := xv in x1) =? - 2 ^ Z.log2 (let (x1, _) := xv in x1)) && - negb ((let (x1, _) := xv in x1) =? 2) - then - Datatypes.Some - (x0 << ##(Z.log2 (let (x1, _) := xv in x1)))%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if + ((let (x1, _) := xv in x1) =? + 2 ^ Z.log2 (let (x1, _) := xv in x1)) && + negb ((let (x1, _) := xv in x1) =? 2) + then + Datatypes.Some + (Base + (x0 << ##(Z.log2 (let (x1, _) := xv in x1)))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -893,19 +887,19 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args0); v <- type.try_make_transport_cps s2 ℤ; v0 <- type.try_make_transport_cps s1 ℤ; - fv <- (x5 <- (if - (Z.abs (let (x5, _) := xv in x5) <=? - Z.abs max_const_val) && - (Z.abs (let (x5, _) := xv0 in x5) <=? - Z.abs max_const_val) - then - Datatypes.Some - (v (Compile.reflect x4) * - (v0 (Compile.reflect x3) * - (##(let (x5, _) := xv in x5) * - ##(let (x5, _) := xv0 in x5))))%expr - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + (Z.abs (let (x5, _) := xv in x5) <=? + Z.abs max_const_val) && + (Z.abs (let (x5, _) := xv0 in x5) <=? + Z.abs max_const_val) + then + Datatypes.Some + (Base + (v (Compile.reflect x4) * + (v0 (Compile.reflect x3) * + (##(let (x5, _) := xv in x5) * + ##(let (x5, _) := xv0 in x5))))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -950,19 +944,19 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s2 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x5 <- (if - (Z.abs (let (x5, _) := xv in x5) <=? - Z.abs max_const_val) && - (Z.abs (let (x5, _) := xv0 in x5) <=? - Z.abs max_const_val) - then - Datatypes.Some - (v (Compile.reflect x2) * - (v0 (Compile.reflect x4) * - (##(let (x5, _) := xv in x5) * - ##(let (x5, _) := xv0 in x5))))%expr - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + (Z.abs (let (x5, _) := xv in x5) <=? + Z.abs max_const_val) && + (Z.abs (let (x5, _) := xv0 in x5) <=? + Z.abs max_const_val) + then + Datatypes.Some + (Base + (v (Compile.reflect x2) * + (v0 (Compile.reflect x4) * + (##(let (x5, _) := xv in x5) * + ##(let (x5, _) := xv0 in x5))))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -997,16 +991,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args0); v <- type.try_make_transport_cps s0 ℤ; v0 <- type.try_make_transport_cps s ℤ; - fv <- (x3 <- (if - Z.abs (let (x3, _) := xv in x3) <=? - Z.abs max_const_val - then - Datatypes.Some - (v (Compile.reflect x2) * - (v0 (Compile.reflect x1) * - ##(let (x3, _) := xv in x3)))%expr - else Datatypes.None); - Datatypes.Some (Base x3)); + fv <- (if + Z.abs (let (x3, _) := xv in x3) <=? + Z.abs max_const_val + then + Datatypes.Some + (Base + (v (Compile.reflect x2) * + (v0 (Compile.reflect x1) * + ##(let (x3, _) := xv in x3)))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1035,14 +1029,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if - Z.abs (let (x1, _) := xv in x1) <=? - Z.abs max_const_val - then - Datatypes.Some - (x0 * ##(let (x1, _) := xv in x1))%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if + Z.abs (let (x1, _) := xv in x1) <=? + Z.abs max_const_val + then + Datatypes.Some + (Base (x0 * ##(let (x1, _) := xv in x1))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1072,11 +1065,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args0); v <- type.try_make_transport_cps s ℤ; - fv <- (x2 <- (if (let (x2, _) := xv in x2) =? 0 - then - Datatypes.Some (v (Compile.reflect x1)) - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) =? 0 + then + Datatypes.Some (Base (v (Compile.reflect x1))) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1099,10 +1091,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (- x0)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 0 + then Datatypes.Some (Base (- x0)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1123,10 +1114,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some x - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 0 + then Datatypes.Some (Base x) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1134,6 +1124,74 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => match x with + | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 => + _ <- invert_bind_args idc0 Raw.ident.Z_opp; + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (s0 -> s)%ptype + then + v <- type.try_make_transport_cps s0 ℤ; + v0 <- type.try_make_transport_cps s ℤ; + Datatypes.Some + (Base + (v0 (Compile.reflect x1) - v (Compile.reflect x2))%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ + (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ + (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;; + match x with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (s -> ℤ)%ptype + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some (Base (- (v (Compile.reflect x1) + x0))%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;; + match x0 with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => + (_ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (ℤ -> s)%ptype + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some (Base (x + v (Compile.reflect x1))%expr) + else Datatypes.None + | Datatypes.None => Datatypes.None + end);; + match x with | @expr.Ident _ _ _ t0 idc0 => (args <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_opp; @@ -1148,13 +1206,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); v <- type.try_make_transport_cps s ℤ; - fv <- (x2 <- (if (let (x2, _) := xv in x2) >? 0 - then - Datatypes.Some - (##(let (x2, _) := xv in x2) + - v (Compile.reflect x1))%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) >? 0 + then + Datatypes.Some + (Base + (##(let (x2, _) := xv in x2) + + v (Compile.reflect x1))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1173,13 +1231,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); v <- type.try_make_transport_cps s ℤ; - fv <- (x2 <- (if (let (x2, _) := xv in x2) <? 0 - then - Datatypes.Some - (v (Compile.reflect x1) - - ##(- (let (x2, _) := xv in x2))%Z)%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) <? 0 + then + Datatypes.Some + (Base + (v (Compile.reflect x1) - + ##(- (let (x2, _) := xv in x2))%Z)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1205,12 +1263,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) <? 0 - then - Datatypes.Some - (- (##(- (let (x1, _) := xv in x1))%Z + x0))%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) <? 0 + then + Datatypes.Some + (Base + (- (##(- (let (x1, _) := xv in x1))%Z + x0))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1232,14 +1290,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then v <- type.try_make_transport_cps s ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x2 <- (if (let (x2, _) := xv in x2) >? 0 - then - Datatypes.Some - (- - (v (Compile.reflect x1) + - ##(let (x2, _) := xv in x2)))%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) >? 0 + then + Datatypes.Some + (Base + (- + (v (Compile.reflect x1) + + ##(let (x2, _) := xv in x2)))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1258,13 +1316,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then v <- type.try_make_transport_cps s ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x2 <- (if (let (x2, _) := xv in x2) <? 0 - then - Datatypes.Some - (##(- (let (x2, _) := xv in x2))%Z - - v (Compile.reflect x1))%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if (let (x2, _) := xv in x2) <? 0 + then + Datatypes.Some + (Base + (##(- (let (x2, _) := xv in x2))%Z - + v (Compile.reflect x1))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1290,89 +1348,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) <? 0 - then - Datatypes.Some - (x + ##(- (let (x1, _) := xv in x1))%Z)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) <? 0 + then + Datatypes.Some + (Base (x + ##(- (let (x1, _) := xv in x1))%Z)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => - match x with - | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 => - _ <- invert_bind_args idc0 Raw.ident.Z_opp; - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (s0 -> s)%ptype - then - v <- type.try_make_transport_cps s0 ℤ; - v0 <- type.try_make_transport_cps s ℤ; - Datatypes.Some - (Base - (v0 (Compile.reflect x1) - v (Compile.reflect x2))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ - (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - match x with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (s -> ℤ)%ptype - then - v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (- (v (Compile.reflect x1) + x0))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - match x0 with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 => - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (ℤ -> s)%ptype - then - v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (x + v (Compile.reflect x1))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None | _ => Datatypes.None end);; Datatypes.None);;; @@ -1427,10 +1412,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some x - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 1 + then Datatypes.Some (Base x) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1447,14 +1431,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if - (let (x1, _) := xv in x1) =? - 2 ^ Z.log2 (let (x1, _) := xv in x1) - then - Datatypes.Some - (x >> ##(Z.log2 (let (x1, _) := xv in x1)))%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if + (let (x1, _) := xv in x1) =? + 2 ^ Z.log2 (let (x1, _) := xv in x1) + then + Datatypes.Some + (Base + (x >> ##(Z.log2 (let (x1, _) := xv in x1)))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1479,10 +1463,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some (##0)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if (let (x1, _) := xv in x1) =? 1 + then Datatypes.Some (Base (##0)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1499,14 +1482,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if - (let (x1, _) := xv in x1) =? - 2 ^ Z.log2 (let (x1, _) := xv in x1) - then - Datatypes.Some - (x &' ##((let (x1, _) := xv in x1) - 1)%Z)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if + (let (x1, _) := xv in x1) =? + 2 ^ Z.log2 (let (x1, _) := xv in x1) + then + Datatypes.Some + (Base (x &' ##((let (x1, _) := xv in x1) - 1)%Z)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1528,54 +1510,29 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Z_shiftl => fun x x0 : expr ℤ => Base (x << x0)%expr | Z_land => fun x x0 : expr ℤ => - (((match x0 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - (ℤ -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (##0)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); - Datatypes.Some (fv0 <-- fv; - Base fv0)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args) -> ℤ)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args) -> ℤ)%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x1 <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (##0)%expr - else Datatypes.None); - Datatypes.Some (Base x1)); - Datatypes.Some (fv0 <-- fv; - Base fv0)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end);; + ((match x0 with + | @expr.Ident _ _ _ t idc => + args <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype + (ℤ -> (projT1 args))%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (ℤ -> (projT1 args))%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (if (let (x1, _) := xv in x1) =? 0 + then Datatypes.Some (Base (##0)%expr) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | _ => Datatypes.None + end;; Datatypes.None);;; Base (x &' x0)%expr)%option | Z_lor => fun x x0 : expr ℤ => Base (x || x0)%expr diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out index 001332dad..06e7a732b 100644 --- a/src/arith_with_casts_rewrite_head.out +++ b/src/arith_with_casts_rewrite_head.out @@ -234,13 +234,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x2 <- (if - ((let (x2, _) := xv in x2) =? 0) && - is_bounded_by_bool (let (x2, _) := xv in x2) - (ZRange.normalize args0) - then Datatypes.Some x0 - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x2, _) := xv in x2) =? 0) + then Datatypes.Some (Base x0) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -267,13 +265,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x2 <- (if - ((let (x2, _) := xv in x2) =? 0) && - is_bounded_by_bool (let (x2, _) := xv in x2) - (ZRange.normalize args0) - then Datatypes.Some x - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x2, _) := xv in x2) =? 0) + then Datatypes.Some (Base x) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -294,6 +290,28 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 : expr ℤ => ((match x with | (@expr.Ident _ _ _ t idc @ @expr.Ident _ _ _ t0 idc0)%expr_pat => + (args <- invert_bind_args idc0 Raw.ident.Literal; + args0 <- invert_bind_args idc Raw.ident.Z_cast; + match + pattern.type.unify_extracted (ℤ -> ℤ)%ptype + ((projT1 args) -> ℤ)%ptype + with + | Datatypes.Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + ((projT1 args) -> ℤ)%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (if + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x2, _) := xv in x2) =? 0) + then Datatypes.Some (Base (- x0)%expr) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end);; match x0 with | (@expr.Ident _ _ _ t1 idc1 @ (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s2 _ @@ -314,18 +332,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); v <- type.try_make_transport_cps s2 ℤ; - fv <- (x5 <- (if - ((let (x5, _) := xv in x5) =? 0) && - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange && - is_bounded_by_bool - (let (x5, _) := xv in x5) args3 - then - Datatypes.Some - (#(Z_cast args)%expr @ - v (Compile.reflect x4))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange && + is_bounded_by_bool 0 (ZRange.normalize args3) && + ((let (x5, _) := xv in x5) =? 0) + then + Datatypes.Some + (Base + (#(Z_cast args)%expr @ v (Compile.reflect x4))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -359,30 +375,6 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => Datatypes.None | _ => Datatypes.None - end;; - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Z_cast; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args) -> ℤ)%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args) -> ℤ)%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x2 <- (if - ((let (x2, _) := xv in x2) =? 0) && - is_bounded_by_bool (let (x2, _) := xv in x2) - (ZRange.normalize args0) - then Datatypes.Some (- x0)%expr - else Datatypes.None); - Datatypes.Some (Base x2)); - Datatypes.Some (fv0 <-- fv; - Base fv0)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None end | (@expr.Ident _ _ _ t idc @ ($_)%expr)%expr_pat | (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _)%expr_pat | @@ -407,14 +399,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with if type.type_beq base.type base.type.type_beq ℤ s1 then v <- type.try_make_transport_cps s1 ℤ; - fv <- (x3 <- (if - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange - then - Datatypes.Some - (#(Z_cast args)%expr @ v (Compile.reflect x2))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x3)); + fv <- (if + (ZRange.normalize args <=? - ZRange.normalize args1)%zrange + then + Datatypes.Some + (Base + (#(Z_cast args)%expr @ v (Compile.reflect x2))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -478,13 +469,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x2 <- (if - ((let (x2, _) := xv in x2) =? 0) && - is_bounded_by_bool (let (x2, _) := xv in x2) - (ZRange.normalize args0) - then Datatypes.Some (##0)%expr - else Datatypes.None); - Datatypes.Some (Base x2)); + fv <- (if + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x2, _) := xv in x2) =? 0) + then Datatypes.Some (Base (##0)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -521,16 +510,15 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> (projT1 args)) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x3 <- (if - ((let (x3, _) := xv in x3) =? 0) && - is_bounded_by_bool (let (x3, _) := xv in x3) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast r[0 ~> 0])%expr @ (##0)%expr, - #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x3)); + fv <- (if + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x3, _) := xv in x3) =? 0) + then + Datatypes.Some + (Base + (#(Z_cast r[0 ~> 0])%expr @ (##0)%expr, + #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -559,17 +547,15 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x3 <- (if - ((let (x3, _) := xv in x3) =? 0) && - is_bounded_by_bool - (let (x3, _) := xv in x3) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast r[0 ~> 0])%expr @ (##0)%expr, - #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x3)); + fv <- (if + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x3, _) := xv in x3) =? 0) + then + Datatypes.Some + (Base + (#(Z_cast r[0 ~> 0])%expr @ (##0)%expr, + #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -603,25 +589,23 @@ 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 s ℤ; - fv <- (x5 <- (if - ((let (x5, _) := xv0 in x5) =? 1) && - (ZRange.normalize args3 <=? - r[0 ~> (let (x5, _) := xv in x5) - - 1])%zrange && - is_bounded_by_bool - (let (x5, _) := xv in x5) - (ZRange.normalize args2) && - is_bounded_by_bool - (let (x5, _) := xv0 in x5) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast args3)%expr @ - v (Compile.reflect x2), - #(Z_cast r[0 ~> 0])%expr @ - (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + is_bounded_by_bool 1 + (ZRange.normalize args0) && + is_bounded_by_bool + (let (x5, _) := xv in x5) + (ZRange.normalize args2) && + (ZRange.normalize args3 <=? + r[0 ~> (let (x5, _) := xv in x5) - 1])%zrange && + ((let (x5, _) := xv0 in x5) =? 1) + then + Datatypes.Some + (Base + (#(Z_cast args3)%expr @ + v (Compile.reflect x2), + #(Z_cast r[0 ~> 0])%expr @ + (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -651,25 +635,23 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s1 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x5 <- (if - ((let (x5, _) := xv0 in x5) =? 1) && - (ZRange.normalize args0 <=? - r[0 ~> (let (x5, _) := xv in x5) - - 1])%zrange && - is_bounded_by_bool - (let (x5, _) := xv in x5) - (ZRange.normalize args2) && - is_bounded_by_bool - (let (x5, _) := xv0 in x5) - (ZRange.normalize args3) - then - Datatypes.Some - (#(Z_cast args0)%expr @ - v (Compile.reflect x4), - #(Z_cast r[0 ~> 0])%expr @ - (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + is_bounded_by_bool 1 + (ZRange.normalize args3) && + is_bounded_by_bool + (let (x5, _) := xv in x5) + (ZRange.normalize args2) && + (ZRange.normalize args0 <=? + r[0 ~> (let (x5, _) := xv in x5) - 1])%zrange && + ((let (x5, _) := xv0 in x5) =? 1) + then + Datatypes.Some + (Base + (#(Z_cast args0)%expr @ + v (Compile.reflect x4), + #(Z_cast r[0 ~> 0])%expr @ + (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -734,28 +716,35 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x5 <- (if - is_bounded_by_bool - (let (x5, _) := xv in x5) - (ZRange.normalize args4) && - is_bounded_by_bool - (let (x5, _) := xv0 in x5) - (ZRange.normalize args2) && - is_bounded_by_bool - (let (x5, _) := xv1 in x5) - (ZRange.normalize args0) - then - Datatypes.Some - (let - '(a1, b1)%zrange := - Z.add_get_carry_full - (let (x5, _) := xv in x5) - (let (x5, _) := xv0 in x5) - (let (x5, _) := xv1 in x5) - in - ((##a1)%expr, (##b1)%expr)%expr_pat) - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + is_bounded_by_bool + (let (x5, _) := xv in x5) + (ZRange.normalize args4) && + is_bounded_by_bool + (let (x5, _) := xv0 in x5) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x5, _) := xv1 in x5) + (ZRange.normalize args0) + then + Datatypes.Some + (Base + ((##(Datatypes.fst + (Z.add_get_carry_full + (let (x5, _) := xv in + x5) + (let (x5, _) := xv0 in + x5) + (let (x5, _) := xv1 in + x5))))%expr, + (##(Datatypes.snd + (Z.add_get_carry_full + (let (x5, _) := xv in x5) + (let (x5, _) := xv0 in + x5) + (let (x5, _) := xv1 in + x5))))%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -784,25 +773,22 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); v <- type.try_make_transport_cps s1 ℤ; - fv <- (x5 <- (if - ((let (x5, _) := xv0 in x5) =? 0) && - (ZRange.normalize args <=? - r[0 ~> (let (x5, _) := xv in x5) - - 1])%zrange && - is_bounded_by_bool - (let (x5, _) := xv0 in x5) - (ZRange.normalize args1) && - is_bounded_by_bool - (let (x5, _) := xv in x5) - (ZRange.normalize args3) - then - Datatypes.Some - (#(Z_cast args)%expr @ - v (Compile.reflect x4), - #(Z_cast r[0 ~> 0])%expr @ - (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + is_bounded_by_bool + (let (x5, _) := xv in x5) + (ZRange.normalize args3) && + is_bounded_by_bool 0 + (ZRange.normalize args1) && + (ZRange.normalize args <=? + r[0 ~> (let (x5, _) := xv in x5) - 1])%zrange && + ((let (x5, _) := xv0 in x5) =? 0) + then + Datatypes.Some + (Base + (#(Z_cast args)%expr @ + v (Compile.reflect x4), + #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -838,23 +824,20 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s0 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x5 <- (if - ((let (x5, _) := xv0 in x5) =? 0) && - (ZRange.normalize args1 <=? - r[0 ~> (let (x5, _) := xv in x5) - 1])%zrange && - is_bounded_by_bool - (let (x5, _) := xv0 in x5) - (ZRange.normalize args0) && - is_bounded_by_bool - (let (x5, _) := xv in x5) - (ZRange.normalize args3) - then - Datatypes.Some - (#(Z_cast args1)%expr @ - v (Compile.reflect x3), - #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x5)); + fv <- (if + is_bounded_by_bool (let (x5, _) := xv in x5) + (ZRange.normalize args3) && + is_bounded_by_bool 0 (ZRange.normalize args0) && + (ZRange.normalize args1 <=? + r[0 ~> (let (x5, _) := xv in x5) - 1])%zrange && + ((let (x5, _) := xv0 in x5) =? 0) + then + Datatypes.Some + (Base + (#(Z_cast args1)%expr @ + v (Compile.reflect x3), + #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -898,13 +881,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args) -> ℤ) -> ℤ)%ptype then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x3 <- (if - ((let (x3, _) := xv in x3) =? 0) && - is_bounded_by_bool (let (x3, _) := xv in x3) - (ZRange.normalize args0) - then Datatypes.Some (x0 + x1)%expr - else Datatypes.None); - Datatypes.Some (Base x3)); + fv <- (if + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x3, _) := xv in x3) =? 0) + then Datatypes.Some (Base (x0 + x1)%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -961,36 +942,50 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args1); xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x7 <- (if - is_bounded_by_bool - (let (x7, _) := xv in x7) - (ZRange.normalize args6) && - is_bounded_by_bool - (let (x7, _) := xv0 in x7) - (ZRange.normalize args4) && - is_bounded_by_bool - (let (x7, _) := xv1 in x7) - (ZRange.normalize args2) && - is_bounded_by_bool - (let (x7, _) := xv2 in x7) - (ZRange.normalize args0) - then - Datatypes.Some - (let - '(a2, b2)%zrange := - Z.add_with_get_carry_full - (let (x7, _) := xv in - x7) - (let (x7, _) := xv0 in - x7) - (let (x7, _) := xv1 in - x7) - (let (x7, _) := xv2 in - x7) in - ((##a2)%expr, - (##b2)%expr)%expr_pat) - else Datatypes.None); - Datatypes.Some (Base x7)); + fv <- (if + is_bounded_by_bool + (let (x7, _) := xv in x7) + (ZRange.normalize args6) && + is_bounded_by_bool + (let (x7, _) := xv0 in x7) + (ZRange.normalize args4) && + is_bounded_by_bool + (let (x7, _) := xv1 in x7) + (ZRange.normalize args2) && + is_bounded_by_bool + (let (x7, _) := xv2 in x7) + (ZRange.normalize args0) + then + Datatypes.Some + (Base + ((##(Datatypes.fst + (Z.add_with_get_carry_full + (let (x7, _) := + xv in + x7) + (let (x7, _) := + xv0 in + x7) + (let (x7, _) := + xv1 in + x7) + (let (x7, _) := + xv2 in + x7))))%expr, + (##(Datatypes.snd + (Z.add_with_get_carry_full + (let (x7, _) := xv in + x7) + (let (x7, _) := + xv0 in + x7) + (let (x7, _) := + xv1 in + x7) + (let (x7, _) := + xv2 in + x7))))%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1026,29 +1021,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args0); v <- type.try_make_transport_cps s2 ℤ; - fv <- (x7 <- (if - ((let (x7, _) := xv0 in x7) =? 0) && - ((let (x7, _) := xv1 in x7) =? 0) && - (ZRange.normalize args <=? - r[0 ~> (let (x7, _) := xv in x7) - - 1])%zrange && - is_bounded_by_bool - (let (x7, _) := xv in x7) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x7, _) := xv0 in x7) - (ZRange.normalize args3) && - is_bounded_by_bool - (let (x7, _) := xv1 in x7) - (ZRange.normalize args1) - then - Datatypes.Some - (#(Z_cast args)%expr @ - v (Compile.reflect x6), - #(Z_cast r[0 ~> 0])%expr @ - (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x7)); + fv <- (if + is_bounded_by_bool + (let (x7, _) := xv in x7) + (ZRange.normalize args5) && + is_bounded_by_bool 0 + (ZRange.normalize args3) && + is_bounded_by_bool 0 + (ZRange.normalize args1) && + (ZRange.normalize args <=? + r[0 ~> (let (x7, _) := xv in x7) - 1])%zrange && + ((let (x7, _) := xv0 in x7) =? 0) && + ((let (x7, _) := xv1 in x7) =? 0) + then + Datatypes.Some + (Base + (#(Z_cast args)%expr @ + v (Compile.reflect x6), + #(Z_cast r[0 ~> 0])%expr @ + (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1091,29 +1083,25 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s1 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x7 <- (if - ((let (x7, _) := xv0 in x7) =? 0) && - ((let (x7, _) := xv1 in x7) =? 0) && - (ZRange.normalize args1 <=? - r[0 ~> (let (x7, _) := xv in x7) - - 1])%zrange && - is_bounded_by_bool - (let (x7, _) := xv in x7) - (ZRange.normalize args5) && - is_bounded_by_bool - (let (x7, _) := xv0 in x7) - (ZRange.normalize args3) && - is_bounded_by_bool - (let (x7, _) := xv1 in x7) - (ZRange.normalize args0) - then - Datatypes.Some - (#(Z_cast args1)%expr @ - v (Compile.reflect x5), - #(Z_cast r[0 ~> 0])%expr @ - (##0)%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x7)); + fv <- (if + is_bounded_by_bool + (let (x7, _) := xv in x7) + (ZRange.normalize args5) && + is_bounded_by_bool 0 + (ZRange.normalize args3) && + is_bounded_by_bool 0 + (ZRange.normalize args0) && + (ZRange.normalize args1 <=? + r[0 ~> (let (x7, _) := xv in x7) - 1])%zrange && + ((let (x7, _) := xv0 in x7) =? 0) && + ((let (x7, _) := xv1 in x7) =? 0) + then + Datatypes.Some + (Base + (#(Z_cast args1)%expr @ + v (Compile.reflect x5), + #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1168,12 +1156,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 lower range =? upper range - then - Datatypes.Some - (#(Z_cast range)%expr @ (##(lower range))%expr)%expr_pat - else Datatypes.None); - Datatypes.Some (Base x0)); + fv <- (if lower range =? upper range + then + Datatypes.Some + (Base + (#(Z_cast range)%expr @ (##(lower range))%expr)%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1187,15 +1175,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with if type.type_beq base.type base.type.type_beq ℤ s then v <- type.try_make_transport_cps s ℤ; - fv <- (x1 <- (if - (ZRange.normalize args <=? - ZRange.normalize range)%zrange - then - Datatypes.Some - (#(Z_cast args)%expr @ - v (Compile.reflect x0))%expr_pat - else Datatypes.None); - Datatypes.Some (Base x1)); + fv <- (if + (ZRange.normalize args <=? ZRange.normalize range)%zrange + then + Datatypes.Some + (Base + (#(Z_cast args)%expr @ v (Compile.reflect x0))%expr_pat) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None @@ -1324,21 +1310,21 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 (Compile.reflect x0) @ (#(Z_cast args)%expr @ v0 (Compile.reflect x5))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + - Datatypes.snd range))%expr @ $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1408,21 +1394,21 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 (Compile.reflect x1) @ (#(Z_cast args)%expr @ v1 (Compile.reflect x5))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + - Datatypes.snd range))%expr @ $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1476,9 +1462,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args); v0 <- type.try_make_transport_cps s ℤ; fv <- (if - ((let (x4, _) := xv in x4) <? 0) && is_bounded_by_bool (let (x4, _) := xv in x4) - (ZRange.normalize args0) + (ZRange.normalize args0) && + ((let (x4, _) := xv in x4) <? 0) then Datatypes.Some (UnderLet @@ -1490,21 +1476,21 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 (Compile.reflect x0) @ (#(Z_cast (- args0))%expr @ (##(- (let (x4, _) := xv in x4))%Z)%expr)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v1 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v1)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + - Datatypes.snd range))%expr @ $v1)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1537,9 +1523,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if - ((let (x4, _) := xv in x4) <? 0) && is_bounded_by_bool (let (x4, _) := xv in x4) - (ZRange.normalize args0) + (ZRange.normalize args0) && + ((let (x4, _) := xv in x4) <? 0) then Datatypes.Some (UnderLet @@ -1551,21 +1537,21 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 (Compile.reflect x1) @ (#(Z_cast (- args0))%expr @ (##(- (let (x4, _) := xv in x4))%Z)%expr)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v1 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v1)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + - Datatypes.snd range))%expr @ $v1)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1696,12 +1682,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s6 ℤ; v1 <- type.try_make_transport_cps s ℤ; fv <- (if - ((let (x8, _) := xv in x8) =? 0) && + is_bounded_by_bool 0 + (ZRange.normalize args3) && (ZRange.normalize args <=? - ZRange.normalize args1)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args3) + ((let (x8, _) := xv in x8) =? 0) then Datatypes.Some (UnderLet @@ -1713,14 +1698,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 (Compile.reflect x0) @ (#(Z_cast args)%expr @ v0 (Compile.reflect x7))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast @@ -1729,7 +1714,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1761,11 +1746,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- type.try_make_transport_cps s ℤ; fv <- (if ((let (x8, _) := xv in x8) <? 0) && - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange && is_bounded_by_bool (let (x8, _) := xv in x8) - (ZRange.normalize args3) + (ZRange.normalize args3) && + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange then Datatypes.Some (UnderLet @@ -1779,14 +1764,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 (Compile.reflect x0) @ (#(Z_cast args)%expr @ v0 (Compile.reflect x7))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -1794,7 +1779,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1863,12 +1848,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s6 ℤ; fv <- (if - ((let (x8, _) := xv in x8) =? 0) && + is_bounded_by_bool 0 + (ZRange.normalize args3) && (ZRange.normalize args <=? - ZRange.normalize args1)%zrange && - is_bounded_by_bool - (let (x8, _) := xv in x8) - (ZRange.normalize args3) + ((let (x8, _) := xv in x8) =? 0) then Datatypes.Some (UnderLet @@ -1880,14 +1864,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 (Compile.reflect x1) @ (#(Z_cast args)%expr @ v1 (Compile.reflect x7))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast @@ -1896,7 +1880,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1928,11 +1912,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- type.try_make_transport_cps s6 ℤ; fv <- (if ((let (x8, _) := xv in x8) <? 0) && - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange && is_bounded_by_bool (let (x8, _) := xv in x8) - (ZRange.normalize args3) + (ZRange.normalize args3) && + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange then Datatypes.Some (UnderLet @@ -1946,14 +1930,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 (Compile.reflect x1) @ (#(Z_cast args)%expr @ v1 (Compile.reflect x7))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -1961,7 +1945,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2051,14 +2035,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 (Compile.reflect x0) @ (#(Z_cast (- args0))%expr @ (##(- (let (x6, _) := xv0 in x6))%Z)%expr)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v1 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v1)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -2066,7 +2050,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v1)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2129,14 +2113,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 (Compile.reflect x1) @ (#(Z_cast (- args0))%expr @ (##(- (let (x6, _) := xv0 in x6))%Z)%expr)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v1 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v1)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -2144,7 +2128,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v1)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2177,9 +2161,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s ℤ; fv <- (if - ((let (x5, _) := xv in x5) =? 0) && - is_bounded_by_bool (let (x5, _) := xv in x5) - (ZRange.normalize args0) + is_bounded_by_bool 0 (ZRange.normalize args0) && + ((let (x5, _) := xv in x5) =? 0) then Datatypes.Some (UnderLet @@ -2188,14 +2171,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v (Compile.reflect x3) @ v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ - (#(Z_cast2 range)%expr @ ($vc)%expr)), + (#(Z_cast2 range)%expr @ ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (#(snd)%expr @ - (#(Z_cast2 range)%expr @ ($vc)%expr)))%expr_pat)) + (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2249,14 +2232,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v2 (Compile.reflect x0) @ (#(Z_cast args)%expr @ v1 (Compile.reflect x9))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v3 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v3)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -2264,7 +2247,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v3)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2350,14 +2333,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 (Compile.reflect x1) @ (#(Z_cast args)%expr @ v2 (Compile.reflect x9))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v3 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v3)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -2365,7 +2348,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v3)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2433,11 +2416,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- type.try_make_transport_cps s ℤ; fv <- (if ((let (x8, _) := xv in x8) <=? 0) && - (ZRange.normalize args1 <=? - - ZRange.normalize args3)%zrange && is_bounded_by_bool (let (x8, _) := xv in x8) - (ZRange.normalize args0) + (ZRange.normalize args0) && + (ZRange.normalize args1 <=? + - ZRange.normalize args3)%zrange then Datatypes.Some (UnderLet @@ -2451,14 +2434,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 (Compile.reflect x0) @ (#(Z_cast (- args0))%expr @ (##(- (let (x8, _) := xv in x8))%Z)%expr)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -2466,7 +2449,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2507,11 +2490,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args); fv <- (if ((let (x8, _) := xv in x8) <=? 0) && - (ZRange.normalize args1 <=? - - ZRange.normalize args3)%zrange && is_bounded_by_bool (let (x8, _) := xv in x8) - (ZRange.normalize args0) + (ZRange.normalize args0) && + (ZRange.normalize args1 <=? + - ZRange.normalize args3)%zrange then Datatypes.Some (UnderLet @@ -2525,14 +2508,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 (Compile.reflect x1) @ (#(Z_cast (- args0))%expr @ (##(- (let (x8, _) := xv in x8))%Z)%expr)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (fun v2 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), + ($v2)%expr)), #(Z_cast (Datatypes.snd range))%expr @ (- (#(Z_cast (- Datatypes.snd range))%expr @ @@ -2540,7 +2523,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) + $v2)))%expr_pat)%expr)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2604,21 +2587,20 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if - ((let (x8, _) := xv0 in x8) =? 0) && - ((let (x8, _) := xv1 in x8) =? 0) && + is_bounded_by_bool 0 + (ZRange.normalize args2) && + is_bounded_by_bool 0 + (ZRange.normalize args0) && (ZRange.normalize args5 <=? r[0 ~> (let (x8, _) := xv in x8) - 1])%zrange && is_bounded_by_bool 0 - (Datatypes.snd range) && + (ZRange.normalize + (Datatypes.snd range)) && is_bounded_by_bool (let (x8, _) := xv in x8) (ZRange.normalize args4) && - is_bounded_by_bool - (let (x8, _) := xv0 in x8) - (ZRange.normalize args2) && - is_bounded_by_bool - (let (x8, _) := xv1 in x8) - (ZRange.normalize args0) + ((let (x8, _) := xv0 in x8) =? 0) && + ((let (x8, _) := xv1 in x8) =? 0) then Datatypes.Some (UnderLet @@ -2629,16 +2611,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast args5)%expr @ v (Compile.reflect x4)) @ (#(Z_cast args2)%expr @ - (##(let (x8, _) := xv0 in x8))%expr) @ + (##0)%expr) @ (#(Z_cast args0)%expr @ - (##(let (x8, _) := xv1 in x8))%expr)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => + (##0)%expr)))%expr_pat + (fun v0 : var (ℤ * ℤ)%etype => Base (#(Z_cast (Datatypes.fst range))%expr @ (#(fst)%expr @ (#(Z_cast2 range)%expr @ - ($vc)%expr)), + ($v0)%expr)), #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat)) else Datatypes.None); 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 diff --git a/src/nbe_rewrite_head.out b/src/nbe_rewrite_head.out index a6b62f776..9c3922844 100644 --- a/src/nbe_rewrite_head.out +++ b/src/nbe_rewrite_head.out @@ -356,9 +356,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v3 <- base.try_make_transport_cps b7 T; v4 <- base.try_make_transport_cps T T; Datatypes.Some - (fv1 <-- x'4 (x'3 (x'2 (x'1 (x'0 (x' x))))) - (v1 (v (Compile.reflect x2))) - (v2 (v0 (Compile.reflect x1))); + (fv1 <-- (e <-- x'4 (x'3 (x'2 (x'1 (x'0 (x' x))))) + (v1 (v (Compile.reflect x2))) + (v2 (v0 (Compile.reflect x1))); + Base e); Base (v4 (v3 fv1)))%under_lets else Datatypes.None | Datatypes.None => Datatypes.None @@ -383,6 +384,43 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun (x x0 : expr unit -> UnderLets (expr T)) (x1 : expr bool) => ((match x1 with | @expr.Ident _ _ _ t idc => + (args <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted + (((((unit -> '1%pbtype) -> + (unit -> '1%pbtype) -> bool -> '1%pbtype) -> + unit -> '1%pbtype) -> unit -> '1%pbtype) -> bool)%ptype + (((((unit -> T) -> (unit -> T) -> bool -> T) -> unit -> T) -> + unit -> T) -> (projT1 args))%ptype + with + | Datatypes.Some + (_, _, (_, _, (_, _)), (_, _), (_, b8), _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((((unit -> b8) -> (unit -> b8) -> bool -> b8) -> + unit -> b8) -> unit -> b8) -> bool)%ptype + (((((unit -> T) -> (unit -> T) -> bool -> T) -> unit -> T) -> + unit -> T) -> (projT1 args))%ptype + then + _ <- ident.unify pattern.ident.bool_rect bool_rect; + x' <- base.try_make_transport_cps T b8; + _ <- base.try_make_transport_cps T b8; + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + x'1 <- base.try_make_transport_cps b8 b8; + _ <- base.try_make_transport_cps b8 b8; + v <- base.try_make_transport_cps b8 T; + v0 <- base.try_make_transport_cps T T; + fv0 <- (if let (x2, _) := xv in x2 + then + Datatypes.Some + (e <-- x'1 (x' x) (##tt)%expr; + Base e)%under_lets + else Datatypes.None); + Datatypes.Some (fv1 <-- fv0; + Base (v0 (v fv1)))%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end);; args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted @@ -402,18 +440,21 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with unit -> T) -> (projT1 args))%ptype then _ <- ident.unify pattern.ident.bool_rect bool_rect; - x' <- base.try_make_transport_cps T b8; + _ <- base.try_make_transport_cps T b8; x'0 <- base.try_make_transport_cps T b8; xv <- ident.unify pattern.ident.Literal ##(projT2 args); - x'1 <- base.try_make_transport_cps b8 b8; + _ <- base.try_make_transport_cps b8 b8; x'2 <- base.try_make_transport_cps b8 b8; v <- base.try_make_transport_cps b8 T; v0 <- base.try_make_transport_cps T T; - Datatypes.Some - (fv0 <-- (if let (x2, _) := xv in x2 - then x'1 (x' x) (##tt)%expr - else x'2 (x'0 x0) (##tt)%expr); - Base (v0 (v fv0)))%under_lets + fv0 <- (if let (x2, _) := xv in x2 + then Datatypes.None + else + Datatypes.Some + (e <-- x'2 (x'0 x0) (##tt)%expr; + Base e)%under_lets); + Datatypes.Some (fv1 <-- fv0; + Base (v0 (v fv1)))%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -652,7 +693,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- base.try_make_transport_cps b10 P; v0 <- base.try_make_transport_cps P P; Datatypes.Some - (fv0 <-- x'3 (x' x) (##tt)%expr; + (fv0 <-- (e <-- x'3 (x' x) (##tt)%expr; + Base e); Base (v0 (v fv0)))%under_lets else Datatypes.None | Datatypes.None => Datatypes.None @@ -704,9 +746,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v3 <- base.try_make_transport_cps b10 P; v4 <- base.try_make_transport_cps P P; Datatypes.Some - (fv1 <-- x'6 (x'5 (x'4 (x'2 (x'1 (x'0 x0))))) - (v1 (v (Compile.reflect x3))) - (v2 (v0 (Compile.reflect x2))); + (fv1 <-- (e <-- x'6 (x'5 (x'4 (x'2 (x'1 (x'0 x0))))) + (v1 (v (Compile.reflect x3))) + (v2 (v0 (Compile.reflect x2))); + Base e); Base (v4 (v3 fv1)))%under_lets else Datatypes.None | Datatypes.None => Datatypes.None @@ -1769,8 +1812,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); Datatypes.Some (Base - (##(Z.shiftr (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) + (##((let (x1, _) := xv in x1) >> + (let (x1, _) := xv0 in x1))%Z)%expr) else Datatypes.None | Datatypes.None => Datatypes.None end @@ -1801,8 +1844,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); Datatypes.Some (Base - (##(Z.shiftl (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) + (##((let (x1, _) := xv in x1) << + (let (x1, _) := xv0 in x1))%Z)%expr) else Datatypes.None | Datatypes.None => Datatypes.None end @@ -1833,8 +1876,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); Datatypes.Some (Base - (##(Z.land (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) + (##((let (x1, _) := xv in x1) &' + (let (x1, _) := xv0 in x1))%Z)%expr) else Datatypes.None | Datatypes.None => Datatypes.None end diff --git a/src/strip_literal_casts_rewrite_head.out b/src/strip_literal_casts_rewrite_head.out index 9880ce10f..916f44c85 100644 --- a/src/strip_literal_casts_rewrite_head.out +++ b/src/strip_literal_casts_rewrite_head.out @@ -175,14 +175,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with if type.type_beq base.type base.type.type_beq ℤ (projT1 args) then xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x0 <- (if - is_bounded_by_bool (let (x0, _) := xv in x0) - (ZRange.normalize range) - then - Datatypes.Some - (##(let (x0, _) := xv in x0))%expr - else Datatypes.None); - Datatypes.Some (Base x0)); + fv <- (if + is_bounded_by_bool (let (x0, _) := xv in x0) + (ZRange.normalize range) + then + Datatypes.Some + (Base (##(let (x0, _) := xv in x0))%expr) + else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets else Datatypes.None |