diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-11-01 15:41:37 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-11-11 11:55:00 -0500 |
| commit | db9921705a8038507335117ecaaeace1f3ac0b80 (patch) | |
| tree | f053b4b931c3203d623d22beb195e3f01388c47f /src | |
| parent | 56c498de53c503222806dfc2399a117802d1b290 (diff) | |
Update the post-bounds rewrite rules
They are all proven, and they work!
To make this possible, we had to make casting commute with negation.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
32m30.13s | Total | 32m17.70s || +0m12.42s | +0.64%
--------------------------------------------------------------------------------------------------------------------
1m38.96s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m23.70s || +0m15.26s | +18.23%
4m44.45s | Experiments/NewPipeline/Toplevel1.vo | 4m58.41s || -0m13.95s | -4.67%
2m08.47s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m56.27s || +0m12.19s | +10.49%
6m36.50s | p384_32.c | 6m42.34s || -0m05.84s | -1.45%
6m19.09s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m15.11s || +0m03.97s | +1.06%
1m24.28s | Experiments/NewPipeline/Rewriter.vo | 1m20.87s || +0m03.40s | +4.21%
0m40.26s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m43.07s || -0m02.81s | -6.52%
1m57.38s | Experiments/NewPipeline/RewriterWf2.vo | 1m59.36s || -0m01.98s | -1.65%
1m40.57s | Experiments/NewPipeline/Toplevel2.vo | 1m41.68s || -0m01.11s | -1.09%
0m42.80s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m41.59s || +0m01.20s | +2.90%
0m25.06s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m26.26s || -0m01.20s | -4.56%
0m18.78s | p256_32.c | 0m17.12s || +0m01.66s | +9.69%
0m18.49s | secp256k1_32.c | 0m17.05s || +0m01.43s | +8.44%
0m15.98s | Experiments/NewPipeline/RewriterWf1.vo | 0m17.00s || -0m01.01s | -5.99%
0m08.04s | p224_32.c | 0m07.03s || +0m01.00s | +14.36%
0m39.70s | p521_32.c | 0m40.46s || -0m00.75s | -1.87%
0m33.03s | p521_64.c | 0m33.98s || -0m00.94s | -2.79%
0m23.34s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m22.79s || +0m00.55s | +2.41%
0m18.64s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m17.70s || +0m00.94s | +5.31%
0m14.98s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m14.20s || +0m00.78s | +5.49%
0m11.58s | p384_64.c | 0m11.49s || +0m00.08s | +0.78%
0m09.16s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.29s || -0m00.12s | -1.39%
0m06.04s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.01s || +0m00.03s | +0.49%
0m05.80s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.85s || -0m00.04s | -0.85%
0m04.74s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.36s || +0m00.37s | +8.71%
0m04.57s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.91s || -0m00.33s | -6.92%
0m03.66s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.55s || +0m00.11s | +3.09%
0m02.24s | curve25519_32.c | 0m02.29s || -0m00.04s | -2.18%
0m02.04s | p224_64.c | 0m01.86s || +0m00.17s | +9.67%
0m01.98s | secp256k1_64.c | 0m02.45s || -0m00.47s | -19.18%
0m01.97s | p256_64.c | 0m01.88s || +0m00.09s | +4.78%
0m01.49s | curve25519_64.c | 0m01.55s || -0m00.06s | -3.87%
0m01.40s | Experiments/NewPipeline/CLI.vo | 0m01.49s || -0m00.09s | -6.04%
0m01.30s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.34s || -0m00.04s | -2.98%
0m01.26s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.31s || -0m00.05s | -3.81%
0m01.10s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.12s || -0m00.02s | -1.78%
0m01.00s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.97s || +0m00.03s | +3.09%
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 244 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesGood.v | 2 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesInterpGood.v | 175 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 3 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/arith_rewrite_head.out | 102 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out | 2779 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/nbe_rewrite_head.out | 32 |
7 files changed, 2148 insertions, 1189 deletions
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index b3ab11159..cadc48b50 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -7,6 +7,7 @@ Require Import Crypto.Util.OptionList. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZUtil.Definitions. Require Crypto.Util.PrimitiveProd. Require Crypto.Util.PrimitiveHList. Require Import Crypto.Experiments.NewPipeline.Language. @@ -397,6 +398,17 @@ Module Compilers. Notation "x &' y" := (#ident.Z_land @ x @ y) : pattern_scope. Notation "x 'mod' y" := (#ident.Z_modulo @ x @ y)%pattern : pattern_scope. Notation "- x" := (#ident.Z_opp @ x) : pattern_scope. + + Notation "??'" := (#ident.Z_cast @ Wildcard _) : pattern_scope. + Notation "x -' y" := (#ident.Z_cast @ (#ident.Z_sub @ x @ y)) : pattern_scope. + Notation "x +' y" := (#ident.Z_cast @ (#ident.Z_add @ x @ y)) : pattern_scope. + Notation "x /' y" := (#ident.Z_cast @ (#ident.Z_div @ x @ y)) : pattern_scope. + Notation "x *' y" := (#ident.Z_cast @ (#ident.Z_mul @ x @ y)) : pattern_scope. + Notation "x >>' y" := (#ident.Z_cast @ (#ident.Z_shiftr @ x @ y)) : pattern_scope. + Notation "x <<' y" := (#ident.Z_cast @ (#ident.Z_shiftl @ x @ y)) : pattern_scope. + Notation "x &'' y" := (#ident.Z_cast @ (#ident.Z_land @ x @ y)) : pattern_scope. + Notation "x 'mod'' y" := (#ident.Z_cast @ (#ident.Z_modulo @ x @ y))%pattern : pattern_scope. + Notation "-' x" := (#ident.Z_cast @ (#ident.Z_opp @ x)) : pattern_scope. End Notations. End pattern. Export pattern.Notations. @@ -1779,143 +1791,189 @@ Module Compilers. ; make_rewriteol (-??) (fun e => (llet v := e in -$v) when negb (SubstVarLike.is_var_fst_snd_pair_opp_cast e)) (* inline negation when the rewriter wouldn't already inline it *) ]. + Let cst {var} (r : zrange) (e : @expr.expr _ _ var _) := (#(ident.Z_cast r) @ e)%expr. + Let cst' {var} (r : zrange) (e : @expr.expr _ _ var _) := (#(ident.Z_cast (-r)) @ e)%expr. + Let cst2 {var} (r : zrange * zrange) (e : @expr.expr _ _ var _) := (#(ident.Z_cast2 r) @ e)%expr. + + Let llet2_opp2 (rvc : zrange * zrange) e + := (let rvc' := (fst rvc, -snd rvc)%zrange in + let cst' e := #(ident.Z_cast2 rvc') @ e in + let cst1 e := #(ident.Z_cast (fst rvc)) @ e in + let cst2 e := #(ident.Z_cast (snd rvc)) @ e in + let cst2' e := #(ident.Z_cast (-snd rvc)) @ e in + (llet vc := cst' e in + (cst1 (#ident.fst @ (cst' ($vc))), cst2 (-(cst2' (#ident.snd @ (cst' ($vc))))))))%expr. + + Let llet2 (rvc : zrange * zrange) e + := ((llet vc := cst2 rvc e in + (cst (fst rvc) (#ident.fst @ (cst2 rvc ($vc))), + cst (snd rvc) (#ident.snd @ (cst2 rvc ($vc))))))%expr. + Definition arith_with_casts_rewrite_rules : rewrite_rulesT := [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 z v => v when z =? 0) + ; make_rewriteo + (#?ℤ - (-'??')) + (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) ; make_rewriteo (#?ℤ - ?? ) (fun z v => -v when z =? 0) ; make_rewriteo (#?ℤ << ??) (fun x y => ##0 when x =? 0) - ; make_rewrite (-(-??)) (fun v => v) + ; make_rewriteo (-(-'??')) (fun rnv rv v => cst rv v when (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??) (fun s xx y => (##0, ##0)%Z when xx =? 0) ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ ?? @ #?ℤ) (fun s y xx => (##0, ##0)%Z when xx =? 0) - ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??) (fun s xx y => (y, ##0)%Z when xx =? 1) - ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ ?? @ #?ℤ) (fun s y xx => (y, ##0)%Z when xx =? 1) - ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??) (fun s xx y => (-y, ##0%Z) when xx =? (-1)) - ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ ?? @ #?ℤ) (fun s y xx => (-y, ##0%Z) when xx =? (-1)) + ; make_rewriteo + (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??') + (fun s xx ry y => (cst ry y, ##0)%Z when (xx =? 1) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + ; make_rewriteo + (#pattern.ident.Z_mul_split @ #?ℤ @ ??' @ #?ℤ) + (fun s ry y xx => (cst ry y, ##0)%Z when (xx =? 1) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + (* + ; make_rewriteo + (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??') + (fun s xx ry y => (cst' ry (-cst ry y), ##0%Z) when (xx =? (-1)) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + ; make_rewriteo + (#pattern.ident.Z_mul_split @ #?ℤ @ ??' @ #?ℤ) + (fun s ry y xx => (cst' ry (-cst ry y), ##0%Z) when (xx =? (-1)) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + *) - ; make_rewritel - (#pattern.ident.Z_add_get_carry @ ?? @ (-??) @ ??) - (fun s y x => (llet vc := #ident.Z_sub_get_borrow @ s @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc)))) - ; make_rewritel - (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ (-??)) - (fun s x y => (llet vc := #ident.Z_sub_get_borrow @ s @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc)))) + + ; make_rewriteol + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ (-'??') @ ??)) + (fun rvc s rny ry y x + => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst ry y)) + when (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) ; make_rewriteol - (#pattern.ident.Z_add_get_carry @ ?? @ #?ℤ @ ??) - (fun s yy x => (llet vc := #ident.Z_sub_get_borrow @ s @ x @ ##(-yy)%Z in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when yy <? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ (-'??'))) + (fun rvc s x rny ry y + => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst ry y)) + when (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) ; make_rewriteol - (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ #?ℤ) - (fun s x yy => (llet vc := #ident.Z_sub_get_borrow @ s @ x @ ##(-yy)%Z in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when yy <? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ #?ℤ @ ??)) + (fun rvc s yy x + => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ ##(-yy)%Z)) + when yy <? 0) + ; make_rewriteol + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ #?ℤ)) + (fun rvc s x yy => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ ##(-yy)%Z)) + when yy <? 0) - ; make_rewritel - (#pattern.ident.Z_add_with_get_carry @ ?? @ (-??) @ (-??) @ ??) - (fun s c y x => (llet vc := #ident.Z_sub_with_get_borrow @ s @ c @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc)))) - ; make_rewritel - (#pattern.ident.Z_add_with_get_carry @ ?? @ (-??) @ ?? @ (-??)) - (fun s c x y => (llet vc := #ident.Z_sub_with_get_borrow @ s @ c @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc)))) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ (-??) @ ??) - (fun s cc y x => (llet vc := #ident.Z_sub_get_borrow @ s @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when cc =? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ (-'??') @ ??)) + (fun rvc s rnc rc c rny ry y x + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ (cst rc c) @ x @ (cst ry y))) + when ((ZRange.normalize ry <=? -ZRange.normalize rny) && (ZRange.normalize rc <=? -ZRange.normalize rnc))%zrange) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ (-??) @ ??) - (fun s cc y x => (llet vc := #ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when cc <? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ ?? @ (-'??'))) + (fun rvc s rnc rc c x rny ry y + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ (cst rc c) @ x @ (cst ry y))) + when ((ZRange.normalize ry <=? -ZRange.normalize rny) && (ZRange.normalize rc <=? -ZRange.normalize rnc))%zrange) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ (-??)) - (fun s cc x y => (llet vc := #ident.Z_sub_get_borrow @ s @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when cc =? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ (-'??') @ ??)) + (fun rvc s cc rny ry y x + => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst ry y)) + when (cc =? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ (-??)) - (fun s cc x y => (llet vc := #ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ y in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when cc <? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ (-'??') @ ??)) + (fun rvc s cc rny ry y x + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ cst ry y)) + when (cc <? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ (-??) @ #?ℤ @ ??) - (fun s c yy x => (llet vc := #ident.Z_sub_with_get_borrow @ s @ c @ x @ ##(-yy)%Z in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when yy <=? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ (-'??'))) + (fun rvc s cc x rny ry y + => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst ry y)) + when (cc =? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ (-??) @ ?? @ #?ℤ) - (fun s c x yy => (llet vc := #ident.Z_sub_with_get_borrow @ s @ c @ x @ ##(-yy)%Z in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when yy <=? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ (-'??'))) + (fun rvc s cc x rny ry y + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ cst ry y)) + when (cc <? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ #?ℤ @ ??) - (fun s cc yy x => (llet vc := #ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ ##(-yy)%Z in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0)) (* at least one must be strictly negative *) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ #?ℤ @ ??)) + (fun rvc s rnc rc c yy x + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst rc c @ x @ ##(-yy)%Z)) + when (yy <=? 0) && (ZRange.normalize rc <=? -ZRange.normalize rnc)%zrange) ; make_rewriteol - (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ #?ℤ) - (fun s cc x yy => (llet vc := #ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ ##(-yy)%Z in - (#ident.fst @ $vc, -(#ident.snd @ $vc))) - when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0)) (* at least one must be strictly negative *) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ ?? @ #?ℤ)) + (fun rvc s rnc rc c x yy + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst rc c @ x @ ##(-yy)%Z)) + when (yy <=? 0) && (ZRange.normalize rc <=? -ZRange.normalize rnc)%zrange) + ; make_rewriteol + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ #?ℤ @ ??)) + (fun rvc s cc yy x + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ ##(-yy)%Z)) + when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0)) (* at least one must be strictly negative *) + ; make_rewriteol + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ #?ℤ)) + (fun rvc s cc x yy + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ ##(-yy)%Z)) + when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0)) (* at least one must be strictly negative *) - ; make_rewriteo (#pattern.ident.Z_add_get_carry @ ?? @ #?ℤ @ ??) (fun s xx y => (y, ##0) when xx =? 0) - ; make_rewriteo (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ #?ℤ) (fun s y xx => (y, ##0) when xx =? 0) + ; make_rewrite + (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ #?ℤ) + (fun s xx yy => ##(Z.add_get_carry_full s xx yy)) + ; make_rewriteo + (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ ??') + (fun s xx ry y => (cst ry y, ##0) when (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + ; make_rewriteo + (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ #?ℤ) + (fun s ry y xx => (cst ry y, ##0) when (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) ; make_rewriteo (#pattern.ident.Z_add_with_carry @ #?ℤ @ ?? @ ??) (fun cc x y => x + y when cc =? 0) (*; make_rewrite_step (#pattern.ident.Z_add_with_carry @ ?? @ ?? @ ??) (fun x y z => $x + $y + $z)*) + ; make_rewrite + (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ #?ℤ) + (fun s cc xx yy => ##(Z.add_with_get_carry_full s cc xx yy)) ; make_rewriteo - (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ ??) (fun s cc xx y => (y, ##0) when (cc =? 0) && (xx =? 0)) + (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ ??') + (fun s cc xx ry y => (cst ry y, ##0) when (cc =? 0) && (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) ; make_rewriteo - (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ?? @ #?ℤ) (fun s cc y xx => (y, ##0) when (cc =? 0) && (xx =? 0)) + (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ #?ℤ) + (fun s cc ry y xx => (cst ry y, ##0) when (cc =? 0) && (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) (*; make_rewriteo (#pattern.ident.Z_add_with_get_carry @ ?? @ ?? @ #?ℤ @ #?ℤ) (fun s c xx yy => (c, ##0) when (xx =? 0) && (yy =? 0))*) ; make_rewriteol (* carry = 0: ADC x y -> ADD x y *) - (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ ??) - (fun s cc x y => (llet vc := #ident.Z_add_get_carry @ s @ x @ y in - (#ident.fst @ $vc, #ident.snd @ $vc)) - when cc =? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ ??)) + (fun rvc s cc x y + => (llet2 rvc (#ident.Z_add_get_carry @ s @ x @ y)) + when cc =? 0) ; make_rewriteol (* ADC 0 0 -> (ADX 0 0, 0) *) (* except we don't do ADX, because C stringification doesn't handle it *) - (#pattern.ident.Z_add_with_get_carry @ ?? @ ?? @ #?ℤ @ #?ℤ) - (fun s c xx yy => (llet vc := #ident.Z_add_with_get_carry @ s @ c @ ##xx @ ##yy in - (#ident.fst @ $vc, ##0)) - when (xx =? 0) && (yy =? 0)) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ #?ℤ)) + (fun rvc s rc c xx yy + => (llet vc := cst2 rvc (#ident.Z_add_with_get_carry @ ##s @ cst rc c @ ##xx @ ##yy) in + (cst (fst rvc) (#ident.fst @ cst2 rvc ($vc)), ##0)) + when (xx =? 0) && (yy =? 0) && (ZRange.normalize rc <=? r[0~>s-1])%zrange && is_bounded_by_bool 0 (snd rvc)) (* let-bind any adc/sbb/mulx *) ; make_rewritel - (#pattern.ident.Z_add_with_get_carry @ ?? @ ?? @ ?? @ ??) - (fun s c x y => (llet vc := #ident.Z_add_with_get_carry @ s @ c @ x @ y in - (#ident.fst @ $vc, #ident.snd @ $vc))) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ ?? @ ?? @ ??)) + (fun rvc s c x y => llet2 rvc (#ident.Z_add_with_get_carry @ s @ c @ x @ y)) ; make_rewritel - (#pattern.ident.Z_add_with_carry @ ?? @ ?? @ ??) - (fun c x y => (llet vc := #ident.Z_add_with_carry @ c @ x @ y in - ($vc))) + (#pattern.ident.Z_cast @ (#pattern.ident.Z_add_with_carry @ ?? @ ?? @ ??)) + (fun rv c x y => (llet vc := cst rv (#ident.Z_add_with_carry @ c @ x @ y) in + (cst rv ($vc)))) ; make_rewritel - (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ ??) - (fun s x y => (llet vc := #ident.Z_add_get_carry @ s @ x @ y in - (#ident.fst @ $vc, #ident.snd @ $vc))) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ ??)) + (fun rvc s x y => llet2 rvc (#ident.Z_add_get_carry @ s @ x @ y)) ; make_rewritel - (#pattern.ident.Z_sub_with_get_borrow @ ?? @ ?? @ ?? @ ??) - (fun s c x y => (llet vc := #ident.Z_sub_with_get_borrow @ s @ c @ x @ y in - (#ident.fst @ $vc, #ident.snd @ $vc))) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_sub_with_get_borrow @ ?? @ ?? @ ?? @ ??)) + (fun rvc s c x y => llet2 rvc (#ident.Z_sub_with_get_borrow @ s @ c @ x @ y)) ; make_rewritel - (#pattern.ident.Z_sub_get_borrow @ ?? @ ?? @ ??) - (fun s x y => (llet vc := #ident.Z_sub_get_borrow @ s @ x @ y in - (#ident.fst @ $vc, #ident.snd @ $vc))) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_sub_get_borrow @ ?? @ ?? @ ??)) + (fun rvc s x y => llet2 rvc (#ident.Z_sub_get_borrow @ s @ x @ y)) ; make_rewritel - (#pattern.ident.Z_mul_split @ ?? @ ?? @ ??) - (fun s x y => (llet vc := #ident.Z_mul_split @ s @ x @ y in - (#ident.fst @ $vc, #ident.snd @ $vc))) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_mul_split @ ?? @ ?? @ ??)) + (fun rvc s x y => llet2 rvc (#ident.Z_mul_split @ s @ x @ y)) + + ; make_rewriteo (#pattern.ident.Z_cast @ #?ℤ) (fun r v => ##v when is_bounded_by_bool v r) + + ; make_rewrite_step (#pattern.ident.Z_cast2 @ (??, ??)) (fun r v1 v2 => (#(ident.Z_cast (fst r)) @ $v1, #(ident.Z_cast (snd r)) @ $v2)) ; make_rewriteo (#pattern.ident.Z_cast @ (#pattern.ident.Z_cast @ ??)) @@ -2389,7 +2447,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) Definition RewriteArith (max_const_val : Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@arith_rewrite_head max_const_val) arith_default_fuel t e. Definition RewriteArithWithCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t - := @Compile.Rewrite (fun var do_again => @arith_with_casts_rewrite_head var) arith_with_casts_default_fuel t e. + := @Compile.Rewrite (@arith_with_casts_rewrite_head) arith_with_casts_default_fuel t e. Definition RewriteToFancy (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v index d66e02998..ec01917e7 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesGood.v @@ -59,7 +59,7 @@ Module Compilers. = (fun var => @fancy_with_casts_rewrite_head0 var (*invert_low invert_high*)). Proof. reflexivity. Qed. - Lemma arith_with_casts_rewrite_head_eq : (fun var _ => @arith_with_casts_rewrite_head var) = @arith_with_casts_rewrite_head0. + Lemma arith_with_casts_rewrite_head_eq : @arith_with_casts_rewrite_head = @arith_with_casts_rewrite_head0. Proof. reflexivity. Qed. Lemma nbe_all_rewrite_rules_eq : @nbe_all_rewrite_rules = @nbe_rewrite_rules. diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v index b205acec1..e5d0e040f 100644 --- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v @@ -172,9 +172,28 @@ Module Compilers. => rewrite ident.cast_normalize | [ H : context[ident.cast (ZRange.normalize ?r)] |- _ ] => rewrite ident.cast_normalize in H + | [ H : ?T, H' : ?T |- _ ] => clear H' + | [ H : context[is_bounded_by_bool _ (ZRange.normalize (-_))] |- _ ] + => rewrite ZRange.is_bounded_by_bool_move_opp_normalize in H + | [ |- context[is_bounded_by_bool _ (ZRange.normalize (-_))] ] + => rewrite ZRange.is_bounded_by_bool_move_opp_normalize + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ ?r ?v] ] + => rewrite (@ident.cast_in_normalized_bounds _ r v) by exact H + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ (-?r) (-?v)] ] + => rewrite (@ident.cast_in_normalized_bounds _ (-r) (-v)); + [ | clear -H ] + | [ |- context[ident.cast _ ?r (-ident.cast _ (-?r) ?v)] ] + => rewrite (ident.cast_in_normalized_bounds r (-ident.cast _ (-r) v)) + by (rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize; apply ident.cast_always_bounded) + | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ] + => 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 : zrange * zrange |- _ ] => destruct H end | progress intros | progress subst + | assumption | progress inversion_option | progress destruct_head'_and | progress Z.ltb_to_lt @@ -294,6 +313,7 @@ Module Compilers. | break_innermost_match_hyps_step | progress destruct_head'_or | match goal with + | [ |- context[-ident.cast _ (-?r) (-?v)] ] => rewrite (ident.cast_opp' r v) | [ |- context[ident.cast ?coor ?r ?v] ] => is_var v; pose proof (@ident.cast_always_bounded coor r v); @@ -304,6 +324,18 @@ Module Compilers. generalize dependent (ident.cast coor r v); intros | [ H : is_bounded_by_bool ?v ?r = true, H' : is_tighter_than_bool ?r ?r' = true |- _ ] => unique assert (is_bounded_by_bool v r' = true) by (eauto 2 using ZRange.is_bounded_by_of_is_tighter_than) + | [ H : is_bounded_by_bool (-?v) ?r = true, H' : (-?r <=? ?r')%zrange = true |- _ ] + => unique assert (is_bounded_by_bool v r' = true) + by (apply (@ZRange.is_bounded_by_of_is_tighter_than _ _ H'); + rewrite <- ZRange.is_bounded_by_bool_opp, ZRange.opp_involutive; exact H) + | [ H : is_bounded_by_bool ?v (-?r) = true |- _ ] + => is_var v; + unique assert (is_bounded_by_bool (-v) r = true) + by now rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize, ZRange.normalize_opp + | [ H : is_bounded_by_bool ?x r[0~>?v-1] = true |- _ ] + => progress (try unique assert (0 <= x); try unique assert (x <= v - 1)); + [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia.. + | ] end | match goal with | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))] @@ -312,6 +344,7 @@ Module Compilers. | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r + | [ |- context[- - _] ] => rewrite Z.opp_involutive | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ] => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith @@ -323,11 +356,33 @@ Module Compilers. | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const | [ |- ?f (?g (nat_rect _ _ _ ?n ?v)) = nat_rect _ _ _ ?n _ ] => revert v; is_var n; induction n; intro v; cbn [nat_rect] + | [ H : 0 <= ?x, H' : ?x <= ?r - 1 |- context[?x mod ?r] ] + => rewrite (Z.mod_small x r) by (clear -H H'; lia) + | [ H : 0 <= ?x, H' : ?x <= ?y - 1 |- context[?x / ?y] ] + => rewrite (Z.div_small x y) by (clear -H H'; lia) | [ |- _ mod ?x = _ mod ?x ] => progress (push_Zmod; pull_Zmod) | [ |- _ mod ?x = _ mod ?x ] => apply f_equal2; (lia + nia) + | [ |- context[-?x + ?y] ] => rewrite !Z.add_opp_l + | [ |- context[?n + - ?m] ] => rewrite !Z.add_opp_r + | [ |- context[?n - - ?m] ] => rewrite !Z.sub_opp_r + | [ |- ?f (?a mod ?r) = ?f (?b mod ?r) ] => apply f_equal; apply f_equal2; lia + | [ |- context[-?a - ?b + ?c] ] => replace (-a - b + c) with (c - a - b) by (clear; lia) + | [ |- context[?x - ?y + ?z] ] + => lazymatch goal with + | [ |- context[z - y + x] ] + => progress replace (z - y + x) with (x - y + z) by (clear; lia) + end + | [ |- context[?x - ?y - ?z] ] + => lazymatch goal with + | [ |- context[x - z - y] ] + => progress replace (x - z - y) with (x - y - z) by (clear; lia) + end + | [ |- - ident.cast _ (-?r) (- (?x / ?y)) = ident.cast _ ?r (?x' / ?y) ] + => tryif constr_eq x x' then fail else replace x with x' by lia | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast + | [ |- ident.cast _ ?r _ = ident.cast _ ?r _ ] => apply f_equal; Z.div_mod_to_quot_rem; nia end ]. Lemma nbe_rewrite_rules_interp_good @@ -337,9 +392,6 @@ Module Compilers. Time all: repeat interp_good_t_step. Qed. - Axiom proof_admitted : False. - Local Notation admit := (match proof_admitted with end). - Lemma arith_rewrite_rules_interp_good max_const : rewrite_rules_interp_goodT (arith_rewrite_rules max_const). Proof using Type. @@ -351,119 +403,7 @@ Module Compilers. : rewrite_rules_interp_goodT arith_with_casts_rewrite_rules. Proof using Type. Time start_interp_good. - Time all: try solve [ repeat interp_good_t_step; (lia + nia) ]. - (* This is mainly for display *) - all: repeat first [ progress cbn [Compile.value' Compile.reify] in * - | progress subst - | match goal with - | [ H : context[expr.interp ?ii ?v] |- _ ] - => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros - | [ |- context[expr.interp ?ii ?v] ] - => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros - end ]. - (* 9 subgoals (ID 32915) - - cast_outside_of_range : zrange -> Z -> Z - max_const, x, x0 : Z - v1 : expr (type.base base.type.Z) - ============================ - match - (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1); - Some (UnderLets.Base x1))%option - with - | Some v0 => - expr.interp ident_interp (UnderLets.interp ident_interp v0) = - Z.mul_split x x0 (expr.interp ident_interp v1) - | None => True - end - -subgoal 2 (ID 32967) is: - match - (x1 <- rwhen (Some (v1, (##0)%expr)%expr_pat) (x0 =? 1); - Some (UnderLets.Base x1))%option - with - | Some v0 => - expr.interp ident_interp (UnderLets.interp ident_interp v0) = - Z.mul_split x (expr.interp ident_interp v1) x0 - | None => True - end -subgoal 3 (ID 33019) is: - match - (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1); - Some (UnderLets.Base x1))%option - with - | Some v0 => - expr.interp ident_interp (UnderLets.interp ident_interp v0) = - Z.mul_split x x0 (expr.interp ident_interp v1) - | None => True - end -subgoal 4 (ID 33071) is: - match - (x1 <- rwhen (Some ((- v1)%expr, (##0)%expr)%expr_pat) (x0 =? -1); - Some (UnderLets.Base x1))%option - with - | Some v0 => - expr.interp ident_interp (UnderLets.interp ident_interp v0) = - Z.mul_split x (expr.interp ident_interp v1) x0 - | None => True - end -subgoal 5 (ID 33168) is: - match - (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0); - Some (UnderLets.Base x0))%option - with - | Some v1 => - expr.interp ident_interp (UnderLets.interp ident_interp v1) = - Z.add_get_carry_full v2 x (expr.interp ident_interp v0) - | None => True - end -subgoal 6 (ID 33265) is: - match - (x0 <- rwhen (Some (v0, (##0)%expr)%expr_pat) (x =? 0); - Some (UnderLets.Base x0))%option - with - | Some v1 => - expr.interp ident_interp (UnderLets.interp ident_interp v1) = - Z.add_get_carry_full v2 (expr.interp ident_interp v0) x - | None => True - end -subgoal 7 (ID 33320) is: - match - (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0)); - Some (UnderLets.Base x2))%option - with - | Some v0 => - expr.interp ident_interp (UnderLets.interp ident_interp v0) = - Z.add_with_get_carry_full x x0 x1 (expr.interp ident_interp v1) - | None => True - end -subgoal 8 (ID 33376) is: - match - (x2 <- rwhen (Some (v1, (##0)%expr)%expr_pat) ((x0 =? 0) && (x1 =? 0)); - Some (UnderLets.Base x2))%option - with - | Some v0 => - expr.interp ident_interp (UnderLets.interp ident_interp v0) = - Z.add_with_get_carry_full x x0 (expr.interp ident_interp v1) x1 - | None => True - end -subgoal 9 (ID 33473) is: - match - rwhenl - (Some - (UnderLets.UnderLet - (#(ident.Z_add_with_get_carry)%expr @ v1 @ v0 @ (##x)%expr @ (##x0)%expr)%expr_pat - (fun vc : Z * Z => - UnderLets.Base (#(ident.fst)%expr @ ($vc)%expr, (##0)%expr)%expr_pat))) - ((x =? 0) && (x0 =? 0)) - with - | Some v2 => - expr.interp ident_interp (UnderLets.interp ident_interp v2) = - Z.add_with_get_carry_full (expr.interp ident_interp v1) (expr.interp ident_interp v0) x x0 - | None => True - end - *) - 1-9: exact admit. + Time all: try solve [ repeat interp_good_t_step; Z.div_mod_to_quot_rem; (lia + nia) ]. Qed. Local Ltac fancy_local_t := @@ -473,6 +413,9 @@ subgoal 9 (ID 33473) is: end | progress autorewrite with zsimplify in * ]. + Axiom proof_admitted : False. + Local Notation admit := (match proof_admitted with end). + Lemma fancy_rewrite_rules_interp_good (invert_low invert_high : Z -> Z -> option Z) (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 390683b93..b1bf23019 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -714,7 +714,6 @@ Module Pipeline. let E := PartialEvaluate E in let E := RewriteAndEliminateDeadAndInline (RewriteRules.RewriteArith 0) with_dead_code_elimination with_subst01 E in let E := RewriteRules.RewriteArith (2^8) E in (* reassociate small consts *) - let E := RewriteAndEliminateDeadAndInline RewriteRules.RewriteArithWithCasts with_dead_code_elimination with_subst01 E in let E := match translate_to_fancy with | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancy invert_low invert_high E | None => E @@ -724,7 +723,7 @@ Module Pipeline. let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in match E' with | inl E - => (*let E := RewriteAndEliminateDeadAndInline RewriteRules.RewriteArithWithCasts with_dead_code_elimination with_subst01 E in*) + => let E := RewriteAndEliminateDeadAndInline RewriteRules.RewriteArithWithCasts with_dead_code_elimination with_subst01 E in let E := match translate_to_fancy with | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancyWithCasts invert_low invert_high E | None => E diff --git a/src/Experiments/NewPipeline/arith_rewrite_head.out b/src/Experiments/NewPipeline/arith_rewrite_head.out index c27f9feda..ea72d9b26 100644 --- a/src/Experiments/NewPipeline/arith_rewrite_head.out +++ b/src/Experiments/NewPipeline/arith_rewrite_head.out @@ -27,7 +27,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> s0) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _, _, (_, (_, (_, _)), b3, b2)) => + | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange => if type.type_beq base.type base.type.type_beq (((b3 * b2)%etype -> b3) -> @@ -78,7 +78,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> s0) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _, _, (_, (_, (_, _)), b3, b2)) => + | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange => if type.type_beq base.type base.type.type_beq (((b3 * b2)%etype -> b2) -> @@ -222,7 +222,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -244,7 +244,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -267,7 +267,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (s -> (projT1 args0))%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> (projT1 args0))%ptype @@ -291,7 +291,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> (projT1 args0))%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> (projT1 args0))%ptype @@ -324,7 +324,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype @@ -348,7 +348,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype @@ -374,7 +374,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s0 -> s)%ptype option (fun x3 : option => x3) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s0 -> s)%ptype @@ -406,7 +406,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> ℤ)%ptype @@ -428,7 +428,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> s)%ptype @@ -458,7 +458,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype @@ -481,7 +481,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -503,7 +503,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -525,7 +525,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -547,7 +547,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -569,7 +569,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> (projT1 args0))%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> (projT1 args0))%ptype @@ -598,7 +598,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype @@ -627,7 +627,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -649,7 +649,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -671,7 +671,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -695,7 +695,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -719,7 +719,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s0 -> s)%ptype option (fun x3 : option => x3) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s0 -> s)%ptype @@ -750,7 +750,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> ℤ)%ptype @@ -772,7 +772,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -796,7 +796,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> s)%ptype @@ -818,7 +818,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -856,7 +856,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args2) -> (projT1 args0) -> s2 -> s1)%ptype option (fun x5 : option => x5) with - | Some (_, (_, (_, _))) => + | Some (_, (_, (_, _)))%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ -> ℤ -> ℤ)%ptype @@ -913,7 +913,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args2) -> s0 -> s2 -> (projT1 args))%ptype option (fun x5 : option => x5) with - | Some (_, (_, (_, _))) => + | Some (_, (_, (_, _)))%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ -> ℤ -> ℤ)%ptype @@ -963,7 +963,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((projT1 args0) -> s0 -> s)%ptype option (fun x3 : option => x3) with - | Some (_, (_, _)) => + | Some (_, (_, _))%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ -> ℤ)%ptype ((projT1 args0) -> s0 -> s)%ptype @@ -1001,7 +1001,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -1034,7 +1034,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args0) -> s)%ptype @@ -1059,7 +1059,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -1081,7 +1081,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -1103,7 +1103,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype @@ -1127,7 +1127,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype @@ -1159,7 +1159,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -1183,7 +1183,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> (projT1 args))%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> (projT1 args))%ptype @@ -1208,7 +1208,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> (projT1 args))%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> (projT1 args))%ptype @@ -1240,7 +1240,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -1264,7 +1264,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s0 -> s)%ptype option (fun x3 : option => x3) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s0 -> s)%ptype @@ -1295,7 +1295,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (s -> ℤ)%ptype @@ -1317,7 +1317,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> s)%ptype @@ -1362,7 +1362,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Some _ => if type.type_beq base.type base.type.type_beq ℤ ℤ then - fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp x) + fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp_cast x) then Some (UnderLet x @@ -1388,7 +1388,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -1406,7 +1406,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -1436,7 +1436,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -1454,7 +1454,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -1492,7 +1492,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype (ℤ -> (projT1 args))%ptype @@ -1514,7 +1514,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -1576,7 +1576,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> s0) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, (_, (_, _)), _, _) => + | Some (_, (_, (_, _)), _, _)%zrange => if type.type_beq base.type base.type.type_beq (((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ)%ptype diff --git a/src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out b/src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out index cdcbf9e3b..09b79718d 100644 --- a/src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out +++ b/src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out @@ -27,7 +27,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> s0) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _, _, (_, (_, (_, _)), b3, b2)) => + | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange => if type.type_beq base.type base.type.type_beq (((b3 * b2)%etype -> b3) -> @@ -78,7 +78,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> s0) -> s)%ptype option (fun x2 : option => x2) with - | Some (_, _, _, (_, (_, (_, _)), b3, b2)) => + | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange => if type.type_beq base.type base.type.type_beq (((b3 * b2)%etype -> b2) -> @@ -221,31 +221,64 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((match x with | @expr.Ident _ _ _ t idc => match x0 with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x1 => - _ <- invert_bind_args idc0 Raw.ident.Z_opp; - args0 <- invert_bind_args idc Raw.ident.Literal; + | (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s1 _ + (@expr.Ident _ _ _ t2 idc2) x3))%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; + args2 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype - ((projT1 args0) -> s)%ptype option (fun x2 : option => x2) + ((projT1 args2) -> s1)%ptype option (fun x4 : option => x4) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> s)%ptype + ((projT1 args2) -> s1)%ptype then idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - v <- type.try_make_transport_cps s ℤ; - x2 <- (if (let (x2, _) := idc_args in x2) =? 0 - then Some (v (Compile.reflect x1)) + ##(projT2 args2); + v <- type.try_make_transport_cps s1 ℤ; + x4 <- (if + ((let (x4, _) := idc_args in x4) =? 0) && + (ZRange.normalize args <=? + - ZRange.normalize args1)%zrange + then + Some + (#(Z_cast args)%expr @ v (Compile.reflect x3))%expr_pat else None); - Some (Base x2) + Some (Base x4) else None | None => None end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat - _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s1 _ ($_)%expr _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s1 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s1 _ (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t0 idc0 @ + (@expr.Ident _ _ _ t1 idc1 @ @expr.App _ _ _ s1 _ + (@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;; args <- invert_bind_args idc Raw.ident.Literal; @@ -253,7 +286,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -273,23 +306,56 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Z_opp => fun x : expr ℤ => ((match x with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x0 => - _ <- invert_bind_args idc Raw.ident.Z_opp; + | (@expr.Ident _ _ _ t idc @ + (@expr.Ident _ _ _ t0 idc0 @ @expr.App _ _ _ s1 _ + (@expr.Ident _ _ _ t1 idc1) x2))%expr_pat => + args <- invert_bind_args idc1 Raw.ident.Z_cast; + _ <- invert_bind_args idc0 Raw.ident.Z_opp; + args1 <- invert_bind_args idc Raw.ident.Z_cast; match - pattern.type.unify_extracted_cps ℤ s option - (fun x1 : option => x1) + pattern.type.unify_extracted_cps ℤ s1 option + (fun x3 : option => x3) with | Some _ => - if type.type_beq base.type base.type.type_beq ℤ s + if type.type_beq base.type base.type.type_beq ℤ s1 then - v <- type.try_make_transport_cps s ℤ; - Some (Base (v (Compile.reflect x0))) + v <- type.try_make_transport_cps s1 ℤ; + x3 <- (if + (ZRange.normalize args <=? - ZRange.normalize args1)%zrange + then + Some + (#(Z_cast args)%expr @ v (Compile.reflect x2))%expr_pat + else None); + Some (Base x3) else None | None => None end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t idc @ + (@expr.Ident _ _ _ t0 idc0 @ @expr.App _ _ _ s1 _ ($_)%expr _))%expr_pat | + (@expr.Ident _ _ _ t idc @ + (@expr.Ident _ _ _ t0 idc0 @ @expr.App _ _ _ s1 _ + (@expr.Abs _ _ _ _ _ _) _))%expr_pat | + (@expr.Ident _ _ _ t idc @ + (@expr.Ident _ _ _ t0 idc0 @ @expr.App _ _ _ s1 _ (_ @ _) _))%expr_pat | + (@expr.Ident _ _ _ t idc @ + (@expr.Ident _ _ _ t0 idc0 @ @expr.App _ _ _ s1 _ + (@expr.LetIn _ _ _ _ _ _ _) _))%expr_pat => None + | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ #(_)))%expr_pat | + (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t idc @ + (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t idc @ + (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t idc @ #(_))%expr_pat | + (@expr.Ident _ _ _ t idc @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t idc @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t idc @ (_ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t idc @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None | _ => None end;; None);;; @@ -313,7 +379,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1) with - | Some (_, _) => + | Some (_, _)%zrange => if type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype ((projT1 args) -> ℤ)%ptype @@ -336,45 +402,45 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 : expr ℤ => Base (#(Z_lnot_modulo)%expr @ x @ x0)%expr_pat | Z_mul_split => fun x x0 x1 : expr ℤ => - (((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype - then - _ <- ident.unify pattern.ident.Literal ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args0 in x2) =? 0 - then Some ((##0)%expr, (##0)%expr)%expr_pat - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; + ((match x with + | @expr.Ident _ _ _ t idc => + match x0 with + | @expr.Ident _ _ _ t0 idc0 => + args <- invert_bind_args idc0 Raw.ident.Literal; + args0 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype option + (fun x2 : option => x2) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype + then + _ <- ident.unify pattern.ident.Literal ##(projT2 args0); + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args); + x2 <- (if (let (x2, _) := idc_args0 in x2) =? 0 + then Some ((##0)%expr, (##0)%expr)%expr_pat + else None); + Some (Base x2) + else None + | None => None + end + | _ => None + end;; + match x1 with + | @expr.Ident _ _ _ t0 idc0 => + (args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args0) -> ℤ) -> (projT1 args))%ptype option (fun x2 : option => x2) with - | Some (_, _, _) => + | Some (_, _, _)%zrange => if type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype @@ -389,557 +455,750 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Some (Base x2) else None | None => None - end - | _ => None - end;; - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype - then - _ <- ident.unify pattern.ident.Literal ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args0 in x2) =? 1 - then Some (x1, (##0)%expr)%expr_pat - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> ℤ) -> (projT1 args))%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> ℤ) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.Literal ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args0 in x2) =? 1 - then Some (x0, (##0)%expr)%expr_pat - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end;; - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype - then - _ <- ident.unify pattern.ident.Literal ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args0 in x2) =? -1 - then Some ((- x1)%expr, (##0)%expr)%expr_pat - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> ℤ) -> (projT1 args))%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args0) -> ℤ) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.Literal ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args0 in x2) =? -1 - then Some ((- x0)%expr, (##0)%expr)%expr_pat - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end - | _ => None - end;; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype - then - Some - (UnderLet (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat - (fun v : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v)%expr, #(snd)%expr @ ($v)%expr)%expr_pat)) - else None - | None => None - end);; + end);; + match x0 with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t1 idc1) x2 => + args <- invert_bind_args idc1 Raw.ident.Z_cast; + args0 <- invert_bind_args idc0 Raw.ident.Literal; + args1 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> s) -> (projT1 args0))%ptype option + (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> s) -> (projT1 args0))%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args1); + v <- type.try_make_transport_cps s ℤ; + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + x3 <- (if + ((let (x3, _) := idc_args0 in x3) =? 1) && + (ZRange.normalize args <=? + r[0 ~> (let (x3, _) := idc_args in x3) - 1])%zrange + then + Some + (#(Z_cast args)%expr @ + v (Compile.reflect x2), (##0)%expr)%expr_pat + else None); + Some (Base x3) + else None + | None => None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ + (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ + (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x2 => + match x0 with + | @expr.Ident _ _ _ t1 idc1 => + args <- invert_bind_args idc1 Raw.ident.Literal; + args0 <- invert_bind_args idc0 Raw.ident.Z_cast; + args1 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> (projT1 args)) -> s)%ptype option + (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> (projT1 args)) -> s)%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args1); + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args); + v <- type.try_make_transport_cps s ℤ; + x3 <- (if + ((let (x3, _) := idc_args0 in x3) =? 1) && + (ZRange.normalize args0 <=? + r[0 ~> (let (x3, _) := idc_args in x3) - 1])%zrange + then + Some + (#(Z_cast args0)%expr @ + v (Compile.reflect x2), (##0)%expr)%expr_pat + else None); + Some (Base x3) + else None + | None => None + end + | _ => None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat + _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end + | _ => None + end;; None);;; Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_get_carry => fun x x0 x1 : expr ℤ => - (((match x0 with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x2 => - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> s) -> ℤ)%ptype option (fun x3 : option => x3) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> s) -> ℤ)%ptype - then - v <- type.try_make_transport_cps s ℤ; - Some - (UnderLet - (#(Z_sub_get_borrow)%expr @ x @ x1 @ - v (Compile.reflect x2))%expr_pat - (fun v0 : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v0)%expr, - (- (#(snd)%expr @ $v0)%expr_pat)%expr)%expr_pat)) - else None - | None => None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;; - match x1 with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x2 => - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> s)%ptype option (fun x3 : option => x3) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> s)%ptype - then - v <- type.try_make_transport_cps s ℤ; - Some - (UnderLet - (#(Z_sub_get_borrow)%expr @ x @ x0 @ - v (Compile.reflect x2))%expr_pat - (fun v0 : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v0)%expr, - (- (#(snd)%expr @ $v0)%expr_pat)%expr)%expr_pat)) - else None - | None => None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;; - match x0 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> (projT1 args)) -> ℤ)%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> (projT1 args)) -> ℤ)%ptype - then - idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (if (let (x2, _) := idc_args in x2) <? 0 - then - Some - (UnderLet - (#(Z_sub_get_borrow)%expr @ x @ x1 @ - (##(- (let (x2, _) := idc_args in x2))%Z)%expr)%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> (projT1 args))%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> (projT1 args))%ptype - then - idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (if (let (x2, _) := idc_args in x2) <? 0 - then - Some - (UnderLet - (#(Z_sub_get_borrow)%expr @ x @ x0 @ - (##(- (let (x2, _) := idc_args in x2))%Z)%expr)%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%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 _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> (projT1 args)) -> ℤ)%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> (projT1 args)) -> ℤ)%ptype - then - idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args in x2) =? 0 - then Some (x1, (##0)%expr)%expr_pat - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> (projT1 args))%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> (projT1 args))%ptype - then - idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args in x2) =? 0 - then Some (x0, (##0)%expr)%expr_pat - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end;; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype - then - Some - (UnderLet (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat - (fun v : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v)%expr, #(snd)%expr @ ($v)%expr)%expr_pat)) - else None - | None => None - end);; + ((match x with + | @expr.Ident _ _ _ t idc => + match x0 with + | @expr.Ident _ _ _ t0 idc0 => + match x1 with + | @expr.Ident _ _ _ t1 idc1 => + args <- invert_bind_args idc1 Raw.ident.Literal; + args0 <- invert_bind_args idc0 Raw.ident.Literal; + args1 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype + option (fun x2 : option => x2) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args1); + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + idc_args1 <- ident.unify pattern.ident.Literal + ##(projT2 args); + Some + (Base + (let + '(a1, b1)%zrange := + Z.add_get_carry_full + (let (x2, _) := idc_args in x2) + (let (x2, _) := idc_args0 in x2) + (let (x2, _) := idc_args1 in x2) in + ((##a1)%expr, (##b1)%expr)%expr_pat)) + else None + | None => None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t1 idc1) x2 => + args <- invert_bind_args idc1 Raw.ident.Z_cast; + args0 <- invert_bind_args idc0 Raw.ident.Literal; + args1 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> (projT1 args0)) -> s)%ptype option + (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> (projT1 args0)) -> s)%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args1); + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + v <- type.try_make_transport_cps s ℤ; + x3 <- (if + ((let (x3, _) := idc_args0 in x3) =? 0) && + (ZRange.normalize args <=? + r[0 ~> (let (x3, _) := idc_args in x3) - 1])%zrange + then + Some + (#(Z_cast args)%expr @ + v (Compile.reflect x2), (##0)%expr)%expr_pat + else None); + Some (Base x3) + else None + | None => None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ + (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ + (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x2 => + match x1 with + | @expr.Ident _ _ _ t1 idc1 => + args <- invert_bind_args idc1 Raw.ident.Literal; + args0 <- invert_bind_args idc0 Raw.ident.Z_cast; + args1 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> s) -> (projT1 args))%ptype option + (fun x3 : option => x3) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args1) -> s) -> (projT1 args))%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args1); + v <- type.try_make_transport_cps s ℤ; + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args); + x3 <- (if + ((let (x3, _) := idc_args0 in x3) =? 0) && + (ZRange.normalize args0 <=? + r[0 ~> (let (x3, _) := idc_args in x3) - 1])%zrange + then + Some + (#(Z_cast args0)%expr @ + v (Compile.reflect x2), (##0)%expr)%expr_pat + else None); + Some (Base x3) + else None + | None => None + end + | _ => None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat + _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end + | _ => None + end;; None);;; Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_with_carry => fun x x0 x1 : expr ℤ => - (((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args) -> ℤ) -> ℤ)%ptype option - (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args) -> ℤ) -> ℤ)%ptype - then - idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - x2 <- (if (let (x2, _) := idc_args in x2) =? 0 - then Some (x0 + x1)%expr - else None); - Some (Base x2) - else None - | None => None - end - | _ => None - end;; - match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype - then - Some - (UnderLet (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat - (fun v : var ℤ => Base ($v)%expr)) - else None - | None => None - end);; - None);;; + (match x with + | @expr.Ident _ _ _ t idc => + args <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args) -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2) + with + | Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args) -> ℤ) -> ℤ)%ptype + then + idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); + x2 <- (if (let (x2, _) := idc_args in x2) =? 0 + then Some (x0 + x1)%expr + else None); + Some (Base x2) + else None + | None => None + end + | _ => None + end;;; Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_with_get_carry => fun x x0 x1 x2 : expr ℤ => - (((match x0 with - | @expr.Ident _ _ _ t idc => - match x1 with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x3 => - (_ <- invert_bind_args idc0 Raw.ident.Z_opp; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype option - (fun x4 : option => x4) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype - then - idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - v <- type.try_make_transport_cps s ℤ; - fv <- (if (let (x4, _) := idc_args in x4) =? 0 - then - Some - (UnderLet - (#(Z_sub_get_borrow)%expr @ x @ x2 @ - v (Compile.reflect x3))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end);; - _ <- invert_bind_args idc0 Raw.ident.Z_opp; - args0 <- invert_bind_args idc Raw.ident.Literal; + (match x with + | @expr.Ident _ _ _ t idc => + match x0 with + | @expr.Ident _ _ _ t0 idc0 => + match x1 with + | @expr.Ident _ _ _ t1 idc1 => + match x2 with + | @expr.Ident _ _ _ t2 idc2 => + args <- invert_bind_args idc2 Raw.ident.Literal; + args0 <- invert_bind_args idc1 Raw.ident.Literal; + args1 <- invert_bind_args idc0 Raw.ident.Literal; + args2 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args2) -> (projT1 args1)) -> + (projT1 args0)) -> (projT1 args))%ptype option + (fun x3 : option => x3) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args2) -> (projT1 args1)) -> + (projT1 args0)) -> (projT1 args))%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args2); + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args1); + idc_args1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + idc_args2 <- ident.unify pattern.ident.Literal + ##(projT2 args); + Some + (Base + (let + '(a2, b2)%zrange := + Z.add_with_get_carry_full + (let (x3, _) := idc_args in x3) + (let (x3, _) := idc_args0 in x3) + (let (x3, _) := idc_args1 in x3) + (let (x3, _) := idc_args2 in x3) in + ((##a2)%expr, (##b2)%expr)%expr_pat)) + else None + | None => None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t2 idc2) x3 => + args <- invert_bind_args idc2 Raw.ident.Z_cast; + args0 <- invert_bind_args idc1 Raw.ident.Literal; + args1 <- invert_bind_args idc0 Raw.ident.Literal; + args2 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args2) -> (projT1 args1)) -> + (projT1 args0)) -> s)%ptype option + (fun x4 : option => x4) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args2) -> (projT1 args1)) -> + (projT1 args0)) -> s)%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args2); + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args1); + idc_args1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + v <- type.try_make_transport_cps s ℤ; + x4 <- (if + ((let (x4, _) := idc_args0 in x4) =? 0) && + ((let (x4, _) := idc_args1 in x4) =? 0) && + (ZRange.normalize args <=? + r[0 ~> (let (x4, _) := idc_args in x4) - 1])%zrange + then + Some + (#(Z_cast args)%expr @ + v (Compile.reflect x3), (##0)%expr)%expr_pat + else None); + Some (Base x4) + else None + | None => None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ + (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ + (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t1 idc1) x3 => + match x2 with + | @expr.Ident _ _ _ t2 idc2 => + args <- invert_bind_args idc2 Raw.ident.Literal; + args0 <- invert_bind_args idc1 Raw.ident.Z_cast; + args1 <- invert_bind_args idc0 Raw.ident.Literal; + args2 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted_cps + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args2) -> (projT1 args1)) -> s) -> + (projT1 args))%ptype option (fun x4 : option => x4) + with + | Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args2) -> (projT1 args1)) -> s) -> + (projT1 args))%ptype + then + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args2); + idc_args0 <- ident.unify pattern.ident.Literal + ##(projT2 args1); + v <- type.try_make_transport_cps s ℤ; + idc_args1 <- ident.unify pattern.ident.Literal + ##(projT2 args); + x4 <- (if + ((let (x4, _) := idc_args0 in x4) =? 0) && + ((let (x4, _) := idc_args1 in x4) =? 0) && + (ZRange.normalize args0 <=? + r[0 ~> (let (x4, _) := idc_args in x4) - 1])%zrange + then + Some + (#(Z_cast args0)%expr @ + v (Compile.reflect x3), (##0)%expr)%expr_pat + else None); + Some (Base x4) + else None + | None => None + end + | _ => None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ + (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ + (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end + | _ => None + end + | _ => None + end;;; + Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option +| Z_sub_get_borrow => + fun x x0 x1 : expr ℤ => + Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat +| Z_sub_with_get_borrow => + fun x x0 x1 x2 : expr ℤ => + Base (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat +| Z_zselect => + fun x x0 x1 : expr ℤ => Base (#(Z_zselect)%expr @ x @ x0 @ x1)%expr_pat +| Z_add_modulo => + fun x x0 x1 : expr ℤ => + Base (#(Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat +| Z_rshi => + fun x x0 x1 x2 : expr ℤ => + Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat +| 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 + idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); + x0 <- (if + is_bounded_by_bool (let (x0, _) := idc_args in x0) + range + then Some (##(let (x0, _) := idc_args in x0))%expr + else None); + Some (Base x0) + 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 ℤ; + 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) + 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 + (fv <-- 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 fv)%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 - (((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype option - (fun x4 : option => x4) + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s4) -> s)%ptype option (fun x6 : option => x6) with - | Some (_, _, _, _) => + | Some (_, _, _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype + ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s4) -> s)%ptype then - idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - v <- type.try_make_transport_cps s ℤ; - fv <- (if (let (x4, _) := idc_args in x4) <? 0 + 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_sub_with_get_borrow)%expr @ x @ - (##(- (let (x4, _) := idc_args in x4))%Z)%expr @ - x2 @ v (Compile.reflect x3))%expr_pat + (#(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 - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) + (#(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.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat - _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@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 x2 with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x3 => - (_ <- invert_bind_args idc0 Raw.ident.Z_opp; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype option - (fun x4 : option => x4) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype - then - idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - v <- type.try_make_transport_cps s ℤ; - fv <- (if (let (x4, _) := idc_args in x4) =? 0 - then - Some - (UnderLet - (#(Z_sub_get_borrow)%expr @ x @ x1 @ - v (Compile.reflect x3))%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end);; - _ <- invert_bind_args idc0 Raw.ident.Z_opp; - args0 <- invert_bind_args idc Raw.ident.Literal; + 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 - (((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype option - (fun x4 : option => x4) + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> s4)%ptype option (fun x6 : option => x6) with - | Some (_, _, _, _) => + | Some (_, _, _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype + ((ℤ -> ℤ) -> ℤ)%ptype ((s1 -> s0) -> s4)%ptype then - idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - v <- type.try_make_transport_cps s ℤ; - fv <- (if (let (x4, _) := idc_args in x4) <? 0 + 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_sub_with_get_borrow)%expr @ x @ - (##(- (let (x4, _) := idc_args in x4))%Z)%expr @ - x1 @ v (Compile.reflect x3))%expr_pat + (#(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 - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) + (#(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.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat - _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@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; - args0 <- invert_bind_args idc Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> (projT1 args)) -> ℤ)%ptype - option (fun x3 : option => x3) + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> (projT1 args)) -> s)%ptype option + (fun x3 : option => x3) with - | Some (_, _, _, _) => + | Some (_, _, _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> (projT1 args)) -> ℤ)%ptype + ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> (projT1 args)) -> s)%ptype then + v <- type.try_make_transport_cps s1 ℤ; idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - fv <- (if - ((let (x3, _) := idc_args0 in x3) <=? 0) && - ((let (x3, _) := idc_args in x3) <=? 0) && - ((let (x3, _) := idc_args0 in x3) + - (let (x3, _) := idc_args in x3) <? 0) + ##(projT2 args); + v0 <- type.try_make_transport_cps s ℤ; + fv <- (if (let (x3, _) := idc_args in x3) <? 0 then Some (UnderLet - (#(Z_sub_with_get_borrow)%expr @ x @ - (##(- (let (x3, _) := idc_args in x3))%Z)%expr @ - x2 @ - (##(- (let (x3, _) := idc_args0 in x3))%Z)%expr)%expr_pat + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + v (Compile.reflect x2) @ + v0 (Compile.reflect x0) @ + (##(- (let (x3, _) := idc_args in x3))%Z)%expr))%expr_pat (fun vc : var (ℤ * ℤ)%etype => Base - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) + (#(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 @@ -948,42 +1207,52 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end;; - match x2 with + match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> ℤ) -> (projT1 args))%ptype - option (fun x3 : option => x3) + pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> (projT1 args))%ptype option + (fun x3 : option => x3) with - | Some (_, _, _, _) => + | Some (_, _, _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args0)) -> ℤ) -> (projT1 args))%ptype + ((ℤ -> ℤ) -> ℤ)%ptype + ((s1 -> s0) -> (projT1 args))%ptype then + v <- type.try_make_transport_cps s1 ℤ; + v0 <- type.try_make_transport_cps s0 ℤ; idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - fv <- (if - ((let (x3, _) := idc_args0 in x3) <=? 0) && - ((let (x3, _) := idc_args in x3) <=? 0) && - ((let (x3, _) := idc_args0 in x3) + - (let (x3, _) := idc_args in x3) <? 0) + ##(projT2 args); + fv <- (if (let (x3, _) := idc_args in x3) <? 0 then Some (UnderLet - (#(Z_sub_with_get_borrow)%expr @ x @ - (##(- (let (x3, _) := idc_args in x3))%Z)%expr @ - x1 @ - (##(- (let (x3, _) := idc_args0 in x3))%Z)%expr)%expr_pat + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + v (Compile.reflect x2) @ + v0 (Compile.reflect x1) @ + (##(- (let (x3, _) := idc_args in x3))%Z)%expr))%expr_pat (fun vc : var (ℤ * ℤ)%etype => Base - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) + (#(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 @@ -992,405 +1261,1103 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end;; - match x with + _ <- 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) + 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_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)) + else None + | None => None + 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 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 ℤ; + idc_args <- 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, _) := idc_args 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 ℤ; + idc_args <- 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, _) := idc_args 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, _) := idc_args 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; + _ <- 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 ℤ; + idc_args <- 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, _) := idc_args 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 ℤ; + idc_args <- 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, _) := idc_args 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, _) := idc_args 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_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; - args1 <- invert_bind_args idc Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args0) -> (projT1 args1)) -> (projT1 args)) -> - ℤ)%ptype option (fun x3 : option => x3) + (((s2 -> (projT1 args0)) -> (projT1 args)) -> s)%ptype + option (fun x4 : option => x4) with - | Some (_, _, _, _) => + | Some (_, _, _, _)%zrange => if type.type_beq base.type base.type.type_beq (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args0) -> (projT1 args1)) -> - (projT1 args)) -> ℤ)%ptype + (((s2 -> (projT1 args0)) -> (projT1 args)) -> s)%ptype then - _ <- ident.unify pattern.ident.Literal - ##(projT2 args0); + v <- type.try_make_transport_cps s2 ℤ; + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args1); - idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); - x3 <- (if - ((let (x3, _) := idc_args0 in x3) =? 0) && - ((let (x3, _) := idc_args1 in x3) =? 0) - then Some (x2, (##0)%expr)%expr_pat + v0 <- type.try_make_transport_cps s ℤ; + fv <- (if + ((let (x4, _) := idc_args0 in x4) <=? 0) && + ((let (x4, _) := idc_args in x4) <=? 0) && + ((let (x4, _) := idc_args0 in x4) + + (let (x4, _) := idc_args 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, _) := idc_args in x4))%Z)%expr @ + v0 (Compile.reflect x0) @ + (##(- (let (x4, _) := idc_args0 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_pat)%expr)%expr_pat)) else None); - Some (Base x3) + Some (fv0 <-- fv; + Base fv0)%under_lets else None | None => None end | _ => None end;; - match x2 with + match x0 with | @expr.Ident _ _ _ t1 idc1 => args <- invert_bind_args idc1 Raw.ident.Literal; args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args0) -> (projT1 args1)) -> ℤ) -> - (projT1 args))%ptype option (fun x3 : option => x3) + (((s2 -> (projT1 args0)) -> s0) -> (projT1 args))%ptype + option (fun x4 : option => x4) with - | Some (_, _, _, _) => + | Some (_, _, _, _)%zrange => if type.type_beq base.type base.type.type_beq (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args0) -> (projT1 args1)) -> ℤ) -> - (projT1 args))%ptype + (((s2 -> (projT1 args0)) -> s0) -> (projT1 args))%ptype then - _ <- ident.unify pattern.ident.Literal - ##(projT2 args0); + v <- type.try_make_transport_cps s2 ℤ; + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args0); + v0 <- type.try_make_transport_cps s0 ℤ; idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args1); - idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); - x3 <- (if - ((let (x3, _) := idc_args0 in x3) =? 0) && - ((let (x3, _) := idc_args1 in x3) =? 0) - then Some (x1, (##0)%expr)%expr_pat + fv <- (if + ((let (x4, _) := idc_args0 in x4) <=? 0) && + ((let (x4, _) := idc_args in x4) <=? 0) && + ((let (x4, _) := idc_args0 in x4) + + (let (x4, _) := idc_args 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, _) := idc_args in x4))%Z)%expr @ + v0 (Compile.reflect x1) @ + (##(- (let (x4, _) := idc_args0 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_pat)%expr)%expr_pat)) else None); - Some (Base x3) + Some (fv0 <-- fv; + Base fv0)%under_lets else None | None => None end | _ => None - end - | _ => None - end;; - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args)) -> ℤ) -> ℤ)%ptype option - (fun x3 : option => x3) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> (projT1 args)) -> ℤ) -> ℤ)%ptype - then - idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (if (let (x3, _) := idc_args in x3) =? 0 - then - Some - (UnderLet - (#(Z_add_get_carry)%expr @ x @ x1 @ x2)%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($vc)%expr, - #(snd)%expr @ ($vc)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x3 => - match x1 with - | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 => - _ <- invert_bind_args idc0 Raw.ident.Z_opp; - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> s) -> s0) -> ℤ)%ptype - option (fun x5 : option => x5) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> s) -> s0) -> ℤ)%ptype - then - v <- type.try_make_transport_cps s ℤ; - v0 <- type.try_make_transport_cps s0 ℤ; - Some - (UnderLet - (#(Z_sub_with_get_borrow)%expr @ x @ - v (Compile.reflect x3) @ x2 @ - v0 (Compile.reflect x4))%expr_pat - (fun v1 : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v1)%expr, - (- (#(snd)%expr @ $v1)%expr_pat)%expr)%expr_pat)) - else None - | None => None - end - | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ - (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;; - match x2 with - | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 => - _ <- invert_bind_args idc0 Raw.ident.Z_opp; - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> s) -> ℤ) -> s0)%ptype - option (fun x5 : option => x5) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> s) -> ℤ) -> s0)%ptype - then - v <- type.try_make_transport_cps s ℤ; - v0 <- type.try_make_transport_cps s0 ℤ; - Some - (UnderLet - (#(Z_sub_with_get_borrow)%expr @ x @ - v (Compile.reflect x3) @ x1 @ - v0 (Compile.reflect x4))%expr_pat - (fun v1 : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v1)%expr, - (- (#(snd)%expr @ $v1)%expr_pat)%expr)%expr_pat)) - else None - | None => None - end - | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ - (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t0 idc0 => + end;; args <- invert_bind_args idc0 Raw.ident.Literal; - _ <- invert_bind_args idc Raw.ident.Z_opp; + _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> s) -> (projT1 args)) -> ℤ)%ptype option + (((s2 -> (projT1 args)) -> s0) -> s)%ptype option (fun x4 : option => x4) with - | Some (_, _, _, _) => + | Some (_, _, _, _)%zrange => if type.type_beq base.type base.type.type_beq (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> s) -> (projT1 args)) -> ℤ)%ptype + (((s2 -> (projT1 args)) -> s0) -> s)%ptype then - v <- type.try_make_transport_cps s ℤ; + v <- type.try_make_transport_cps s2 ℤ; idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (if (let (x4, _) := idc_args in x4) <=? 0 + v0 <- type.try_make_transport_cps s0 ℤ; + v1 <- type.try_make_transport_cps s ℤ; + fv <- (if (let (x4, _) := idc_args in x4) =? 0 then Some (UnderLet - (#(Z_sub_with_get_borrow)%expr @ x @ - v (Compile.reflect x3) @ x2 @ - (##(- (let (x4, _) := idc_args in x4))%Z)%expr)%expr_pat + (#(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 - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) + (#(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 - | _ => None - end;; - match x2 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - _ <- invert_bind_args idc Raw.ident.Z_opp; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> s) -> ℤ) -> (projT1 args))%ptype option - (fun x4 : option => x4) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> s) -> ℤ) -> (projT1 args))%ptype - then - v <- type.try_make_transport_cps s ℤ; - idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args); - fv <- (if (let (x4, _) := idc_args in x4) <=? 0 + | @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 - Some - (UnderLet - (#(Z_sub_with_get_borrow)%expr @ x @ - v (Compile.reflect x3) @ x1 @ - (##(- (let (x4, _) := idc_args in x4))%Z)%expr)%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($vc)%expr, - (- (#(snd)%expr @ $vc)%expr_pat)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None - end - | _ => None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;; - match x1 with - | @expr.Ident _ _ _ t idc => - match x2 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> ℤ) -> (projT1 args0)) -> (projT1 args))%ptype - option (fun x3 : option => x3) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> ℤ) -> (projT1 args0)) -> (projT1 args))%ptype - then - idc_args <- ident.unify pattern.ident.Literal - ##(projT2 args0); - idc_args0 <- ident.unify pattern.ident.Literal - ##(projT2 args); - fv <- (if - ((let (x3, _) := idc_args in x3) =? 0) && - ((let (x3, _) := idc_args0 in x3) =? 0) + 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_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 - Some - (UnderLet - (#(Z_add_with_get_carry)%expr @ x @ x0 @ - (##(let (x3, _) := idc_args in x3))%expr @ - (##(let (x3, _) := idc_args0 in x3))%expr)%expr_pat - (fun vc : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($vc)%expr, (##0)%expr)%expr_pat)) - else None); - Some (fv0 <-- fv; - Base fv0)%under_lets - else None - | None => None + 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_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 ℤ; + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args); + v1 <- type.try_make_transport_cps s ℤ; + fv <- (if + ((let (x7, _) := idc_args 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, _) := idc_args 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 ℤ; + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args); + fv <- (if + ((let (x7, _) := idc_args 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, _) := idc_args 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 + idc_args <- ident.unify pattern.ident.Literal + ##(projT2 args1); + v <- type.try_make_transport_cps s3 ℤ; + idc_args0 <- ident.unify + pattern.ident.Literal + ##(projT2 args0); + idc_args1 <- ident.unify + pattern.ident.Literal + ##(projT2 args); + fv <- (if + ((let (x5, _) := idc_args0 in x5) =? + 0) && + ((let (x5, _) := idc_args1 in x5) =? + 0) && + (ZRange.normalize args2 <=? + r[0 ~> (let (x5, _) := idc_args 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, _) := idc_args in + x5))%expr @ + (#(Z_cast args2)%expr @ + v (Compile.reflect x4)) @ + (##(let (x5, _) := + idc_args0 in + x5))%expr @ + (##(let (x5, _) := + idc_args1 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 - | _ => None - end;; - match - pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype option (fun x3 : option => x3) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - then - Some - (UnderLet - (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat - (fun v : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v)%expr, #(snd)%expr @ ($v)%expr)%expr_pat)) - else None - | None => None - end);; + 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; + 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;; None);;; - Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option -| Z_sub_get_borrow => - fun x x0 x1 : expr ℤ => - (match - pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2) - with - | Some (_, _, _) => - if - type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype - ((ℤ -> ℤ) -> ℤ)%ptype - then - Some - (UnderLet (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat - (fun v : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v)%expr, #(snd)%expr @ ($v)%expr)%expr_pat)) - else None - | None => None - end;;; - Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_sub_with_get_borrow => - fun x x0 x1 x2 : expr ℤ => - (match - pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype option (fun x3 : option => x3) - with - | Some (_, _, _, _) => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - then - Some - (UnderLet - (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat - (fun v : var (ℤ * ℤ)%etype => - Base - (#(fst)%expr @ ($v)%expr, #(snd)%expr @ ($v)%expr)%expr_pat)) - else None - | None => None - end;;; - Base (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option -| Z_zselect => - fun x x0 x1 : expr ℤ => Base (#(Z_zselect)%expr @ x @ x0 @ x1)%expr_pat -| Z_add_modulo => - fun x x0 x1 : expr ℤ => - Base (#(Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat -| Z_rshi => - fun x x0 x1 x2 : expr ℤ => - Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat -| 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.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 ℤ; - 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) - else None - | None => None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None - | _ => None - end;;; - Base (#(Z_cast range)%expr @ x)%expr_pat)%option -| Z_cast2 range => - fun x : expr (ℤ * ℤ)%etype => Base (#(Z_cast2 range)%expr @ x)%expr_pat + Base (#(Z_cast2 range)%expr @ x)%expr_pat)%option | fancy_add log2wordmax imm => fun x : expr (ℤ * ℤ)%etype => Base (#(fancy_add log2wordmax imm)%expr @ x)%expr_pat diff --git a/src/Experiments/NewPipeline/nbe_rewrite_head.out b/src/Experiments/NewPipeline/nbe_rewrite_head.out index 076992962..2eb887afe 100644 --- a/src/Experiments/NewPipeline/nbe_rewrite_head.out +++ b/src/Experiments/NewPipeline/nbe_rewrite_head.out @@ -3002,9 +3002,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with if type.type_beq base.type base.type.type_beq ℤ (projT1 args) then idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); - Some - (Base - (##(Definitions.Z.bneg (let (x0, _) := idc_args in x0)))%expr) + Some (Base (##(Z.bneg (let (x0, _) := idc_args in x0)))%expr) else None | None => None end @@ -3036,8 +3034,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args); Some (Base - (##(Definitions.Z.lnot_modulo - (let (x1, _) := idc_args in x1) + (##(Z.lnot_modulo (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) else None | None => None @@ -3080,8 +3077,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (Base (let '(a1, b1)%zrange := - Definitions.Z.mul_split - (let (x2, _) := idc_args in x2) + Z.mul_split (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2) in ((##a1)%expr, (##b1)%expr)%expr_pat)) @@ -3128,7 +3124,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (Base (let '(a1, b1)%zrange := - Definitions.Z.add_get_carry_full + Z.add_get_carry_full (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2) in @@ -3174,7 +3170,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args); Some (Base - (##(Definitions.Z.add_with_carry + (##(Z.add_with_carry (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2)))%expr) @@ -3229,7 +3225,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (Base (let '(a2, b2)%zrange := - Definitions.Z.add_with_get_carry_full + Z.add_with_get_carry_full (let (x3, _) := idc_args in x3) (let (x3, _) := idc_args0 in x3) (let (x3, _) := idc_args1 in x3) @@ -3280,7 +3276,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (Base (let '(a1, b1)%zrange := - Definitions.Z.sub_get_borrow_full + Z.sub_get_borrow_full (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2) in @@ -3336,7 +3332,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (Base (let '(a2, b2)%zrange := - Definitions.Z.sub_with_get_borrow_full + Z.sub_with_get_borrow_full (let (x3, _) := idc_args in x3) (let (x3, _) := idc_args0 in x3) (let (x3, _) := idc_args1 in x3) @@ -3385,8 +3381,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args); Some (Base - (##(Definitions.Z.zselect - (let (x2, _) := idc_args in x2) + (##(Z.zselect (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2)))%expr) else None @@ -3430,8 +3425,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args); Some (Base - (##(Definitions.Z.add_modulo - (let (x2, _) := idc_args in x2) + (##(Z.add_modulo (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2)))%expr) else None @@ -3483,8 +3477,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args); Some (Base - (##(Definitions.Z.rshi - (let (x3, _) := idc_args in x3) + (##(Z.rshi (let (x3, _) := idc_args in x3) (let (x3, _) := idc_args0 in x3) (let (x3, _) := idc_args1 in x3) (let (x3, _) := idc_args2 in x3)))%expr) @@ -3525,8 +3518,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args); Some (Base - (##(Definitions.Z.cc_m - (let (x1, _) := idc_args in x1) + (##(Z.cc_m (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) else None | None => None |