diff options
Diffstat (limited to 'src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out')
| -rw-r--r-- | src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out | 4364 |
1 files changed, 2975 insertions, 1389 deletions
diff --git a/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out b/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out index 7abfcbfbf..f3c6cd79f 100644 --- a/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out +++ b/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out @@ -735,12 +735,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; fv <- (x10 <- (if ((let (x10, _) := xv in x10) =? @@ -831,10 +829,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s4 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -930,10 +926,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s4 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1163,14 +1157,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> (projT1 args0) -> s8)%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; fv <- (x10 <- (if ((let (x10, _) := xv in x10) =? @@ -1259,12 +1251,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1358,12 +1348,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1578,14 +1566,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> (projT1 args0) -> s8)%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; fv <- (x10 <- (if ((let (x10, _) := xv0 in x10) =? @@ -1662,12 +1648,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1749,12 +1733,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1942,8 +1924,7 @@ 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 s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal @@ -2008,12 +1989,10 @@ 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 s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; fv <- (x8 <- (if ((let (x8, _) := xv in x8) =? 2 @@ -2081,10 +2060,8 @@ 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 s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x8 <- (if @@ -2144,12 +2121,9 @@ 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 s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; - v1 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; + v1 <- type.try_make_transport_cps s7 ℤ; fv <- (x9 <- (if ((let (x9, _) := xv in x9) =? 2 @@ -2235,8 +2209,7 @@ 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 s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal @@ -2295,12 +2268,10 @@ 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 s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; fv <- (x8 <- (if ((let (x8, _) := xv in x8) =? 1) && @@ -2362,10 +2333,8 @@ 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 s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x8 <- (if @@ -2419,12 +2388,9 @@ 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 s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; - v1 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; + v1 <- type.try_make_transport_cps s7 ℤ; fv <- (x9 <- (if ((let (x9, _) := xv in x9) =? 1) && @@ -2499,8 +2465,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((s5 -> (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal @@ -2559,14 +2524,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((s5 -> (projT1 args1)) -> (projT1 args0)) -> s6)%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; fv <- (x8 <- (if ((let (x8, _) := xv in x8) =? 1) && @@ -2626,12 +2589,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((s5 -> (projT1 args1)) -> s6) -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x8 <- (if @@ -2683,14 +2644,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((s5 -> (projT1 args1)) -> s6) -> s7)%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); - v0 <- type.try_make_transport_cps s6 - ℤ; - v1 <- type.try_make_transport_cps s7 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; + v1 <- type.try_make_transport_cps s7 ℤ; fv <- (x9 <- (if ((let (x9, _) := xv in x9) =? 1) && @@ -3167,86 +3125,115 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x3 with | (@expr.Ident _ _ _ t3 idc3 @ x5 @ x4)%expr_pat => match x5 with - | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t4 idc4) - x6 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x4 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Literal; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype option - (fun x7 : option => x7) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x10 : option => x10) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s8 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x7 <- (let - '(r1, r2)%zrange := - range in - fun (s6 xx : Z) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s6 =? 2 ^ Z.log2 s6) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s6 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add - (Z.log2 s6) - offset)%expr @ - ((##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x7, _) := xv in - x7) - (let (x7, _) := xv0 in - x7) args2 args0 - (v (Compile.reflect x6)) - (let (x7, _) := xv1 in - x7); - Some (Base x7)); + fv <- (x10 <- (let + '(r1, r2)%zrange := + range in + fun (s9 xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s9 =? 2 ^ Z.log2 s9) && + (ZRange.normalize ry << + 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 ~> s9 - 1])%zrange && + (mask =? + Z.ones + (Z.log2 s9 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add + (Z.log2 s9) + offset)%expr @ + ((##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x10, _) := xv in + x10) + (let (x10, _) := + xv0 in + x10) args5 args3 + args1 + (v + (Compile.reflect x9)) + (let (x10, _) := + xv1 in + x10) + (let (x10, _) := + xv2 in + x10); + Some (Base x10)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -3254,10 +3241,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s5 _ ($_)%expr _ | @expr.App _ _ - _ s5 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s5 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x5 with @@ -3300,8 +3338,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -3413,87 +3450,116 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x3 with | (@expr.Ident _ _ _ t3 idc3 @ x5 @ x4)%expr_pat => match x5 with - | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t4 idc4) - x6 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x4 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Literal; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> s5 -> (projT1 args)) -> - (projT1 args2))%ptype option - (fun x7 : option => x7) + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s8 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype + option (fun x10 : option => x10) with - | Some (_, (_, _), _)%zrange => + | Some (_, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> - s5 -> (projT1 args)) -> - (projT1 args2))%ptype + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s8 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s5 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args); + ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args2); - fv <- (x7 <- (let - '(r1, r2)%zrange := - range in - fun (s6 : Z) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset xx : Z) => - if - (s6 =? 2 ^ Z.log2 s6) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s6 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add - (Z.log2 s6) - offset)%expr @ - ((##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x7, _) := xv in - x7) args3 args0 - (v (Compile.reflect x6)) - (let (x7, _) := xv0 in - x7) - (let (x7, _) := xv1 in - x7); - Some (Base x7)); + ##(projT2 args); + xv2 <- ident.unify + pattern.ident.Literal + ##(projT2 args5); + fv <- (x10 <- (let + '(r1, r2)%zrange := + range in + fun (s9 : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset xx : Z) + => + if + (s9 =? 2 ^ Z.log2 s9) && + (ZRange.normalize ry << + 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 ~> s9 - 1])%zrange && + (mask =? + Z.ones + (Z.log2 s9 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add + (Z.log2 s9) + offset)%expr @ + ((##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x10, _) := xv in + x10) args6 args3 + args1 + (v + (Compile.reflect x9)) + (let (x10, _) := + xv0 in + x10) + (let (x10, _) := + xv1 in + x10) + (let (x10, _) := + xv2 in + x10); + Some (Base x10)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -3501,10 +3567,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s5 _ ($_)%expr _ | @expr.App _ _ - _ s5 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s5 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x5 with @@ -3545,8 +3662,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -3652,178 +3768,392 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | @expr.App _ _ _ s3 _ (@expr.Ident _ _ _ t2 idc2) x4 => match x4 with - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Ident _ _ _ - t5 idc5)%expr_pat => - args <- invert_bind_args idc5 Raw.ident.Literal; - args0 <- invert_bind_args idc4 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Ident _ _ _ t8 idc8)%expr_pat => + args <- invert_bind_args idc8 Raw.ident.Literal; + args0 <- invert_bind_args idc7 Raw.ident.Literal; + args1 <- invert_bind_args idc6 Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 Raw.ident.Literal; + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> s6 -> (projT1 args))%ptype - option (fun x8 : option => x8) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> (projT1 args))%ptype + option (fun x11 : option => x11) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> - s6 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); v <- type.try_make_transport_cps s2 ℤ; - v0 <- type.try_make_transport_cps s6 ℤ; + v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := range in - fun (s7 : Z) (rx : zrange) - (x8 : expr ℤ) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s7) - offset)%expr @ - (#(Z_cast rx)%expr @ x8, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x8, _) := xv in x8) args3 - (v (Compile.reflect x3)) args2 - args0 (v0 (Compile.reflect x7)) - (let (x8, _) := xv0 in x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := range in + fun (s10 : Z) (rx : zrange) + (x11 : expr ℤ) + (rshiftl rland ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s10 =? 2 ^ Z.log2 s10) && + (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 ~> s10 - 1])%zrange && + (mask =? + Z.ones (Z.log2 s10 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add (Z.log2 s10) + offset)%expr @ + (#(Z_cast rx)%expr @ x11, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x11, _) := xv in x11) + args6 (v (Compile.reflect x3)) + args5 args3 args1 + (v0 (Compile.reflect x10)) + (let (x11, _) := xv0 in x11) + (let (x11, _) := xv1 in x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Abs _ _ _ _ _ + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Abs _ _ _ + _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.LetIn _ _ + _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ _ @ + _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ _ + _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.LetIn _ _ _ _ - _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => None + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ + _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t3 idc3 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; match x3 with - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Ident _ _ _ - t5 idc5)%expr_pat => - args <- invert_bind_args idc5 Raw.ident.Literal; - args0 <- invert_bind_args idc4 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Ident _ _ _ t8 idc8)%expr_pat => + args <- invert_bind_args idc8 Raw.ident.Literal; + args0 <- invert_bind_args idc7 Raw.ident.Literal; + args1 <- invert_bind_args idc6 Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 Raw.ident.Literal; + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> s6 -> (projT1 args)) -> s3)%ptype - option (fun x8 : option => x8) + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s9 -> (projT1 args0)) -> (projT1 args)) -> + s3)%ptype option (fun x11 : option => x11) with - | Some (_, (_, _), _)%zrange => + | Some (_, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> s6 -> (projT1 args)) -> + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s9 -> (projT1 args0)) -> (projT1 args)) -> s3)%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s6 ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); v0 <- type.try_make_transport_cps s3 ℤ; - fv <- (x8 <- (let - '(r1, r2)%zrange := range in - fun (s7 : Z) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) - (rx : zrange) (x8 : expr ℤ) - => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s7) - offset)%expr @ - (#(Z_cast rx)%expr @ x8, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x8, _) := xv in x8) args3 - args0 (v (Compile.reflect x7)) - (let (x8, _) := xv0 in x8) - args2 (v0 (Compile.reflect x4)); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := range in + fun (s10 : Z) + (rshiftl rland ry : zrange) + (y : expr ℤ) + (mask offset : Z) + (rx : zrange) (x11 : expr ℤ) + => + if + (s10 =? 2 ^ Z.log2 s10) && + (ZRange.normalize ry << + 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 ~> s10 - 1])%zrange && + (mask =? + Z.ones (Z.log2 s10 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add (Z.log2 s10) + offset)%expr @ + (#(Z_cast rx)%expr @ x11, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x11, _) := xv in x11) + args6 args3 args1 + (v (Compile.reflect x10)) + (let (x11, _) := xv0 in x11) + (let (x11, _) := xv1 in x11) + args5 + (v0 (Compile.reflect x4)); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Abs _ _ _ _ _ + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Abs _ _ _ + _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.LetIn _ _ + _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ _ @ + _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ _ + _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.LetIn _ _ _ _ - _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => None + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ + _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t3 idc3 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None @@ -4073,86 +4403,115 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x3 with | (@expr.Ident _ _ _ t3 idc3 @ x5 @ x4)%expr_pat => match x5 with - | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t4 idc4) - x6 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x4 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Literal; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype option - (fun x7 : option => x7) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x10 : option => x10) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s8 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x7 <- (let - '(r1, r2)%zrange := - range in - fun (s6 xx : Z) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s6 =? 2 ^ Z.log2 s6) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s6 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_sub - (Z.log2 s6) - offset)%expr @ - ((##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x7, _) := xv in - x7) - (let (x7, _) := xv0 in - x7) args2 args0 - (v (Compile.reflect x6)) - (let (x7, _) := xv1 in - x7); - Some (Base x7)); + fv <- (x10 <- (let + '(r1, r2)%zrange := + range in + fun (s9 xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s9 =? 2 ^ Z.log2 s9) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s9 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s9 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_sub + (Z.log2 s9) + offset)%expr @ + ((##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x10, _) := xv in + x10) + (let (x10, _) := + xv0 in + x10) args5 args3 + args1 + (v + (Compile.reflect x9)) + (let (x10, _) := + xv1 in + x10) + (let (x10, _) := + xv2 in + x10); + Some (Base x10)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -4160,10 +4519,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s5 _ ($_)%expr _ | @expr.App _ _ - _ s5 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s5 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x5 with @@ -4206,8 +4616,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -4366,89 +4775,117 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t3 idc3 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ (@expr.Ident _ _ _ t4 idc4) - x7 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x5 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> - s6 -> (projT1 args))%ptype option - (fun x8 : option => x8) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x11 : option => x11) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> - s6 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s2 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 : Z) - (rx : zrange) - (x8 : expr ℤ) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_sub - (Z.log2 s7) - offset)%expr @ - (#(Z_cast rx)%expr @ - x8, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := xv in - x8) args3 - (v (Compile.reflect x3)) - args2 args0 - (v0 - (Compile.reflect x7)) - (let (x8, _) := xv0 in - x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun (s10 : Z) + (rx : zrange) + (x11 : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_sub + (Z.log2 s10) + offset)%expr @ + (#(Z_cast rx)%expr @ + x11, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := xv in + x11) args6 + (v + (Compile.reflect x3)) + args5 args3 args1 + (v0 + (Compile.reflect + x10)) + (let (x11, _) := + xv0 in + x11) + (let (x11, _) := + xv1 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -4456,10 +4893,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App _ _ - _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s6 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -4499,10 +4987,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s2 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -4633,107 +5119,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t4 idc4 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t5 idc5) x7 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x5 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype option - (fun x8 : option => x8) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x11 : option => x11) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s9 ℤ; xv2 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv3 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 cc xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s7 =? - 2 ^ Z.log2 s7) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s7) - offset)%expr @ - ((##cc)%expr, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := - xv in - x8) - (let (x8, _) := - xv0 in - x8) - (let (x8, _) := - xv1 in - x8) args2 args0 - (v - (Compile.reflect - x7)) - (let (x8, _) := - xv2 in - x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun + (s10 cc xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s10) + offset)%expr @ + ((##cc)%expr, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := + xv in + x11) + (let (x11, _) := + xv0 in + x11) + (let (x11, _) := + xv1 in + x11) args5 args3 + args1 + (v + (Compile.reflect + x10)) + (let (x11, _) := + xv2 in + x11) + (let (x11, _) := + xv3 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -4742,11 +5259,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App - _ _ _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s6 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -4797,8 +5368,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s6 ℤ; xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -4932,108 +5502,136 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t4 idc4 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t5 idc5) x7 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x5 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Literal; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s6 -> (projT1 args)) -> - (projT1 args2))%ptype option - (fun x8 : option => x8) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (s9 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype + option (fun x11 : option => x11) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> - s6 -> (projT1 args)) -> - (projT1 args2))%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> + ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> + (s9 -> (projT1 args0)) -> + (projT1 args)) -> + (projT1 args5))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s9 ℤ; xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); + ##(projT2 args0); xv2 <- ident.unify pattern.ident.Literal - ##(projT2 args2); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 cc : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset xx : Z) - => - if - (s7 =? - 2 ^ Z.log2 s7) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s7) - offset)%expr @ - ((##cc)%expr, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := - xv in - x8) - (let (x8, _) := - xv0 in - x8) args3 args0 - (v - (Compile.reflect - x7)) - (let (x8, _) := - xv1 in - x8) - (let (x8, _) := - xv2 in - x8); - Some (Base x8)); + ##(projT2 args); + xv3 <- ident.unify + pattern.ident.Literal + ##(projT2 args5); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun (s10 cc : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset + xx : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s10) + offset)%expr @ + ((##cc)%expr, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := + xv in + x11) + (let (x11, _) := + xv0 in + x11) args6 args3 + args1 + (v + (Compile.reflect + x10)) + (let (x11, _) := + xv1 in + x11) + (let (x11, _) := + xv2 in + x11) + (let (x11, _) := + xv3 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -5042,11 +5640,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App - _ _ _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s6 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -5094,8 +5746,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s6 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -5226,208 +5877,445 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @expr.App _ _ _ s4 _ (@expr.Ident _ _ _ t3 idc3) x5 => match x5 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> s3) -> - s7 -> (projT1 args))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> s3) -> + (s10 -> (projT1 args0)) -> (projT1 args))%ptype + option (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s3) -> s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := range in - fun (s8 cc : Z) - (rx : zrange) - (x9 : expr ℤ) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) - => - if - (s8 =? 2 ^ Z.log2 s8) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) offset)%expr @ - ((##cc)%expr, - #(Z_cast rx)%expr @ x9, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x9, _) := xv in x9) - (let (x9, _) := xv0 in x9) - args3 - (v (Compile.reflect x4)) - args2 args0 - (v0 (Compile.reflect x8)) - (let (x9, _) := xv1 in x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := range + in + fun (s11 cc : Z) + (rx : zrange) + (x12 : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s11 =? 2 ^ Z.log2 s11) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize rshiftl)%zrange && + (ZRange.normalize rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 s11) + offset)%expr @ + ((##cc)%expr, + #(Z_cast rx)%expr @ + x12, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x12, _) := xv in x12) + (let (x12, _) := xv0 in + x12) args6 + (v (Compile.reflect x4)) + args5 args3 args1 + (v0 (Compile.reflect x11)) + (let (x12, _) := xv1 in + x12) + (let (x12, _) := xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; match x4 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s7 -> (projT1 args)) -> s4)%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (s10 -> (projT1 args0)) -> (projT1 args)) -> + s4)%ptype option (fun x12 : option => x12) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s7 -> (projT1 args)) -> s4)%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (s10 -> (projT1 args0)) -> + (projT1 args)) -> s4)%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); - v0 <- type.try_make_transport_cps s4 - ℤ; - fv <- (x9 <- (let - '(r1, r2)%zrange := range in - fun (s8 cc : Z) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) - (rx : zrange) - (x9 : expr ℤ) => - if - (s8 =? 2 ^ Z.log2 s8) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) offset)%expr @ - ((##cc)%expr, - #(Z_cast rx)%expr @ x9, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x9, _) := xv in x9) - (let (x9, _) := xv0 in x9) - args3 args0 - (v (Compile.reflect x8)) - (let (x9, _) := xv1 in x9) - args2 - (v0 (Compile.reflect x5)); - Some (Base x9)); + v0 <- type.try_make_transport_cps s4 ℤ; + fv <- (x12 <- (let + '(r1, r2)%zrange := range + in + fun (s11 cc : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) + (rx : zrange) + (x12 : expr ℤ) => + if + (s11 =? 2 ^ Z.log2 s11) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize rshiftl)%zrange && + (ZRange.normalize rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 s11) + offset)%expr @ + ((##cc)%expr, + #(Z_cast rx)%expr @ + x12, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x12, _) := xv in x12) + (let (x12, _) := xv0 in + x12) args6 args3 args1 + (v (Compile.reflect x11)) + (let (x12, _) := xv1 in + x12) + (let (x12, _) := xv2 in + x12) args5 + (v0 (Compile.reflect x5)); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None @@ -5465,10 +6353,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args5); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x9 <- (let @@ -5570,12 +6456,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args5); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - v0 <- type.try_make_transport_cps s4 - ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; fv <- (x9 <- (let '(r1, r2)%zrange := range in fun (s8 cc : Z) @@ -5768,109 +6652,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args6); + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 : Z) - (rc : zrange) - (c : expr ℤ) - (xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) - offset)%expr @ - (#(Z_cast rc)%expr @ - c, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) args4 - (v - (Compile.reflect - x4)) - (let (x9, _) := - xv0 in - x9) args2 args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 : Z) + (rc : zrange) + (c : expr ℤ) + (xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s11) + offset)%expr @ + (#(Z_cast rc)%expr @ + c, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) args7 + (v + (Compile.reflect + x4)) + (let (x12, _) := + xv0 in + x12) args5 args3 + args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -5879,11 +6792,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -5927,13 +6894,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -6071,110 +7036,136 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Literal; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s7 -> (projT1 args)) -> - (projT1 args2))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype + option (fun x12 : option => x12) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s7 -> (projT1 args)) -> - (projT1 args2))%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> + ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args)) -> + (projT1 args5))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s10 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args); + ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args2); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 : Z) - (rc : zrange) - (c : expr ℤ) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset xx : Z) - => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) - offset)%expr @ - (#(Z_cast rc)%expr @ - c, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) args4 - (v - (Compile.reflect - x4)) args3 - args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv0 in - x9) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + ##(projT2 args); + xv2 <- ident.unify + pattern.ident.Literal + ##(projT2 args5); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 : Z) + (rc : zrange) + (c : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset + xx : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s11) + offset)%expr @ + (#(Z_cast rc)%expr @ + c, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) args7 + (v + (Compile.reflect + x4)) args6 + args3 args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv0 in + x12) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -6183,11 +7174,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -6231,10 +7276,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -6369,222 +7412,448 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t3 idc3) x6 => match x6 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype option - (fun x10 : option => x10) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> (projT1 args))%ptype + option (fun x13 : option => x13) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s11 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x10 <- (let + fv <- (x13 <- (let '(r1, r2)%zrange := range in - fun (s9 : Z) (rc : zrange) + fun (s12 : Z) + (rc : zrange) (c : expr ℤ) (rx : zrange) - (x10 : expr ℤ) - (rshiftl ry : zrange) + (x13 : expr ℤ) + (rshiftl rland + ry : zrange) (y : expr ℤ) - (offset : Z) => + (mask offset : Z) => if - (s9 =? 2 ^ Z.log2 s9) && + (s12 =? 2 ^ Z.log2 s12) && (ZRange.normalize ry << 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 ~> s9 - 1])%zrange + r[0 ~> s12 - 1])%zrange && + (mask =? + Z.ones + (Z.log2 s12 - offset)) then Some (#(Z_cast2 (r1, r2))%expr @ (#(fancy_addc - (Z.log2 s9) + (Z.log2 s12) offset)%expr @ (#(Z_cast rc)%expr @ c, #(Z_cast rx)%expr @ - x10, + x13, #(Z_cast ry)%expr @ y)))%expr_pat else None) - (let (x10, _) := xv in x10) - args4 + (let (x13, _) := xv in x13) + args7 (v (Compile.reflect x4)) - args3 + args6 (v0 (Compile.reflect x5)) - args2 args0 - (v1 (Compile.reflect x9)) - (let (x10, _) := xv0 in - x10); - Some (Base x10)); + args5 args3 args1 + (v1 (Compile.reflect x12)) + (let (x13, _) := xv0 in + x13) + (let (x13, _) := xv1 in + x13); + Some (Base x13)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; match x5 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s8 -> (projT1 args)) -> s5)%ptype option - (fun x10 : option => x10) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s11 -> (projT1 args0)) -> (projT1 args)) -> + s5)%ptype option (fun x13 : option => x13) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s8 -> (projT1 args)) -> s5)%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s11 -> (projT1 args0)) -> + (projT1 args)) -> s5)%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s11 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - v1 <- type.try_make_transport_cps s5 - ℤ; - fv <- (x10 <- (let + v1 <- type.try_make_transport_cps s5 ℤ; + fv <- (x13 <- (let '(r1, r2)%zrange := range in - fun (s9 : Z) (rc : zrange) + fun (s12 : Z) + (rc : zrange) (c : expr ℤ) - (rshiftl ry : zrange) + (rshiftl rland + ry : zrange) (y : expr ℤ) - (offset : Z) + (mask offset : Z) (rx : zrange) - (x10 : expr ℤ) => + (x13 : expr ℤ) => if - (s9 =? 2 ^ Z.log2 s9) && + (s12 =? 2 ^ Z.log2 s12) && (ZRange.normalize ry << ZRange.normalize (ZRange.constant offset) <=? ZRange.normalize rshiftl)%zrange && (ZRange.normalize rshiftl <=? - r[0 ~> s9 - 1])%zrange + r[0 ~> s12 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (mask =? + Z.ones + (Z.log2 s12 - offset)) then Some (#(Z_cast2 (r1, r2))%expr @ (#(fancy_addc - (Z.log2 s9) + (Z.log2 s12) offset)%expr @ (#(Z_cast rc)%expr @ c, #(Z_cast rx)%expr @ - x10, + x13, #(Z_cast ry)%expr @ y)))%expr_pat else None) - (let (x10, _) := xv in x10) - args4 + (let (x13, _) := xv in x13) + args7 (v (Compile.reflect x4)) - args3 args0 - (v0 (Compile.reflect x9)) - (let (x10, _) := xv0 in - x10) args2 + args6 args3 args1 + (v0 (Compile.reflect x12)) + (let (x13, _) := xv0 in + x13) + (let (x13, _) := xv1 in + x13) args5 (v1 (Compile.reflect x6)); - Some (Base x10)); + Some (Base x13)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None @@ -6619,12 +7888,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (let @@ -6730,14 +7996,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - v1 <- type.try_make_transport_cps s5 - ℤ; + v1 <- type.try_make_transport_cps s5 ℤ; fv <- (x10 <- (let '(r1, r2)%zrange := range in @@ -6893,107 +8156,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t4 idc4 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t5 idc5) x7 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x5 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype option - (fun x8 : option => x8) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x11 : option => x11) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s9 ℤ; xv2 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv3 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 bb xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s7 =? - 2 ^ Z.log2 s7) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 s7) - offset)%expr @ - ((##bb)%expr, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := - xv in - x8) - (let (x8, _) := - xv0 in - x8) - (let (x8, _) := - xv1 in - x8) args2 args0 - (v - (Compile.reflect - x7)) - (let (x8, _) := - xv2 in - x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun + (s10 bb xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_subb + (Z.log2 + s10) + offset)%expr @ + ((##bb)%expr, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := + xv in + x11) + (let (x11, _) := + xv0 in + x11) + (let (x11, _) := + xv1 in + x11) args5 args3 + args1 + (v + (Compile.reflect + x10)) + (let (x11, _) := + xv2 in + x11) + (let (x11, _) := + xv3 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -7002,11 +8296,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App - _ _ _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s6 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -7057,8 +8405,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s6 ℤ; xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -7248,108 +8595,137 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s3) -> s7 -> (projT1 args))%ptype - option (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> s3) -> - s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 bb : Z) - (rx : zrange) - (x9 : expr ℤ) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 s8) - offset)%expr @ - ((##bb)%expr, - #(Z_cast rx)%expr @ - x9, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) - (let (x9, _) := - xv0 in - x9) args3 - (v - (Compile.reflect - x4)) args2 - args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 bb : Z) + (rx : zrange) + (x12 : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_subb + (Z.log2 + s11) + offset)%expr @ + ((##bb)%expr, + #(Z_cast rx)%expr @ + x12, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) + (let (x12, _) := + xv0 in + x12) args6 + (v + (Compile.reflect + x4)) args5 + args3 args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -7358,11 +8734,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -7408,10 +8838,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -7612,109 +9040,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args6); + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 : Z) - (rb : zrange) - (b3 : expr ℤ) - (xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 s8) - offset)%expr @ - (#(Z_cast rb)%expr @ - b3, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) args4 - (v - (Compile.reflect - x4)) - (let (x9, _) := - xv0 in - x9) args2 args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 : Z) + (rb : zrange) + (b4 : expr ℤ) + (xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_subb + (Z.log2 + s11) + offset)%expr @ + (#(Z_cast rb)%expr @ + b4, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) args7 + (v + (Compile.reflect + x4)) + (let (x12, _) := + xv0 in + x12) args5 args3 + args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -7723,11 +9180,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -7771,13 +9282,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -7971,68 +9480,80 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x6 with | (@expr.Ident _ _ _ t4 idc4 @ x8 @ x7)%expr_pat => match x8 with - | @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x7 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype option - (fun x10 : option => x10) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x13 : option => x13) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s11 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x10 <- (let + fv <- (x13 <- (let '(r1, r2)%zrange := range in - fun (s9 : Z) + fun (s12 : Z) (rb : zrange) - (b3 : expr ℤ) + (b4 : expr ℤ) (rx : zrange) - (x10 : expr ℤ) - (rshiftl + (x13 : expr ℤ) + (rshiftl rland ry : zrange) (y : expr ℤ) - (offset : Z) => + (mask + offset : Z) => if - (s9 =? - 2 ^ Z.log2 s9) && + (s12 =? + 2 ^ Z.log2 s12) && (ZRange.normalize ry << ZRange.normalize @@ -8042,39 +9563,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with rshiftl)%zrange && (ZRange.normalize rshiftl <=? - r[0 ~> s9 - 1])%zrange + r[0 ~> s12 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s12 - + offset)) then Some (#(Z_cast2 (r1, r2))%expr @ (#(fancy_subb (Z.log2 - s9) + s12) offset)%expr @ (#(Z_cast rb)%expr @ - b3, + b4, #(Z_cast rx)%expr @ - x10, + x13, #(Z_cast ry)%expr @ y)))%expr_pat else None) - (let (x10, _) := + (let (x13, _) := xv in - x10) args4 + x13) args7 (v (Compile.reflect - x4)) args3 + x4)) args6 (v0 (Compile.reflect - x5)) args2 - args0 + x5)) args5 + args3 args1 (v1 (Compile.reflect - x9)) - (let (x10, _) := + x12)) + (let (x13, _) := xv0 in - x10); - Some (Base x10)); + x13) + (let (x13, _) := + xv1 in + x13); + Some (Base x13)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -8083,11 +9618,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s8 _ ($_)%expr _ | @expr.App - _ _ _ s8 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s8 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s8 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x8 with @@ -8129,12 +9718,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); |