aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-10-30 16:58:15 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2018-11-11 11:55:00 -0500
commit56c498de53c503222806dfc2399a117802d1b290 (patch)
tree343d6649d84a0cb76d66800e2c183a9ffe8c6491 /src
parent5a2bb6ac51fe7db51e06bd5d74d21541bb43a2da (diff)
Split off all of the arithmetic rules that need bounds info
Because we need to do extra passes of DCE and subst01 to fully reduce things, we generalize some of the interp proofs over cast behavior. For ease of rewriting, we make [ident.interp] an alias (notation) for [ident.gen_interp], rather than a [Definition]. We also factor out the rewriting wrapper inside the pipeline module into its own definition. After | File Name | Before || Change | % Change --------------------------------------------------------------------------------------------------------------------- 32m09.80s | Total | 26m07.22s || +6m02.58s | +23.13% --------------------------------------------------------------------------------------------------------------------- 6m41.53s | p384_32.c | 0m28.22s || +6m13.30s | +1322.85% 1m19.67s | Experiments/NewPipeline/Rewriter.vo | 2m22.97s || -1m03.29s | -44.27% 0m21.90s | secp256k1_32.c | 0m06.46s || +0m15.43s | +239.00% 0m21.24s | p256_32.c | 0m06.32s || +0m14.91s | +236.07% 6m18.26s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m13.65s || +0m04.61s | +1.23% 0m14.12s | p384_64.c | 0m10.22s || +0m03.89s | +38.16% 0m07.86s | p224_32.c | 0m03.92s || +0m03.94s | +100.51% 4m34.19s | Experiments/NewPipeline/Toplevel1.vo | 4m37.15s || -0m02.95s | -1.06% 1m41.50s | Experiments/NewPipeline/Toplevel2.vo | 1m38.62s || +0m02.87s | +2.92% 0m37.69s | p521_64.c | 0m35.62s || +0m02.07s | +5.81% 0m29.75s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m27.09s || +0m02.66s | +9.81% 0m17.88s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m15.52s || +0m02.35s | +15.20% 1m47.75s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m46.74s || +0m01.00s | +0.94% 0m44.38s | p521_32.c | 0m42.47s || +0m01.91s | +4.49% 0m43.92s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m41.97s || +0m01.95s | +4.64% 0m24.99s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m26.52s || -0m01.53s | -5.76% 0m20.62s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m22.26s || -0m01.64s | -7.36% 0m11.42s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m12.88s || -0m01.46s | -11.33% 0m08.44s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m07.12s || +0m01.31s | +18.53% 1m50.48s | Experiments/NewPipeline/RewriterWf2.vo | 1m50.18s || +0m00.29s | +0.27% 1m15.53s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m15.26s || +0m00.26s | +0.35% 0m43.94s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m43.00s || +0m00.93s | +2.18% 0m10.25s | Experiments/NewPipeline/RewriterWf1.vo | 0m10.46s || -0m00.21s | -2.00% 0m07.27s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m07.41s || -0m00.14s | -1.88% 0m06.29s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m05.75s || +0m00.54s | +9.39% 0m05.54s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m06.24s || -0m00.70s | -11.21% 0m04.86s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m05.62s || -0m00.75s | -13.52% 0m02.86s | curve25519_32.c | 0m02.43s || +0m00.42s | +17.69% 0m02.80s | secp256k1_64.c | 0m02.29s || +0m00.50s | +22.27% 0m02.74s | p256_64.c | 0m02.67s || +0m00.07s | +2.62% 0m02.13s | curve25519_64.c | 0m02.38s || -0m00.25s | -10.50% 0m01.97s | p224_64.c | 0m01.86s || +0m00.10s | +5.91% 0m01.46s | Experiments/NewPipeline/CLI.vo | 0m01.52s || -0m00.06s | -3.94% 0m01.36s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.25s || +0m00.11s | +8.80% 0m01.22s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.19s || +0m00.03s | +2.52% 0m01.02s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.05s || -0m00.03s | -2.85% 0m00.97s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.94s || +0m00.03s | +3.19%
Diffstat (limited to 'src')
-rw-r--r--src/Experiments/NewPipeline/Rewriter.v30
-rw-r--r--src/Experiments/NewPipeline/RewriterRulesInterpGood.v14
-rw-r--r--src/Experiments/NewPipeline/Toplevel1.v3
-rw-r--r--src/Experiments/NewPipeline/arith_rewrite_head.out1114
-rw-r--r--src/Experiments/NewPipeline/arith_with_casts_rewrite_head.out1122
5 files changed, 1196 insertions, 1087 deletions
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index b8c8bdead..b3ab11159 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -1773,6 +1773,23 @@ Module Compilers.
; make_rewriteo (#?ℤ * (?? * ??)) (fun c x y => (x * (y * ##c)) when (Z.abs c <=? Z.abs max_const_val))
; make_rewriteo (#?ℤ * ??) (fun c x => (x * ##c) when (Z.abs c <=? Z.abs max_const_val))
+ ; make_rewrite_step (* _step, so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *)
+ (#pattern.ident.Z_cast2 @ (??, ??)) (fun r x y => (#(ident.Z_cast (fst r)) @ $x, #(ident.Z_cast (snd r)) @ $y))
+
+ ; 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 *)
+ ].
+
+ 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 v => -v when z =? 0)
+
+ ; make_rewriteo (#?ℤ << ??) (fun x y => ##0 when x =? 0)
+
+ ; make_rewrite (-(-??)) (fun v => v)
+
; 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)
@@ -1900,19 +1917,10 @@ Module Compilers.
(fun s x y => (llet vc := #ident.Z_mul_split @ s @ x @ y in
(#ident.fst @ $vc, #ident.snd @ $vc)))
-
- ; make_rewrite_step (* _step, so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *)
- (#pattern.ident.Z_cast2 @ (??, ??)) (fun r x y => (#(ident.Z_cast (fst r)) @ $x, #(ident.Z_cast (snd r)) @ $y))
-
- ; 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 *)
- ].
-
- 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
(#pattern.ident.Z_cast @ (#pattern.ident.Z_cast @ ??))
- (fun r1 r2 x => #(ident.Z_cast r2) @ x when ZRange.is_tighter_than_bool (ZRange.normalize r2) (ZRange.normalize r1))].
+ (fun r1 r2 x => #(ident.Z_cast r2) @ x when ZRange.is_tighter_than_bool (ZRange.normalize r2) (ZRange.normalize r1))
+ ].
Definition nbe_dtree'
:= Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 nbe_rewrite_rules.
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 2bad756c9..b205acec1 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -345,6 +345,13 @@ Module Compilers.
Proof using Type.
Time start_interp_good.
Time all: try solve [ repeat interp_good_t_step; (lia + nia) ].
+ Qed.
+
+ Lemma arith_with_casts_rewrite_rules_interp_good
+ : 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
@@ -459,13 +466,6 @@ subgoal 9 (ID 33473) is:
1-9: exact admit.
Qed.
- Lemma arith_with_casts_rewrite_rules_interp_good
- : 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) ].
- Qed.
-
Local Ltac fancy_local_t :=
repeat first [ match goal with
| [ H : forall s v v', ?invert_low s v = Some v' -> v = _,
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index d4a4cc35f..390683b93 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -714,6 +714,7 @@ 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
@@ -723,7 +724,7 @@ Module Pipeline.
let E' := CheckedPartialEvaluateWithBounds relax_zrange E arg_bounds out_bounds in
match E' with
| inl E
- => let E := RewriteRules.RewriteArithWithCasts 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 43d55747c..c27f9feda 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))%zrange =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
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))%zrange =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, (_, (_, _)))%zrange =>
+ | Some (_, (_, (_, _))) =>
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 (_, (_, (_, _)))%zrange =>
+ | Some (_, (_, (_, _))) =>
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 (_, (_, _))%zrange =>
+ | Some (_, (_, _)) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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_cast x)
+ fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp 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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
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 (_, _)%zrange =>
+ | Some (_, _) =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -1536,1022 +1536,22 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| Z_lnot_modulo =>
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 (_, _, _)%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 (_, _, _)%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 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) =? 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 (_, _, _)%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) =? 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 (_, _, _)%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) =? -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 (_, _, _)%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) =? -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 (_, _, _)%zrange =>
- 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);;
- None);;;
- Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat)%option
+ fun x x0 x1 : expr ℤ => Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
| 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 (_, _, _)%zrange =>
- 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 (_, _, _)%zrange =>
- 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 (_, _, _)%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);
- 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 (_, _, _)%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);
- 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 (_, _, _)%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 (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 (_, _, _)%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, (##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 (_, _, _)%zrange =>
- 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);;
- None);;;
- Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat)%option
+ Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
| 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 (_, _, _)%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;;
- match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
- with
- | Some (_, _, _)%zrange =>
- 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);;;
- Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat)%option
+ Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
| 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 (_, _, _, _)%zrange =>
- 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
- pattern.type.unify_extracted_cps
- (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype option
- (fun x4 : option => x4)
- with
- | Some (_, _, _, _)%zrange =>
- 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_with_get_borrow)%expr @ x @
- (##(- (let (x4, _) := idc_args in x4))%Z)%expr @
- 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
- | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
- (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat
- _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => 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 (_, _, _, _)%zrange =>
- 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
- pattern.type.unify_extracted_cps
- (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype option
- (fun x4 : option => x4)
- with
- | Some (_, _, _, _)%zrange =>
- 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_with_get_borrow)%expr @ x @
- (##(- (let (x4, _) := idc_args in x4))%Z)%expr @
- 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
- | @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 _ _ _ 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 (_, _, _, _)%zrange =>
- 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_args0 in x3) <=? 0) &&
- ((let (x3, _) := idc_args in x3) <=? 0) &&
- ((let (x3, _) := idc_args0 in x3) +
- (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
- (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 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 (_, _, _, _)%zrange =>
- 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_args0 in x3) <=? 0) &&
- ((let (x3, _) := idc_args in x3) <=? 0) &&
- ((let (x3, _) := idc_args0 in x3) +
- (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
- (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 x 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 args0) -> (projT1 args1)) -> (projT1 args)) ->
- ℤ)%ptype option (fun x3 : option => x3)
- with
- | Some (_, _, _, _)%zrange =>
- if
- type.type_beq base.type base.type.type_beq
- (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- ((((projT1 args0) -> (projT1 args1)) ->
- (projT1 args)) -> ℤ)%ptype
- then
- _ <- 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
- else None);
- Some (Base x3)
- else None
- | None => None
- end
- | _ => None
- end;;
- match x2 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 args0) -> (projT1 args1)) -> ℤ) ->
- (projT1 args))%ptype option (fun x3 : option => x3)
- with
- | Some (_, _, _, _)%zrange =>
- if
- type.type_beq base.type base.type.type_beq
- (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- ((((projT1 args0) -> (projT1 args1)) -> ℤ) ->
- (projT1 args))%ptype
- then
- _ <- 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 (x1, (##0)%expr)%expr_pat
- else None);
- Some (Base x3)
- 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 (_, _, _, _)%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);
- 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 (_, _, _, _)%zrange =>
- 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 (_, _, _, _)%zrange =>
- 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 =>
- 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 (_, _, _, _)%zrange =>
- 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
- 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
- (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 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 (_, _, _, _)%zrange =>
- 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
- 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 (_, _, _, _)%zrange =>
- 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)
- 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
- end
- | _ => None
- end
- | _ => None
- end;;
- match
- pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype option (fun x3 : option => x3)
- with
- | Some (_, _, _, _)%zrange =>
- 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);;
- None);;;
- Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option
+ Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
| Z_sub_get_borrow =>
fun x x0 x1 : expr ℤ =>
- (match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
- with
- | Some (_, _, _)%zrange =>
- 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
+ Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
| 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 (_, _, _, _)%zrange =>
- 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
+ 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 =>
@@ -2576,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 (_, (_, (_, _)), _, _)%zrange =>
+ | Some (_, (_, (_, _)), _, _) =>
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 c08cfc083..cdcbf9e3b 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))%zrange =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
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))%zrange =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
if
type.type_beq base.type base.type.type_beq
(((b3 * b2)%etype -> b2) ->
@@ -216,8 +216,84 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| Z_add => fun x x0 : expr ℤ => Base (x + x0)%expr
| Z_mul => fun x x0 : expr ℤ => Base (x * x0)%expr
| Z_pow => fun x x0 : expr ℤ => Base (#(Z_pow)%expr @ x @ x0)%expr_pat
-| Z_sub => fun x x0 : expr ℤ => Base (x - x0)%expr
-| Z_opp => fun x : expr ℤ => Base (- x)%expr
+| Z_sub =>
+ fun x x0 : expr ℤ =>
+ ((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;
+ match
+ pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> s)%ptype option (fun x2 : option => x2)
+ 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 ℤ;
+ x2 <- (if (let (x2, _) := idc_args in x2) =? 0
+ then Some (v (Compile.reflect x1))
+ else None);
+ Some (Base x2)
+ 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;;
+ args <- invert_bind_args idc Raw.ident.Literal;
+ match
+ pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
+ 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);
+ x1 <- (if (let (x1, _) := idc_args in x1) =? 0
+ then Some (- x0)%expr
+ else None);
+ Some (Base x1)
+ else None
+ | None => None
+ end
+ | _ => None
+ end;;
+ None);;;
+ Base (x - x0)%expr)%option
+| Z_opp =>
+ fun x : expr ℤ =>
+ ((match x with
+ | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x0 =>
+ _ <- invert_bind_args idc Raw.ident.Z_opp;
+ 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 ℤ;
+ Some (Base (v (Compile.reflect x0)))
+ 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;;
+ None);;;
+ Base (- x)%expr)%option
| Z_div => fun x x0 : expr ℤ => Base (x / x0)%expr
| Z_modulo => fun x x0 : expr ℤ => Base (x mod x0)%expr
| Z_log2 => fun x : expr ℤ => Base (#(Z_log2)%expr @ x)%expr_pat
@@ -228,29 +304,1053 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| Z_of_nat => fun x : expr ℕ => Base (#(Z_of_nat)%expr @ x)%expr_pat
| Z_to_nat => fun x : expr ℤ => Base (#(Z_to_nat)%expr @ x)%expr_pat
| Z_shiftr => fun x x0 : expr ℤ => Base (x >> x0)%expr
-| Z_shiftl => fun x x0 : expr ℤ => Base (x << x0)%expr
+| Z_shiftl =>
+ fun x x0 : 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 x1 : option => x1)
+ 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);
+ x1 <- (if (let (x1, _) := idc_args in x1) =? 0
+ then Some (##0)%expr
+ else None);
+ Some (Base x1)
+ else None
+ | None => None
+ end
+ | _ => None
+ end;;;
+ Base (x << x0)%expr)%option
| Z_land => fun x x0 : expr ℤ => Base (x &' x0)%expr
| Z_lor => fun x x0 : expr ℤ => Base (x || x0)%expr
| Z_bneg => fun x : expr ℤ => Base (#(Z_bneg)%expr @ x)%expr_pat
| Z_lnot_modulo =>
fun x x0 : expr ℤ => Base (#(Z_lnot_modulo)%expr @ x @ x0)%expr_pat
| Z_mul_split =>
- fun x x0 x1 : expr ℤ => Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
+ 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;
+ 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 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);;
+ None);;;
+ Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat)%option
| Z_add_get_carry =>
fun x x0 x1 : expr ℤ =>
- Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
+ (((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);;
+ None);;;
+ Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat)%option
| Z_add_with_carry =>
fun x x0 x1 : expr ℤ =>
- Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
+ (((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);;;
+ Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat)%option
| Z_add_with_get_carry =>
fun x x0 x1 x2 : expr ℤ =>
- Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
+ (((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
+ 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_with_get_borrow)%expr @ x @
+ (##(- (let (x4, _) := idc_args in x4))%Z)%expr @
+ 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
+ | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _
+ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat
+ _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => 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
+ 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_with_get_borrow)%expr @ x @
+ (##(- (let (x4, _) := idc_args in x4))%Z)%expr @
+ 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
+ | @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 _ _ _ 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_args0 in x3) <=? 0) &&
+ ((let (x3, _) := idc_args in x3) <=? 0) &&
+ ((let (x3, _) := idc_args0 in x3) +
+ (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
+ (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 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_args0 in x3) <=? 0) &&
+ ((let (x3, _) := idc_args in x3) <=? 0) &&
+ ((let (x3, _) := idc_args0 in x3) +
+ (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
+ (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 x 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 args0) -> (projT1 args1)) -> (projT1 args)) ->
+ ℤ)%ptype option (fun x3 : option => x3)
+ with
+ | Some (_, _, _, _) =>
+ if
+ type.type_beq base.type base.type.type_beq
+ (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ ((((projT1 args0) -> (projT1 args1)) ->
+ (projT1 args)) -> ℤ)%ptype
+ then
+ _ <- 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
+ else None);
+ Some (Base x3)
+ else None
+ | None => None
+ end
+ | _ => None
+ end;;
+ match x2 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 args0) -> (projT1 args1)) -> ℤ) ->
+ (projT1 args))%ptype option (fun x3 : option => x3)
+ with
+ | Some (_, _, _, _) =>
+ if
+ type.type_beq base.type base.type.type_beq
+ (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ ((((projT1 args0) -> (projT1 args1)) -> ℤ) ->
+ (projT1 args))%ptype
+ then
+ _ <- 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 (x1, (##0)%expr)%expr_pat
+ else None);
+ Some (Base x3)
+ 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 =>
+ 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
+ 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
+ (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 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
+ 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)
+ 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
+ end
+ | _ => 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);;
+ None);;;
+ 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
+ (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 ℤ =>
- Base (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat
+ (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 =>
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 05:29:04 +0000