From 60bade02ccd577550bfcd5974d3c62a3d40e751a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 15 Jan 2019 15:53:34 -0500 Subject: 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% --- src/PushButtonSynthesis.v | 30 +- src/Rewriter.v | 2 + src/RewriterRulesInterpGood.v | 6 +- src/arith_with_casts_rewrite_head.out | 2634 +++++++++++++++++---------------- 4 files changed, 1346 insertions(+), 1326 deletions(-) (limited to 'src') diff --git a/src/PushButtonSynthesis.v b/src/PushButtonSynthesis.v index 0c7f0c994..e20904f63 100644 --- a/src/PushButtonSynthesis.v +++ b/src/PushButtonSynthesis.v @@ -212,11 +212,13 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very Definition saturated_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) := Some saturated_bounds_list. + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) Definition possible_values_of_machine_wordsize - := [machine_wordsize; 2 * machine_wordsize]%Z. + := [0; machine_wordsize; 2 * machine_wordsize]%Z. Definition possible_values_of_machine_wordsize_with_bytes - := [1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. Let possible_values := possible_values_of_machine_wordsize. Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. @@ -600,11 +602,13 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very Definition m_enc : list Z := encode (weight (Qnum limbwidth) (Qden limbwidth)) n s c m. + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) Definition possible_values_of_machine_wordsize - := [machine_wordsize; 2 * machine_wordsize]%Z. + := [0; machine_wordsize; 2 * machine_wordsize]%Z. Definition possible_values_of_machine_wordsize_with_bytes - := [1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. Let possible_values := possible_values_of_machine_wordsize. Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. @@ -1131,8 +1135,10 @@ Module SaturatedSolinas. (c : list (Z * Z)) (machine_wordsize : Z). + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) Definition possible_values_of_machine_wordsize - := [1; machine_wordsize]%Z. + := [0; 1; machine_wordsize]%Z. Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). Let m := s - Associational.eval c. @@ -1518,11 +1524,13 @@ Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize). Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) Definition possible_values_of_machine_wordsize - := [1; machine_wordsize; 2 * machine_wordsize]%Z. + := [0; 1; machine_wordsize; 2 * machine_wordsize]%Z. Definition possible_values_of_machine_wordsize_with_bytes - := [1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. Let possible_values := possible_values_of_machine_wordsize. Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. @@ -2825,8 +2833,10 @@ Module BarrettReduction. Let muLow := mu mod (2 ^ machine_wordsize). Let consts_list := [M; muLow]. + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) Definition possible_values_of_machine_wordsize - := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. + := [0; 1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. Let possible_values := possible_values_of_machine_wordsize. Definition check_args {T} (res : Pipeline.ErrorT T) @@ -3026,8 +3036,10 @@ Module MontgomeryReduction. Let bound := Some value_range. Let consts_list := [N; N']. + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) Definition possible_values_of_machine_wordsize - := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. + := [0; 1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. Local Arguments possible_values_of_machine_wordsize / . Let possible_values := possible_values_of_machine_wordsize. diff --git a/src/Rewriter.v b/src/Rewriter.v index 76071b866..8bbf13173 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1790,6 +1790,8 @@ Module Compilers. := [make_rewrite (#(@pattern.ident.fst '1 '2) @ (??, ??)) (fun _ _ x y => x) ; make_rewrite (#(@pattern.ident.snd '1 '2) @ (??, ??)) (fun _ x _ y => y) + ; make_rewriteo (??') (fun r v => ##(lower r) when lower r =? upper r) + ; make_rewriteo (#?ℤ - (-'??')) (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index 40177e3a0..469f0cb31 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -502,7 +502,11 @@ Module Compilers. => rewrite (@ident.cast_idempotent _ _ r) | [ H : is_bounded_by_bool _ ?r = true |- _] => is_var r; unique pose proof (ZRange.is_bounded_by_normalize _ _ H) - + | [ H : lower ?x = upper ?x |- _ ] => is_var x; destruct x; cbn [upper lower] in * + | [ H : is_bounded_by_bool ?x (ZRange.normalize r[?y~>?y]) = true |- _ ] + => apply ZRange.is_bounded_by_bool_normalize_constant_iff in H + | [ H : is_bounded_by_bool ?x r[?y~>?y] = true |- _ ] + => apply ZRange.is_bounded_by_bool_constant_iff in H end | progress intros | progress subst 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) - 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) - 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) + 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) + 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,360 +1333,108 @@ 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; - _ <- 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) - 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; - _ <- 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; - _ <- 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) - 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 x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; + 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; _ <- 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) + (((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 args0)) -> (projT1 args)) -> s)%ptype + (((s2 -> (projT1 args2)) -> s5) -> 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 ℤ; + ##(projT2 args2); + v0 <- type.try_make_transport_cps s5 ℤ; + v1 <- 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) Base (#(Z_cast (Datatypes.fst range))%expr @ @@ -1749,48 +1456,139 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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; + 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) + 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; _ <- 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) + (((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 args0)) -> s0) -> (projT1 args))%ptype + (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype then v <- type.try_make_transport_cps s2 ℤ; xv <- ident.unify pattern.ident.Literal - ##(projT2 args0); + ##(projT2 args2); v0 <- type.try_make_transport_cps s0 ℤ; - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args); + v1 <- type.try_make_transport_cps s5 ℤ; fv <- (if - ((let (x4, _) := xv0 in x4) <=? 0) && - ((let (x4, _) := xv in x4) <=? 0) && - ((let (x4, _) := xv0 in x4) + - (let (x4, _) := xv in x4) Base (#(Z_cast (Datatypes.fst range))%expr @ @@ -1812,510 +1610,688 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 + 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 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 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) + 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 @ - (#(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 + ($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 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) + 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)) @ - 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_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 + ($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) + 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 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)), + #(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 - | _ => 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 + | (@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 - | _ => 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 + | (@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_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_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 => -- cgit v1.2.3