diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-15 15:53:34 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-16 16:51:11 -0500 |
| commit | 60bade02ccd577550bfcd5974d3c62a3d40e751a (patch) | |
| tree | 46a9e9ef505704bdff47f0c794c163ecd5d7fd76 /src/arith_with_casts_rewrite_head.out | |
| parent | 538e541709d70caaa78104739cb965c6523d89a8 (diff) | |
Add a rewrite rule to collapse constant casts
If, e.g., we know from bounds analysis that the result of an operation
fits in the range r[0~>0], we now just replace it with the literal
constant.
Fixes #493
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
21m22.14s | Total | 21m22.79s || -0m00.65s | -0.05%
--------------------------------------------------------------------------------------------
4m09.97s | PushButtonSynthesis.vo | 4m10.56s || -0m00.59s | -0.23%
3m09.12s | p384_32.c | 3m08.91s || +0m00.21s | +0.11%
2m05.94s | Rewriter.vo | 2m06.30s || -0m00.35s | -0.28%
1m56.58s | RewriterWf2.vo | 1m56.09s || +0m00.48s | +0.42%
1m52.39s | RewriterRulesGood.vo | 1m52.04s || +0m00.35s | +0.31%
1m46.01s | RewriterRulesInterpGood.vo | 1m45.79s || +0m00.21s | +0.20%
0m46.44s | RewriterInterpProofs1.vo | 0m46.47s || -0m00.03s | -0.06%
0m44.96s | ExtractionHaskell/word_by_word_montgomery | 0m45.59s || -0m00.63s | -1.38%
0m39.18s | p521_32.c | 0m39.33s || -0m00.14s | -0.38%
0m32.41s | p521_64.c | 0m32.54s || -0m00.13s | -0.39%
0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m30.67s || +0m00.19s | +0.65%
0m24.32s | ExtractionHaskell/saturated_solinas | 0m24.44s || -0m00.12s | -0.49%
0m23.59s | RewriterWf1.vo | 0m24.10s || -0m00.51s | -2.11%
0m17.01s | ExtractionOCaml/word_by_word_montgomery | 0m17.14s || -0m00.12s | -0.75%
0m13.48s | secp256k1_32.c | 0m13.30s || +0m00.17s | +1.35%
0m13.11s | p256_32.c | 0m13.37s || -0m00.25s | -1.94%
0m11.34s | p484_64.c | 0m11.34s || +0m00.00s | +0.00%
0m10.78s | ExtractionOCaml/unsaturated_solinas | 0m10.79s || -0m00.00s | -0.09%
0m10.27s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.06s || +0m00.20s | +2.08%
0m08.11s | ExtractionOCaml/saturated_solinas | 0m07.92s || +0m00.18s | +2.39%
0m06.92s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.02s || -0m00.09s | -1.42%
0m06.18s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s || -0m00.10s | -1.59%
0m06.13s | BoundsPipeline.vo | 0m05.98s || +0m00.14s | +2.50%
0m05.90s | p224_32.c | 0m05.92s || -0m00.01s | -0.33%
0m05.29s | p384_64.c | 0m05.33s || -0m00.04s | -0.75%
0m05.17s | ExtractionOCaml/saturated_solinas.ml | 0m05.20s || -0m00.03s | -0.57%
0m04.91s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.93s || -0m00.01s | -0.40%
0m04.06s | ExtractionHaskell/saturated_solinas.hs | 0m04.00s || +0m00.05s | +1.49%
0m02.21s | curve25519_32.c | 0m02.22s || -0m00.01s | -0.45%
0m01.52s | curve25519_64.c | 0m01.50s || +0m00.02s | +1.33%
0m01.38s | CLI.vo | 0m01.42s || -0m00.04s | -2.81%
0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88%
0m01.14s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.17s | +18.74%
0m01.12s | StandaloneHaskellMain.vo | 0m01.03s || +0m00.09s | +8.73%
0m01.12s | secp256k1_64.c | 0m01.00s || +0m00.12s | +12.00%
0m01.05s | p256_64.c | 0m00.98s || +0m00.07s | +7.14%
0m01.03s | p224_64.c | 0m01.15s || -0m00.11s | -10.43%
Diffstat (limited to 'src/arith_with_casts_rewrite_head.out')
| -rw-r--r-- | src/arith_with_casts_rewrite_head.out | 2570 |
1 files changed, 1286 insertions, 1284 deletions
diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out index 2baf1c5d2..053110d89 100644 --- a/src/arith_with_casts_rewrite_head.out +++ b/src/arith_with_casts_rewrite_head.out @@ -888,440 +888,71 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat | Z_cast range => fun x : expr ℤ => - (match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ℤ (projT1 args) option - (fun x0 : option => x0) - with - | Some _ => - if type.type_beq base.type base.type.type_beq ℤ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x0 <- (if - is_bounded_by_bool (let (x0, _) := xv in x0) - range - then Some (##(let (x0, _) := xv in x0))%expr - else None); - Some (Base x0)); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x0 => - args <- invert_bind_args idc Raw.ident.Z_cast; - match - pattern.type.unify_extracted_cps ℤ s option - (fun x1 : option => x1) - with - | Some _ => - if type.type_beq base.type base.type.type_beq ℤ s - then - v <- type.try_make_transport_cps s ℤ; - fv <- (x1 <- (if - (ZRange.normalize args <=? - ZRange.normalize range)%zrange - then - Some - (#(Z_cast args)%expr @ v (Compile.reflect x0))%expr_pat - else None); - Some (Base x1)); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t idc) x2) x1) x0 => - _ <- invert_bind_args idc Raw.ident.Z_add_with_carry; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3) - with - | Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s)%ptype - then - v <- type.try_make_transport_cps s1 ℤ; - v0 <- type.try_make_transport_cps s0 ℤ; - v1 <- type.try_make_transport_cps s ℤ; - Some - (UnderLet - (#(Z_cast range)%expr @ - (#(Z_add_with_carry)%expr @ v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var ℤ => - Base (#(Z_cast range)%expr @ ($v2)%expr)%expr_pat)) - else None - | None => None - end - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ ($_)%expr _) _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _) - _) _ | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _) _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _ => None - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(_)%expr_pat _) _ | - @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ - _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App - _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => - None - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;;; - Base (#(Z_cast range)%expr @ x)%expr_pat)%option -| Z_cast2 range => - fun x : expr (ℤ * ℤ)%etype => - ((match x with - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 => - args <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ)%ptype - ((((let (x2, _) := args in x2) -> - (let (_, y) := args in y) -> - ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype option (fun x2 : option => x2) - with - | Some (_, (_, (_, _)), _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ)%ptype - ((((let (x2, _) := args in x2) -> - (let (_, y) := args in y) -> - ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype - then - _ <- ident.unify pattern.ident.pair pair; - v <- type.try_make_transport_cps s0 ℤ; - v0 <- type.try_make_transport_cps s ℤ; - Some - (fv0 <-- do_again (ℤ * ℤ) - (#(Z_cast (Datatypes.fst range))%expr @ - ($(v (Compile.reflect x1)))%expr, - #(Z_cast (Datatypes.snd range))%expr @ - ($(v0 (Compile.reflect x0)))%expr)%expr_pat; + (((match + pattern.type.unify_extracted_cps ℤ ℤ option (fun x0 : option => x0) + with + | Some _ => + if type.type_beq base.type base.type.type_beq ℤ ℤ + then + fv <- (x0 <- (if lower range =? upper range + then Some (##(lower range))%expr + else None); + Some (Base x0)); + Some (fv0 <-- fv; Base fv0)%under_lets - else None - | None => None - end - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t idc) x2) x1) x0 => - (match x1 with - | (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ - (@expr.Ident _ _ _ t2 idc2) x5))%expr_pat => - args <- invert_bind_args idc2 Raw.ident.Z_cast; - _ <- invert_bind_args idc1 Raw.ident.Z_opp; - args1 <- invert_bind_args idc0 Raw.ident.Z_cast; - _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> s4) -> s)%ptype option (fun x6 : option => x6) - with - | Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s4) -> s)%ptype - then - v <- type.try_make_transport_cps s1 ℤ; - v0 <- type.try_make_transport_cps s4 ℤ; - v1 <- type.try_make_transport_cps s ℤ; - fv <- (if - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v1 (Compile.reflect x0) @ - (#(Z_cast args)%expr @ - v0 (Compile.reflect x5))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ ($_)%expr _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ - (@expr.Abs _ _ _ _ _ _) _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ (_ @ _) _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ - (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None - | (@expr.Ident _ _ _ t0 idc0 @ (@expr.Ident _ _ _ t1 idc1 @ #(_)))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => - None - | (@expr.Ident _ _ _ t0 idc0 @ #(_))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (($_)%expr @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (_ @ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - None - | _ => None - end;; - match x0 with - | (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ - (@expr.Ident _ _ _ t2 idc2) x5))%expr_pat => - args <- invert_bind_args idc2 Raw.ident.Z_cast; - _ <- invert_bind_args idc1 Raw.ident.Z_opp; - args1 <- invert_bind_args idc0 Raw.ident.Z_cast; - _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> s0) -> s4)%ptype option (fun x6 : option => x6) - with - | Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s4)%ptype - then - v <- type.try_make_transport_cps s1 ℤ; - v0 <- type.try_make_transport_cps s0 ℤ; - v1 <- type.try_make_transport_cps s4 ℤ; - fv <- (if - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ - (#(Z_cast args)%expr @ - v1 (Compile.reflect x5))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ ($_)%expr _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ - (@expr.Abs _ _ _ _ _ _) _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ (_ @ _) _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ - (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None - | (@expr.Ident _ _ _ t0 idc0 @ (@expr.Ident _ _ _ t1 idc1 @ #(_)))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ - (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => - None - | (@expr.Ident _ _ _ t0 idc0 @ #(_))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (($_)%expr @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (_ @ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - None - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> (projT1 args)) -> s)%ptype option - (fun x3 : option => x3) - with - | Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> (projT1 args)) -> s)%ptype - then - v <- type.try_make_transport_cps s1 ℤ; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - v0 <- type.try_make_transport_cps s ℤ; - fv <- (if (let (x3, _) := xv in x3) <? 0 - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v0 (Compile.reflect x0) @ - (##(- (let (x3, _) := xv in x3))%Z)%expr))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end;; - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> s0) -> (projT1 args))%ptype option - (fun x3 : option => x3) - with - | Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> s0) -> (projT1 args))%ptype - then - v <- type.try_make_transport_cps s1 ℤ; - v0 <- type.try_make_transport_cps s0 ℤ; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (if (let (x3, _) := xv in x3) <? 0 - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ - (##(- (let (x3, _) := xv in x3))%Z)%expr))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end;; - _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; + else None + | None => None + end;; + match x with + | @expr.Ident _ _ _ t idc => + args <- invert_bind_args idc Raw.ident.Literal; match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3) + pattern.type.unify_extracted_cps ℤ (projT1 args) option + (fun x0 : option => x0) with - | Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s)%ptype + | Some _ => + if type.type_beq base.type base.type.type_beq ℤ (projT1 args) then - v <- type.try_make_transport_cps s1 ℤ; - v0 <- type.try_make_transport_cps s0 ℤ; - v1 <- type.try_make_transport_cps s ℤ; - Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_get_carry)%expr @ v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (x0 <- (if + is_bounded_by_bool (let (x0, _) := xv in x0) + range + then Some (##(let (x0, _) := xv in x0))%expr + else None); + Some (Base x0)); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x0 => + args <- invert_bind_args idc Raw.ident.Z_cast; + match + pattern.type.unify_extracted_cps ℤ s option + (fun x1 : option => x1) + with + | Some _ => + if type.type_beq base.type base.type.type_beq ℤ s + then + v <- type.try_make_transport_cps s ℤ; + fv <- (x1 <- (if + (ZRange.normalize args <=? + ZRange.normalize range)%zrange + then + Some + (#(Z_cast args)%expr @ + v (Compile.reflect x0))%expr_pat + else None); + Some (Base x1)); + Some (fv0 <-- fv; + Base fv0)%under_lets else None | None => None - end);; - (_ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow; + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t idc) x2) x1) x0 => + _ <- invert_bind_args idc Raw.ident.Z_add_with_carry; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3) @@ -1336,19 +967,347 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- type.try_make_transport_cps s ℤ; Some (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_sub_get_borrow)%expr @ v (Compile.reflect x2) @ + (#(Z_cast range)%expr @ + (#(Z_add_with_carry)%expr @ v (Compile.reflect x2) @ v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + (fun v2 : var ℤ => + Base (#(Z_cast range)%expr @ ($v2)%expr)%expr_pat)) else None | None => None - end);; - _ <- invert_bind_args idc Raw.ident.Z_mul_split; + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ ($_)%expr _) _) _ | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _) _) _ | @expr.App _ + _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _) _) + _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _ => None + | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(_)%expr_pat _) _ | + @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App + _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ + (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end);; + None);;; + Base (#(Z_cast range)%expr @ x)%expr_pat)%option +| Z_cast2 range => + fun x : expr (ℤ * ℤ)%etype => + (match x with + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 => + args <- invert_bind_args idc Raw.ident.pair; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ)%ptype + ((((let (x2, _) := args in x2) -> + (let (_, y) := args in y) -> + ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> + s0) -> s)%ptype option (fun x2 : option => x2) + with + | Some (_, (_, (_, _)), _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ)%ptype + ((((let (x2, _) := args in x2) -> + (let (_, y) := args in y) -> + ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> + s0) -> s)%ptype + then + _ <- ident.unify pattern.ident.pair pair; + v <- type.try_make_transport_cps s0 ℤ; + v0 <- type.try_make_transport_cps s ℤ; + Some + (fv0 <-- do_again (ℤ * ℤ) + (#(Z_cast (Datatypes.fst range))%expr @ + ($(v (Compile.reflect x1)))%expr, + #(Z_cast (Datatypes.snd range))%expr @ + ($(v0 (Compile.reflect x0)))%expr)%expr_pat; + Base fv0)%under_lets + else None + | None => None + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t idc) x2) x1) x0 => + (match x1 with + | (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ + (@expr.Ident _ _ _ t2 idc2) x5))%expr_pat => + args <- invert_bind_args idc2 Raw.ident.Z_cast; + _ <- invert_bind_args idc1 Raw.ident.Z_opp; + args1 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s4) -> s)%ptype option (fun x6 : option => x6) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s4) -> s)%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s ℤ; + fv <- (if + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + v (Compile.reflect x2) @ + v1 (Compile.reflect x0) @ + (#(Z_cast args)%expr @ + v0 (Compile.reflect x5))))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ ($_)%expr _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ + (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None + | (@expr.Ident _ _ _ t0 idc0 @ (@expr.Ident _ _ _ t1 idc1 @ #(_)))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t0 idc0 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (_ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | _ => None + end;; + match x0 with + | (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ + (@expr.Ident _ _ _ t2 idc2) x5))%expr_pat => + args <- invert_bind_args idc2 Raw.ident.Z_cast; + _ <- invert_bind_args idc1 Raw.ident.Z_opp; + args1 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> s4)%ptype option (fun x6 : option => x6) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s4)%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + v0 <- type.try_make_transport_cps s0 ℤ; + v1 <- type.try_make_transport_cps s4 ℤ; + fv <- (if + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + v (Compile.reflect x2) @ + v0 (Compile.reflect x1) @ + (#(Z_cast args)%expr @ + v1 (Compile.reflect x5))))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ ($_)%expr _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s4 _ + (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None + | (@expr.Ident _ _ _ t0 idc0 @ (@expr.Ident _ _ _ t1 idc1 @ #(_)))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t0 idc0 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (_ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | _ => None + end;; + match x1 with + | @expr.Ident _ _ _ t0 idc0 => + args <- invert_bind_args idc0 Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> (projT1 args)) -> s)%ptype option + (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> (projT1 args)) -> s)%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + v0 <- type.try_make_transport_cps s ℤ; + fv <- (if (let (x3, _) := xv in x3) <? 0 + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + v (Compile.reflect x2) @ + v0 (Compile.reflect x0) @ + (##(- (let (x3, _) := xv in x3))%Z)%expr))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | _ => None + end;; + match x0 with + | @expr.Ident _ _ _ t0 idc0 => + args <- invert_bind_args idc0 Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> (projT1 args))%ptype option + (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> (projT1 args))%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + v0 <- type.try_make_transport_cps s0 ℤ; + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (if (let (x3, _) := xv in x3) <? 0 + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + v (Compile.reflect x2) @ + v0 (Compile.reflect x1) @ + (##(- (let (x3, _) := xv in x3))%Z)%expr))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | _ => None + end;; + _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3) @@ -1364,7 +1323,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Some (UnderLet (#(Z_cast2 range)%expr @ - (#(Z_mul_split)%expr @ v (Compile.reflect x2) @ + (#(Z_add_get_carry)%expr @ v (Compile.reflect x2) @ v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat (fun v2 : var (ℤ * ℤ)%etype => Base @@ -1374,77 +1333,72 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) else None | None => None - end - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ - (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t idc) x3) x2) x1) x0 => - (match x2 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ - (@expr.Ident _ _ _ t3 idc3) x6))%expr_pat => - (args <- invert_bind_args idc3 Raw.ident.Z_cast; - _ <- invert_bind_args idc2 Raw.ident.Z_opp; - args1 <- invert_bind_args idc1 Raw.ident.Z_cast; - args2 <- 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 - (((s2 -> (projT1 args2)) -> s5) -> s)%ptype option - (fun x7 : option => x7) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> (projT1 args2)) -> s5) -> s)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - xv <- ident.unify pattern.ident.Literal - ##(projT2 args2); - v0 <- type.try_make_transport_cps s5 ℤ; - v1 <- type.try_make_transport_cps s ℤ; - fv <- (if - ((let (x7, _) := xv in x7) =? 0) && - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x3) @ - v1 (Compile.reflect x0) @ - (#(Z_cast args)%expr @ - v0 (Compile.reflect x6))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end);; - args <- invert_bind_args idc3 Raw.ident.Z_cast; + end);; + (_ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s)%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + v0 <- type.try_make_transport_cps s0 ℤ; + v1 <- type.try_make_transport_cps s ℤ; + Some + (UnderLet + (#(Z_cast2 range)%expr @ + (#(Z_sub_get_borrow)%expr @ v (Compile.reflect x2) @ + v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat + (fun v2 : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + else None + | None => None + end);; + _ <- invert_bind_args idc Raw.ident.Z_mul_split; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s)%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + v0 <- type.try_make_transport_cps s0 ℤ; + v1 <- type.try_make_transport_cps s ℤ; + Some + (UnderLet + (#(Z_cast2 range)%expr @ + (#(Z_mul_split)%expr @ v (Compile.reflect x2) @ + v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat + (fun v2 : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + else None + | None => None + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ + (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t idc) x3) x2) x1) x0 => + (match x2 with + | @expr.Ident _ _ _ t0 idc0 => + match x1 with + | (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ + (@expr.Ident _ _ _ t3 idc3) x6))%expr_pat => + (args <- invert_bind_args idc3 Raw.ident.Z_cast; _ <- invert_bind_args idc2 Raw.ident.Z_opp; args1 <- invert_bind_args idc1 Raw.ident.Z_cast; args2 <- invert_bind_args idc0 Raw.ident.Literal; @@ -1467,7 +1421,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s5 ℤ; v1 <- type.try_make_transport_cps s ℤ; fv <- (if - ((let (x7, _) := xv in x7) <? 0) && + ((let (x7, _) := xv in x7) =? 0) && (ZRange.normalize args <=? - ZRange.normalize args1)%zrange then @@ -1476,9 +1430,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ + (#(Z_sub_get_borrow)%expr @ v (Compile.reflect x3) @ - (##(- (let (x7, _) := xv in x7))%Z)%expr @ v1 (Compile.reflect x0) @ (#(Z_cast args)%expr @ v0 (Compile.reflect x6))))%expr_pat @@ -1503,102 +1456,103 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Base fv0)%under_lets else None | None => None - end - | (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ ($_)%expr - _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ - (@expr.Abs _ _ _ _ _ _) _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ (_ @ _) _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None - | (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ #(_)))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ ($_)%expr))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.Abs _ _ _ _ _ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => - None - | (@expr.Ident _ _ _ t1 idc1 @ #(_))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (($_)%expr @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (_ @ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - None - | _ => None - end;; - match x0 with - | (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ - (@expr.Ident _ _ _ t3 idc3) x6))%expr_pat => - (args <- invert_bind_args idc3 Raw.ident.Z_cast; - _ <- invert_bind_args idc2 Raw.ident.Z_opp; - args1 <- invert_bind_args idc1 Raw.ident.Z_cast; - args2 <- 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 - (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype option - (fun x7 : option => x7) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - xv <- ident.unify pattern.ident.Literal - ##(projT2 args2); - v0 <- type.try_make_transport_cps s0 ℤ; - v1 <- type.try_make_transport_cps s5 ℤ; - fv <- (if - ((let (x7, _) := xv in x7) =? 0) && - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x3) @ - v0 (Compile.reflect x1) @ - (#(Z_cast args)%expr @ - v1 (Compile.reflect x6))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end);; - args <- invert_bind_args idc3 Raw.ident.Z_cast; + end);; + args <- invert_bind_args idc3 Raw.ident.Z_cast; + _ <- invert_bind_args idc2 Raw.ident.Z_opp; + args1 <- invert_bind_args idc1 Raw.ident.Z_cast; + args2 <- 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 + (((s2 -> (projT1 args2)) -> s5) -> s)%ptype option + (fun x7 : option => x7) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> (projT1 args2)) -> s5) -> s)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + xv <- ident.unify pattern.ident.Literal + ##(projT2 args2); + v0 <- type.try_make_transport_cps s5 ℤ; + v1 <- type.try_make_transport_cps s ℤ; + fv <- (if + ((let (x7, _) := xv in x7) <? 0) && + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (##(- (let (x7, _) := xv in x7))%Z)%expr @ + v1 (Compile.reflect x0) @ + (#(Z_cast args)%expr @ + v0 (Compile.reflect x6))))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ ($_)%expr + _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ + (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None + | (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ #(_)))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t1 idc1 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (_ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | _ => None + end;; + match x0 with + | (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ + (@expr.Ident _ _ _ t3 idc3) x6))%expr_pat => + (args <- invert_bind_args idc3 Raw.ident.Z_cast; _ <- invert_bind_args idc2 Raw.ident.Z_opp; args1 <- invert_bind_args idc1 Raw.ident.Z_cast; args2 <- invert_bind_args idc0 Raw.ident.Literal; @@ -1621,7 +1575,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s5 ℤ; fv <- (if - ((let (x7, _) := xv in x7) <? 0) && + ((let (x7, _) := xv in x7) =? 0) && (ZRange.normalize args <=? - ZRange.normalize args1)%zrange then @@ -1630,9 +1584,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ + (#(Z_sub_get_borrow)%expr @ v (Compile.reflect x3) @ - (##(- (let (x7, _) := xv in x7))%Z)%expr @ v0 (Compile.reflect x1) @ (#(Z_cast args)%expr @ v1 (Compile.reflect x6))))%expr_pat @@ -1657,665 +1610,688 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Base fv0)%under_lets else None | None => None - end - | (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ ($_)%expr - _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ - (@expr.Abs _ _ _ _ _ _) _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ (_ @ _) _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None - | (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ #(_)))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ ($_)%expr))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.Abs _ _ _ _ _ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ - (@expr.Ident _ _ _ t2 idc2 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => - None - | (@expr.Ident _ _ _ t1 idc1 @ #(_))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (($_)%expr @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (_ @ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - None - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- 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 - (((s2 -> (projT1 args0)) -> (projT1 args)) -> s)%ptype - option (fun x4 : option => x4) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> (projT1 args0)) -> (projT1 args)) -> s)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - xv <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - v0 <- type.try_make_transport_cps s ℤ; - fv <- (if - ((let (x4, _) := xv0 in x4) <=? 0) && - ((let (x4, _) := xv in x4) <=? 0) && - ((let (x4, _) := xv0 in x4) + - (let (x4, _) := xv in x4) <? 0) - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (##(- (let (x4, _) := xv in x4))%Z)%expr @ - v0 (Compile.reflect x0) @ - (##(- (let (x4, _) := xv0 in x4))%Z)%expr))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ + end);; + args <- invert_bind_args idc3 Raw.ident.Z_cast; + _ <- invert_bind_args idc2 Raw.ident.Z_opp; + args1 <- invert_bind_args idc1 Raw.ident.Z_cast; + args2 <- 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 + (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype option + (fun x7 : option => x7) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + xv <- ident.unify pattern.ident.Literal + ##(projT2 args2); + v0 <- type.try_make_transport_cps s0 ℤ; + v1 <- type.try_make_transport_cps s5 ℤ; + fv <- (if + ((let (x7, _) := xv in x7) <? 0) && + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (##(- (let (x7, _) := xv in x7))%Z)%expr @ + v0 (Compile.reflect x1) @ + (#(Z_cast args)%expr @ + v1 (Compile.reflect x6))))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end;; - match x0 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- 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 - (((s2 -> (projT1 args0)) -> s0) -> (projT1 args))%ptype - option (fun x4 : option => x4) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> (projT1 args0)) -> s0) -> (projT1 args))%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - xv <- ident.unify pattern.ident.Literal - ##(projT2 args0); - v0 <- type.try_make_transport_cps s0 ℤ; - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - fv <- (if - ((let (x4, _) := xv0 in x4) <=? 0) && - ((let (x4, _) := xv in x4) <=? 0) && - ((let (x4, _) := xv0 in x4) + - (let (x4, _) := xv in x4) <? 0) - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (##(- (let (x4, _) := xv in x4))%Z)%expr @ - v0 (Compile.reflect x1) @ - (##(- (let (x4, _) := xv0 in x4))%Z)%expr))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ ($_)%expr + _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.App _ _ _ s5 _ + (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None + | (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ #(_)))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ + (@expr.Ident _ _ _ t2 idc2 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t1 idc1 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (_ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | _ => None + end;; + match x1 with + | @expr.Ident _ _ _ t1 idc1 => + args <- invert_bind_args idc1 Raw.ident.Literal; + args0 <- 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 + (((s2 -> (projT1 args0)) -> (projT1 args)) -> s)%ptype + option (fun x4 : option => x4) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> (projT1 args0)) -> (projT1 args)) -> s)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + xv <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args); + v0 <- type.try_make_transport_cps s ℤ; + fv <- (if + ((let (x4, _) := xv0 in x4) <=? 0) && + ((let (x4, _) := xv in x4) <=? 0) && + ((let (x4, _) := xv0 in x4) + + (let (x4, _) := xv in x4) <? 0) + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (##(- (let (x4, _) := xv in x4))%Z)%expr @ + v0 (Compile.reflect x0) @ + (##(- (let (x4, _) := xv0 in x4))%Z)%expr))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end;; - args <- 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 - (((s2 -> (projT1 args)) -> s0) -> s)%ptype option - (fun x4 : option => x4) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | _ => None + end;; + match x0 with + | @expr.Ident _ _ _ t1 idc1 => + args <- invert_bind_args idc1 Raw.ident.Literal; + args0 <- 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 - (((s2 -> (projT1 args)) -> s0) -> s)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - v0 <- type.try_make_transport_cps s0 ℤ; - v1 <- type.try_make_transport_cps s ℤ; - fv <- (if (let (x4, _) := xv in x4) =? 0 - then - Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_get_carry)%expr @ - v (Compile.reflect x3) @ - v0 (Compile.reflect x1) @ - v1 (Compile.reflect x0)))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 range)%expr @ ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 range)%expr @ ($vc)%expr)))%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | @expr.App _ _ _ s3 _ (@expr.Ident _ _ _ t0 idc0) x4 => - match x4 with - | (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ - (@expr.Ident _ _ _ t2 idc2) x6)%expr_pat => - match x1 with - | (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9))%expr_pat => - args <- invert_bind_args idc5 Raw.ident.Z_cast; - _ <- invert_bind_args idc4 Raw.ident.Z_opp; - args1 <- invert_bind_args idc3 Raw.ident.Z_cast; - args2 <- invert_bind_args idc2 Raw.ident.Z_cast; - _ <- invert_bind_args idc1 Raw.ident.Z_opp; - args4 <- invert_bind_args idc0 Raw.ident.Z_cast; - _ <- invert_bind_args idc - Raw.ident.Z_add_with_get_carry; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> s8) -> s)%ptype option - (fun x10 : option => x10) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> s8) -> s)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - v0 <- type.try_make_transport_cps s5 ℤ; - v1 <- type.try_make_transport_cps s8 ℤ; - v2 <- type.try_make_transport_cps s ℤ; - fv <- (if - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange && - (ZRange.normalize args2 <=? - - ZRange.normalize args4)%zrange - then - Some - (UnderLet + (((s2 -> (projT1 args0)) -> s0) -> (projT1 args))%ptype + option (fun x4 : option => x4) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> (projT1 args0)) -> s0) -> (projT1 args))%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + xv <- ident.unify pattern.ident.Literal + ##(projT2 args0); + v0 <- type.try_make_transport_cps s0 ℤ; + xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args); + fv <- (if + ((let (x4, _) := xv0 in x4) <=? 0) && + ((let (x4, _) := xv in x4) <=? 0) && + ((let (x4, _) := xv0 in x4) + + (let (x4, _) := xv in x4) <? 0) + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (##(- (let (x4, _) := xv in x4))%Z)%expr @ + v0 (Compile.reflect x1) @ + (##(- (let (x4, _) := xv0 in x4))%Z)%expr))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args2)%expr @ - v0 (Compile.reflect x6)) @ - v2 (Compile.reflect x0) @ - (#(Z_cast args)%expr @ - v1 (Compile.reflect x9))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | _ => None + end;; + args <- 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 + (((s2 -> (projT1 args)) -> s0) -> s)%ptype option + (fun x4 : option => x4) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> (projT1 args)) -> s0) -> s)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + v0 <- type.try_make_transport_cps s0 ℤ; + v1 <- type.try_make_transport_cps s ℤ; + fv <- (if (let (x4, _) := xv in x4) =? 0 + then + Some + (UnderLet + (#(Z_cast2 range)%expr @ + (#(Z_add_get_carry)%expr @ + v (Compile.reflect x3) @ + v0 (Compile.reflect x1) @ + v1 (Compile.reflect x0)))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 range)%expr @ ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 range)%expr @ ($vc)%expr)))%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | @expr.App _ _ _ s3 _ (@expr.Ident _ _ _ t0 idc0) x4 => + match x4 with + | (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ + (@expr.Ident _ _ _ t2 idc2) x6)%expr_pat => + match x1 with + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (@expr.Ident _ _ _ t5 idc5) x9))%expr_pat => + args <- invert_bind_args idc5 Raw.ident.Z_cast; + _ <- invert_bind_args idc4 Raw.ident.Z_opp; + args1 <- invert_bind_args idc3 Raw.ident.Z_cast; + args2 <- invert_bind_args idc2 Raw.ident.Z_cast; + _ <- invert_bind_args idc1 Raw.ident.Z_opp; + args4 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc + Raw.ident.Z_add_with_get_carry; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> s8) -> s)%ptype option + (fun x10 : option => x10) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> s8) -> s)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s5 ℤ; + v1 <- type.try_make_transport_cps s8 ℤ; + v2 <- type.try_make_transport_cps s ℤ; + fv <- (if + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange && + (ZRange.normalize args2 <=? + - ZRange.normalize args4)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (#(Z_cast args2)%expr @ + v0 (Compile.reflect x6)) @ + v2 (Compile.reflect x0) @ + (#(Z_cast args)%expr @ + v1 (Compile.reflect x9))))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast - (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - ($_)%expr _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Abs _ _ _ _ _ _) _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (_ @ _) _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@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.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 x0 with - | (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9))%expr_pat => - args <- invert_bind_args idc5 Raw.ident.Z_cast; - _ <- invert_bind_args idc4 Raw.ident.Z_opp; - args1 <- invert_bind_args idc3 Raw.ident.Z_cast; - args2 <- invert_bind_args idc2 Raw.ident.Z_cast; - _ <- invert_bind_args idc1 Raw.ident.Z_opp; - args4 <- invert_bind_args idc0 Raw.ident.Z_cast; - _ <- invert_bind_args idc - Raw.ident.Z_add_with_get_carry; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> s0) -> s8)%ptype option - (fun x10 : option => x10) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> s0) -> s8)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - v0 <- type.try_make_transport_cps s5 ℤ; - v1 <- type.try_make_transport_cps s0 ℤ; - v2 <- type.try_make_transport_cps s8 ℤ; - fv <- (if - (ZRange.normalize args <=? - - ZRange.normalize args1)%zrange && - (ZRange.normalize args2 <=? - - ZRange.normalize args4)%zrange - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args2)%expr @ - v0 (Compile.reflect x6)) @ - v1 (Compile.reflect x1) @ - (#(Z_cast args)%expr @ - v2 (Compile.reflect x9))))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + ($_)%expr _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (@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.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 x0 with + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (@expr.Ident _ _ _ t5 idc5) x9))%expr_pat => + args <- invert_bind_args idc5 Raw.ident.Z_cast; + _ <- invert_bind_args idc4 Raw.ident.Z_opp; + args1 <- invert_bind_args idc3 Raw.ident.Z_cast; + args2 <- invert_bind_args idc2 Raw.ident.Z_cast; + _ <- invert_bind_args idc1 Raw.ident.Z_opp; + args4 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc + Raw.ident.Z_add_with_get_carry; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> s0) -> s8)%ptype option + (fun x10 : option => x10) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> s0) -> s8)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s5 ℤ; + v1 <- type.try_make_transport_cps s0 ℤ; + v2 <- type.try_make_transport_cps s8 ℤ; + fv <- (if + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange && + (ZRange.normalize args2 <=? + - ZRange.normalize args4)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (#(Z_cast args2)%expr @ + v0 (Compile.reflect x6)) @ + v1 (Compile.reflect x1) @ + (#(Z_cast args)%expr @ + v2 (Compile.reflect x9))))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast - (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - ($_)%expr _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Abs _ _ _ _ _ _) _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (_ @ _) _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@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.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 x1 with - | @expr.Ident _ _ _ t3 idc3 => - args <- invert_bind_args idc3 Raw.ident.Literal; - args0 <- invert_bind_args idc2 Raw.ident.Z_cast; - _ <- invert_bind_args idc1 Raw.ident.Z_opp; - args2 <- invert_bind_args idc0 Raw.ident.Z_cast; - _ <- invert_bind_args idc - Raw.ident.Z_add_with_get_carry; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> (projT1 args)) -> s)%ptype option - (fun x7 : option => x7) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> (projT1 args)) -> s)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - v0 <- type.try_make_transport_cps s5 ℤ; - xv <- ident.unify pattern.ident.Literal - ##(projT2 args); - v1 <- type.try_make_transport_cps s ℤ; - fv <- (if - ((let (x7, _) := xv in x7) <=? 0) && - (ZRange.normalize args0 <=? - - ZRange.normalize args2)%zrange - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args0)%expr @ - v0 (Compile.reflect x6)) @ - v1 (Compile.reflect x0) @ - (##(- (let (x7, _) := xv in x7))%Z)%expr))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + ($_)%expr _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ + (@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.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 x1 with + | @expr.Ident _ _ _ t3 idc3 => + args <- invert_bind_args idc3 Raw.ident.Literal; + args0 <- invert_bind_args idc2 Raw.ident.Z_cast; + _ <- invert_bind_args idc1 Raw.ident.Z_opp; + args2 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc + Raw.ident.Z_add_with_get_carry; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> (projT1 args)) -> s)%ptype option + (fun x7 : option => x7) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> (projT1 args)) -> s)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s5 ℤ; + xv <- ident.unify pattern.ident.Literal + ##(projT2 args); + v1 <- type.try_make_transport_cps s ℤ; + fv <- (if + ((let (x7, _) := xv in x7) <=? 0) && + (ZRange.normalize args0 <=? + - ZRange.normalize args2)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (#(Z_cast args0)%expr @ + v0 (Compile.reflect x6)) @ + v1 (Compile.reflect x0) @ + (##(- (let (x7, _) := xv in x7))%Z)%expr))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast - (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end;; - match x0 with - | @expr.Ident _ _ _ t3 idc3 => - args <- invert_bind_args idc3 Raw.ident.Literal; - args0 <- invert_bind_args idc2 Raw.ident.Z_cast; - _ <- invert_bind_args idc1 Raw.ident.Z_opp; - args2 <- invert_bind_args idc0 Raw.ident.Z_cast; - _ <- invert_bind_args idc - Raw.ident.Z_add_with_get_carry; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> s0) -> (projT1 args))%ptype option - (fun x7 : option => x7) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s5) -> s0) -> (projT1 args))%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - v0 <- type.try_make_transport_cps s5 ℤ; - v1 <- type.try_make_transport_cps s0 ℤ; - xv <- ident.unify pattern.ident.Literal - ##(projT2 args); - fv <- (if - ((let (x7, _) := xv in x7) <=? 0) && - (ZRange.normalize args0 <=? - - ZRange.normalize args2)%zrange - then - Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args0)%expr @ - v0 (Compile.reflect x6)) @ - v1 (Compile.reflect x1) @ - (##(- (let (x7, _) := xv in x7))%Z)%expr))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | _ => None + end;; + match x0 with + | @expr.Ident _ _ _ t3 idc3 => + args <- invert_bind_args idc3 Raw.ident.Literal; + args0 <- invert_bind_args idc2 Raw.ident.Z_cast; + _ <- invert_bind_args idc1 Raw.ident.Z_opp; + args2 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc + Raw.ident.Z_add_with_get_carry; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> s0) -> (projT1 args))%ptype option + (fun x7 : option => x7) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s5) -> s0) -> (projT1 args))%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s5 ℤ; + v1 <- type.try_make_transport_cps s0 ℤ; + xv <- ident.unify pattern.ident.Literal + ##(projT2 args); + fv <- (if + ((let (x7, _) := xv in x7) <=? 0) && + (ZRange.normalize args0 <=? + - ZRange.normalize args2)%zrange + then + Some + (UnderLet + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + v (Compile.reflect x3) @ + (#(Z_cast args0)%expr @ + v0 (Compile.reflect x6)) @ + v1 (Compile.reflect x1) @ + (##(- (let (x7, _) := xv in x7))%Z)%expr))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + ($vc)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 (Datatypes.fst range, - Datatypes.snd range))%expr @ - ($vc)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast - (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $vc)))%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end - | (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ ($_)%expr - _)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ - (@expr.Abs _ _ _ _ _ _) _)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ (_ @ _) _)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _)%expr_pat => None - | (@expr.Ident _ _ _ t1 idc1 @ #(_))%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - None - | _ => None - end;; - match x3 with - | @expr.Ident _ _ _ t1 idc1 => - match x1 with - | @expr.Ident _ _ _ t2 idc2 => - match x0 with - | @expr.Ident _ _ _ t3 idc3 => - args <- invert_bind_args idc3 Raw.ident.Literal; - args0 <- invert_bind_args idc2 Raw.ident.Literal; - args1 <- invert_bind_args idc1 Raw.ident.Literal; - args2 <- invert_bind_args idc0 Raw.ident.Z_cast; - _ <- invert_bind_args idc - Raw.ident.Z_add_with_get_carry; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args1) -> s3) -> (projT1 args0)) -> - (projT1 args))%ptype option - (fun x5 : option => x5) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args1) -> s3) -> (projT1 args0)) -> - (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - v <- type.try_make_transport_cps s3 ℤ; - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - fv <- (if - ((let (x5, _) := xv0 in x5) =? 0) && - ((let (x5, _) := xv1 in x5) =? 0) && - (ZRange.normalize args2 <=? - r[0 ~> (let (x5, _) := xv in x5) - 1])%zrange && - is_bounded_by_bool 0 - (Datatypes.snd range) - then - Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_with_get_carry)%expr @ - (##(let (x5, _) := xv in x5))%expr @ - (#(Z_cast args2)%expr @ - v (Compile.reflect x4)) @ - (##(let (x5, _) := xv0 in x5))%expr @ - (##(let (x5, _) := xv1 in x5))%expr))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(Z_cast - (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 range)%expr @ - ($vc)%expr)), (##0)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end - | _ => None - end - | _ => None - end - | @expr.App _ _ _ s3 _ ($_)%expr _ | @expr.App _ _ _ s3 _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s3 _ - (_ @ _)%expr_pat _ | @expr.App _ _ _ s3 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;; - _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; - match - pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s1) -> s0) -> s)%ptype option (fun x4 : option => x4) - with - | Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((s2 -> s1) -> s0) -> s)%ptype - then - v <- type.try_make_transport_cps s2 ℤ; - v0 <- type.try_make_transport_cps s1 ℤ; - v1 <- type.try_make_transport_cps s0 ℤ; - v2 <- type.try_make_transport_cps s ℤ; - Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_with_get_carry)%expr @ v (Compile.reflect x3) @ - v0 (Compile.reflect x2) @ v1 (Compile.reflect x1) @ - v2 (Compile.reflect x0)))%expr_pat - (fun v3 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)))%expr_pat)) - else None - | None => None - end);; - _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; + $vc)))%expr_pat)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | _ => None + end + | (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ ($_)%expr _)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ + (@expr.Abs _ _ _ _ _ _) _)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ (_ @ _) _)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s5 _ + (@expr.LetIn _ _ _ _ _ _ _) _)%expr_pat => None + | (@expr.Ident _ _ _ t1 idc1 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | _ => None + end;; + match x3 with + | @expr.Ident _ _ _ t1 idc1 => + match x1 with + | @expr.Ident _ _ _ t2 idc2 => + match x0 with + | @expr.Ident _ _ _ t3 idc3 => + args <- invert_bind_args idc3 Raw.ident.Literal; + args0 <- invert_bind_args idc2 Raw.ident.Literal; + args1 <- invert_bind_args idc1 Raw.ident.Literal; + args2 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc + Raw.ident.Z_add_with_get_carry; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args1) -> s3) -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x5 : option => x5) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args1) -> s3) -> (projT1 args0)) -> + (projT1 args))%ptype + then + xv <- ident.unify pattern.ident.Literal + ##(projT2 args1); + v <- type.try_make_transport_cps s3 ℤ; + xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args); + fv <- (if + ((let (x5, _) := xv0 in x5) =? 0) && + ((let (x5, _) := xv1 in x5) =? 0) && + (ZRange.normalize args2 <=? + r[0 ~> (let (x5, _) := xv in x5) - 1])%zrange && + is_bounded_by_bool 0 + (Datatypes.snd range) + then + Some + (UnderLet + (#(Z_cast2 range)%expr @ + (#(Z_add_with_get_carry)%expr @ + (##(let (x5, _) := xv in x5))%expr @ + (#(Z_cast args2)%expr @ + v (Compile.reflect x4)) @ + (##(let (x5, _) := xv0 in x5))%expr @ + (##(let (x5, _) := xv1 in x5))%expr))%expr_pat + (fun vc : var (ℤ * ℤ)%etype => + Base + (#(Z_cast + (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 range)%expr @ + ($vc)%expr)), (##0)%expr)%expr_pat)) + else None); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | _ => None + end + | _ => None + end + | _ => None + end + | @expr.App _ _ _ s3 _ ($_)%expr _ | @expr.App _ _ _ s3 _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s3 _ (_ @ _)%expr_pat + _ | @expr.App _ _ _ s3 _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end;; + _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((s2 -> s1) -> s0) -> s)%ptype option (fun x4 : option => x4) @@ -2332,7 +2308,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Some (UnderLet (#(Z_cast2 range)%expr @ - (#(Z_sub_with_get_borrow)%expr @ v (Compile.reflect x3) @ + (#(Z_add_with_get_carry)%expr @ v (Compile.reflect x3) @ v0 (Compile.reflect x2) @ v1 (Compile.reflect x1) @ v2 (Compile.reflect x0)))%expr_pat (fun v3 : var (ℤ * ℤ)%etype => @@ -2343,40 +2319,66 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)))%expr_pat)) else None | None => None - end - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ ($_)%expr _) _) _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ - (@expr.App _ _ _ s2 _ (@expr.Abs _ _ _ _ _ _) _) _) _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ (_ @ _)%expr_pat _) _) - _) _ | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ - (@expr.App _ _ _ s2 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _) _ => - None - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ ($_)%expr _) _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _) _) _ | @expr.App _ - _ _ s _ - (@expr.App _ _ _ s0 _ - (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _ => None - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App - _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None - | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr - _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s - _ (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;; - None);;; + end);; + _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; + match + pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((s2 -> s1) -> s0) -> s)%ptype option (fun x4 : option => x4) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((s2 -> s1) -> s0) -> s)%ptype + then + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s1 ℤ; + v1 <- type.try_make_transport_cps s0 ℤ; + v2 <- type.try_make_transport_cps s ℤ; + Some + (UnderLet + (#(Z_cast2 range)%expr @ + (#(Z_sub_with_get_borrow)%expr @ v (Compile.reflect x3) @ + v0 (Compile.reflect x2) @ v1 (Compile.reflect x1) @ + v2 (Compile.reflect x0)))%expr_pat + (fun v3 : var (ℤ * ℤ)%etype => + Base + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)))%expr_pat)) + else None + | None => None + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ ($_)%expr _) _) _) _ | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ + (@expr.App _ _ _ s2 _ (@expr.Abs _ _ _ _ _ _) _) _) _) _ | @expr.App + _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ (_ @ _)%expr_pat _) _) _) + _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ + (@expr.App _ _ _ s2 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _) _ => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ ($_)%expr _) _) _ | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _) + _) _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ + (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _ => None + | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ + _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App + _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => + None + | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr + _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s + _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end;;; Base (#(Z_cast2 range)%expr @ x)%expr_pat)%option | fancy_add log2wordmax imm => fun x : expr (ℤ * ℤ)%etype => |