aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-01-31 18:52:33 -0500
committerGravatar Jason Gross <jasongross9@gmail.com>2019-02-01 23:40:21 -0500
commit25c3428cebabf4c0cf19aa20cf6857560052e849 (patch)
treee07a8d9186c4d3c43c072b9122eed821be6aa0be
parent014c627a93f09c2867e76e35837eb8cb64f98384 (diff)
Uncps unify_extracted
We never used the cps form, and this form is easier to read.
Diffstat
-rw-r--r--src/Rewriter.v107
-rw-r--r--src/RewriterWf1.v29
-rw-r--r--src/arith_rewrite_head.out202
-rw-r--r--src/arith_with_casts_rewrite_head.out204
-rw-r--r--src/fancy_with_casts_rewrite_head.out722
-rw-r--r--src/nbe_rewrite_head.out282
6 files changed, 575 insertions, 971 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v
index fb14b31f0..b9b57ff43 100644
--- a/src/Rewriter.v
+++ b/src/Rewriter.v
@@ -87,48 +87,26 @@ Module Compilers.
| type.type_base _ => fun _ => k evm
end v.
- Fixpoint unify_extracted_cps
+ Fixpoint unify_extracted
(ptype : type) (etype : Compilers.base.type)
- : ~> option (var_types_of ptype)
- := match ptype return ~> option (var_types_of ptype) with
- | type.var p => fun T k => k (Some etype)
- | type.type_base t
- => fun T k
- => match etype with
- | Compilers.base.type.type_base t'
- => if base.type.base_beq t t'
- then k (Some tt)
- else k None
- | _ => k None
- end
- | type.prod A B
- => fun T k
- => match etype with
- | Compilers.base.type.prod A' B'
- => unify_extracted_cps
- A A' _
- (fun a
- => match a with
- | Some a
- => unify_extracted_cps
- B B' _
- (fun b
- => match b with
- | Some b => k (Some (a, b))
- | None => k None
- end)
- | None => k None
- end)
- | _ => k None
- end
- | type.list A
- => fun T k
- => match etype with
- | Compilers.base.type.list A'
- => unify_extracted_cps A A' _ k
- | _ => k None
- end
- end%cps.
+ : option (var_types_of ptype)
+ := match ptype, etype return option (var_types_of ptype) with
+ | type.var p, _ => Some etype
+ | type.type_base t, Compilers.base.type.type_base t'
+ => if base.type.base_beq t t'
+ then Some tt
+ else None
+ | type.prod A B, Compilers.base.type.prod A' B'
+ => a <- unify_extracted A A';
+ b <- unify_extracted B B';
+ Some (a, b)
+ | type.list A, Compilers.base.type.list A'
+ => unify_extracted A A'
+ | type.type_base _, _
+ | type.prod _ _, _
+ | type.list _, _
+ => None
+ end%option.
End base.
Module type.
@@ -173,39 +151,20 @@ Module Compilers.
=> fun '(a, b) => @add_var_types_cps A a evm _ (fun evm => @add_var_types_cps B b evm _ k)
end v.
- Fixpoint unify_extracted_cps
+ Fixpoint unify_extracted
(ptype : type) (etype : type.type Compilers.base.type)
- : ~> option (var_types_of ptype)
- := match ptype return ~> option (var_types_of ptype) with
- | type.base t
- => fun T k
- => match etype with
- | type.base t' => base.unify_extracted_cps t t' T k
- | type.arrow _ _ => k None
- end
- | type.arrow A B
- => fun T k
- => match etype with
- | type.arrow A' B'
- => unify_extracted_cps
- A A' _
- (fun a
- => match a with
- | Some a
- => unify_extracted_cps
- B B' _
- (fun b
- => match b with
- | Some b => k (Some (a, b))
- | None => k None
- end)
- | None => k None
- end)
- | type.base _ => k None
- end
- end%cps.
-
- Notation unify_extracted ptype etype := (unify_extracted_cps ptype etype _ id).
+ : option (var_types_of ptype)
+ := match ptype, etype return option (var_types_of ptype) with
+ | type.base t, type.base t'
+ => base.unify_extracted t t'
+ | type.arrow A B, type.arrow A' B'
+ => a <- unify_extracted A A';
+ b <- unify_extracted B B';
+ Some (a, b)
+ | type.base _, _
+ | type.arrow _ _, _
+ => None
+ end%option.
Local Notation forall_vars_body K LS EVM0
:= (fold_right
@@ -2442,7 +2401,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y)
:= (eval cbv -[pr2_rewrite_rules
base.interp base.try_make_transport_cps
type.try_make_transport_cps
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
Compile.option_type_type_beq
Let_In Option.sequence Option.sequence_return
UnderLets.splice UnderLets.to_expr
diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v
index 19ea1e9e7..2b18d01d0 100644
--- a/src/RewriterWf1.v
+++ b/src/RewriterWf1.v
@@ -302,20 +302,6 @@ Module Compilers.
Ltac add_var_types_cps_id :=
cps_id_with_option (@add_var_types_cps_id _ _ _ _ _).
- Lemma unify_extracted_cps_id {pt et T k}
- : @pattern.base.unify_extracted_cps pt et T k = k (@pattern.base.unify_extracted_cps pt et _ id).
- Proof using Type.
- revert et T k; induction pt, et; cbn [pattern.base.unify_extracted_cps]; cbv [id] in *; intros;
- repeat first [ reflexivity
- | progress inversion_option
- | progress subst
- | break_innermost_match_step
- | rewrite_hyp !* ].
- Qed.
-
- Ltac unify_extracted_cps_id :=
- cps_id_with_option (@unify_extracted_cps_id _ _ _ _).
-
Lemma mem_collect_vars_subst_Some_find {x t evm t'}
(Hmem : PositiveSet.mem x (pattern.base.collect_vars t) = true)
(H : pattern.base.subst t evm = Some t')
@@ -403,21 +389,6 @@ Module Compilers.
Ltac add_var_types_cps_id :=
cps_id_with_option (@add_var_types_cps_id _ _ _ _ _).
- Lemma unify_extracted_cps_id {pt et T k}
- : @pattern.type.unify_extracted_cps pt et T k = k (@pattern.type.unify_extracted_cps pt et _ id).
- Proof using Type.
- revert et T k; induction pt, et; cbn [pattern.type.unify_extracted_cps]; cbv [id] in *; intros;
- repeat first [ reflexivity
- | progress inversion_option
- | progress subst
- | apply base.unify_extracted_cps_id
- | break_innermost_match_step
- | rewrite_hyp !* ].
- Qed.
-
- Ltac unify_extracted_cps_id :=
- cps_id_with_option (@unify_extracted_cps_id _ _ _ _).
-
Local Ltac t_subst_eq_iff :=
repeat first [ progress apply conj
| progress cbv [option_map Option.bind] in *
diff --git a/src/arith_rewrite_head.out b/src/arith_rewrite_head.out
index 669f6f8c8..60beec0c2 100644
--- a/src/arith_rewrite_head.out
+++ b/src/arith_rewrite_head.out
@@ -18,7 +18,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) _ =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((('1 * '2)%pbtype -> '1%pbtype) ->
(('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
'2%pbtype)%ptype
@@ -26,7 +26,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((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)
+ s0) -> s)%ptype
with
| Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
@@ -70,7 +70,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) _) x0 =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((('1 * '2)%pbtype -> '2%pbtype) ->
(('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
'2%pbtype)%ptype
@@ -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) ->
((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
- s0) -> s)%ptype option (fun x2 : option => x2)
+ s0) -> s)%ptype
with
| Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
@@ -222,8 +222,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -246,8 +246,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -269,9 +269,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(_ <- invert_bind_args idc0 Raw.ident.Z_opp;
args0 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (s -> (projT1 args0))%ptype option
- (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (s -> (projT1 args0))%ptype
with
| Some (_, _)%zrange =>
if
@@ -295,8 +294,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_opp;
args0 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (s -> (projT1 args0))%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (s -> (projT1 args0))%ptype
with
| Some (_, _)%zrange =>
if
@@ -329,8 +328,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> s)%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -354,8 +353,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> s)%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -381,8 +380,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_opp;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (s0 -> s)%ptype option (fun x3 : option => x3)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -413,8 +411,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
- option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -435,8 +432,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
- option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -464,9 +460,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -486,8 +481,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end;;
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -510,8 +505,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -534,8 +529,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -558,8 +553,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -581,8 +576,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_opp;
args0 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (s -> (projT1 args0))%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (s -> (projT1 args0))%ptype
with
| Some (_, _)%zrange =>
if
@@ -611,8 +606,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> s)%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -641,8 +636,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -665,8 +660,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -689,8 +684,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -715,8 +710,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -741,8 +736,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_opp;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (s0 -> s)%ptype option (fun x3 : option => x3)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -772,8 +766,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
- option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -794,8 +787,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -820,8 +813,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
- option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -842,8 +834,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -879,10 +871,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_mul;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(ℤ -> ℤ -> ℤ -> ℤ)%ptype
((projT1 args2) -> (projT1 args0) -> s2 -> s1)%ptype
- option (fun x5 : option => x5)
with
| Some (_, (_, (_, _)))%zrange =>
if
@@ -938,10 +929,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_mul;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
- (ℤ -> ℤ -> ℤ -> ℤ)%ptype
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ -> ℤ)%ptype
((projT1 args2) -> s0 -> s2 -> (projT1 args))%ptype
- option (fun x5 : option => x5)
with
| Some (_, (_, (_, _)))%zrange =>
if
@@ -991,9 +980,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_mul;
args0 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ -> ℤ)%ptype
- ((projT1 args0) -> s0 -> s)%ptype option
- (fun x3 : option => x3)
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
+ ((projT1 args0) -> s0 -> s)%ptype
with
| Some (_, (_, _))%zrange =>
if
@@ -1031,8 +1019,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end;;
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1066,8 +1054,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1092,8 +1080,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end;;
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1116,8 +1104,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1140,8 +1128,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> s)%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1165,8 +1153,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> s)%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1198,8 +1186,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1224,8 +1212,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(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 x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (s -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1250,8 +1238,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (s -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1283,8 +1271,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1309,8 +1297,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc0 Raw.ident.Z_opp;
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (s0 -> s)%ptype option (fun x3 : option => x3)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s0 -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1340,8 +1327,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
- option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1362,8 +1348,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x1 =>
_ <- invert_bind_args idc Raw.ident.Z_opp;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
- option (fun x2 : option => x2)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1387,10 +1372,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((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
+ match pattern.type.unify_extracted ℤ s with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ s
then
@@ -1404,9 +1386,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
@expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None
| _ => None
end;;
- match
- pattern.type.unify_extracted_cps ℤ ℤ option (fun x0 : option => x0)
- with
+ match pattern.type.unify_extracted ℤ ℤ with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ ℤ
then
@@ -1426,8 +1406,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1446,8 +1426,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end);;
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1478,8 +1458,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1498,8 +1478,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end);;
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1538,8 +1518,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (ℤ -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1562,8 +1542,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1622,12 +1602,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ -> (ℤ * ℤ)%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)
+ s0) -> s)%ptype
with
| Some (_, (_, (_, _)), _, _)%zrange =>
if
diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out
index e85d57fd0..365a351b0 100644
--- a/src/arith_with_casts_rewrite_head.out
+++ b/src/arith_with_casts_rewrite_head.out
@@ -18,7 +18,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) _ =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((('1 * '2)%pbtype -> '1%pbtype) ->
(('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
'2%pbtype)%ptype
@@ -26,7 +26,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((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)
+ s0) -> s)%ptype
with
| Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
@@ -70,7 +70,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) _) x0 =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((('1 * '2)%pbtype -> '2%pbtype) ->
(('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
'2%pbtype)%ptype
@@ -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) ->
((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
- s0) -> s)%ptype option (fun x2 : option => x2)
+ s0) -> s)%ptype
with
| Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
@@ -232,8 +232,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 args2) -> s1)%ptype option (fun x4 : option => x4)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args2) -> s1)%ptype
with
| Some (_, _)%zrange =>
if
@@ -288,8 +288,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end;;
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -319,10 +319,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 ℤ s1 option
- (fun x3 : option => x3)
- with
+ match pattern.type.unify_extracted ℤ s1 with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ s1
then
@@ -386,8 +383,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args) -> ℤ)%ptype
with
| Some (_, _)%zrange =>
if
@@ -421,9 +418,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args0) -> (projT1 args)) -> ℤ)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -449,9 +445,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args0) -> ℤ) -> (projT1 args))%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -476,9 +471,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args1) -> s) -> (projT1 args0))%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -519,9 +513,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args1) -> (projT1 args)) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -572,9 +565,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
args1 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x2 : option => x2)
with
| Some (_, _, _)%zrange =>
if
@@ -604,9 +596,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args1) -> (projT1 args0)) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -647,9 +638,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args1) -> s) -> (projT1 args))%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -694,8 +684,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) 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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args) -> ℤ) -> ℤ)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -730,11 +720,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) ->
- (projT1 args0)) -> (projT1 args))%ptype option
- (fun x3 : option => x3)
+ (projT1 args0)) -> (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -770,11 +759,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) ->
- (projT1 args0)) -> s)%ptype option
- (fun x4 : option => x4)
+ (projT1 args0)) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -822,10 +810,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) -> s) ->
- (projT1 args))%ptype option (fun x4 : option => x4)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -889,9 +877,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat
| Z_cast range =>
fun x : expr ℤ =>
- (((match
- pattern.type.unify_extracted_cps ℤ ℤ option (fun x0 : option => x0)
- with
+ (((match pattern.type.unify_extracted ℤ ℤ with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ ℤ
then
@@ -907,10 +893,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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
+ match pattern.type.unify_extracted ℤ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ (projT1 args)
then
@@ -928,10 +911,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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
+ match pattern.type.unify_extracted ℤ s with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ s
then
@@ -958,8 +938,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- ((projT1 args0) -> s1)%ptype option (fun x3 : option => x3)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> s1)%ptype
with
| Some (_, _)%zrange =>
if
@@ -1015,8 +995,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_add;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
- (s1 -> (projT1 args))%ptype option (fun x3 : option => x3)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ (s1 -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1075,8 +1055,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s0) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1124,12 +1104,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ -> (ℤ * ℤ)%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)
+ s0) -> s)%ptype
with
| Some (_, (_, (_, _)), _, _)%zrange =>
if
@@ -1165,8 +1145,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((s1 -> s4) -> s)%ptype option (fun x6 : option => x6)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s4) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1249,8 +1229,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((s1 -> s0) -> s4)%ptype option (fun x6 : option => x6)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s0) -> s4)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1329,9 +1309,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((s1 -> (projT1 args)) -> s)%ptype option
- (fun x3 : option => x3)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> (projT1 args)) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1380,9 +1359,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((s1 -> s0) -> (projT1 args))%ptype option
- (fun x3 : option => x3)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s0) -> (projT1 args))%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1429,8 +1407,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end;;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s0) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1456,8 +1434,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s0) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1483,8 +1461,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s0) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -1524,10 +1502,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((s2 -> (projT1 args2)) -> s5) -> s)%ptype option
- (fun x7 : option => x7)
+ (((s2 -> (projT1 args2)) -> s5) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -1583,10 +1560,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ (((s2 -> (projT1 args2)) -> s5) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -1678,10 +1653,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype option
- (fun x7 : option => x7)
+ (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -1737,10 +1711,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ (((s2 -> (projT1 args2)) -> s0) -> s5)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -1828,10 +1800,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
- (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((s2 -> (projT1 args0)) -> (projT1 args)) -> s)%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, _, _)%zrange =>
if
@@ -1891,10 +1861,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
- (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((s2 -> (projT1 args0)) -> s0) -> (projT1 args))%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, _, _)%zrange =>
if
@@ -1951,9 +1919,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((s2 -> (projT1 args)) -> s0) -> s)%ptype option
- (fun x4 : option => x4)
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ (((s2 -> (projT1 args)) -> s0) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2005,10 +1972,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((s2 -> s5) -> s8) -> s)%ptype option
- (fun x10 : option => x10)
+ (((s2 -> s5) -> s8) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2106,10 +2072,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((s2 -> s5) -> s0) -> s8)%ptype option
- (fun x10 : option => x10)
+ (((s2 -> s5) -> s0) -> s8)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2203,10 +2168,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((s2 -> s5) -> (projT1 args)) -> s)%ptype option
- (fun x7 : option => x7)
+ (((s2 -> s5) -> (projT1 args)) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2268,10 +2232,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- (((s2 -> s5) -> s0) -> (projT1 args))%ptype option
- (fun x7 : option => x7)
+ (((s2 -> s5) -> s0) -> (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2350,11 +2313,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args1) -> s3) -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x5 : option => x5)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2413,8 +2375,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ (((s2 -> s1) -> s0) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2442,8 +2404,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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)
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ (((s2 -> s1) -> s0) -> s)%ptype
with
| Some (_, _, _, _)%zrange =>
if
diff --git a/src/fancy_with_casts_rewrite_head.out b/src/fancy_with_casts_rewrite_head.out
index 4a5354593..551fd7e18 100644
--- a/src/fancy_with_casts_rewrite_head.out
+++ b/src/fancy_with_casts_rewrite_head.out
@@ -157,8 +157,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| Z_add_modulo =>
fun x x0 x1 : expr ℤ =>
(match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((ℤ -> ℤ) -> ℤ)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -191,9 +191,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ -> ℤ)%ptype
- ((projT1 args3) -> (projT1 args0) -> s4)%ptype option
- (fun x6 : option => x6)
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
+ ((projT1 args3) -> (projT1 args0) -> s4)%ptype
with
| Some (_, (_, _))%zrange =>
if
@@ -247,9 +246,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ -> ℤ)%ptype
- ((projT1 args3) -> (projT1 args0) -> s4)%ptype option
- (fun x6 : option => x6)
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
+ ((projT1 args3) -> (projT1 args0) -> s4)%ptype
with
| Some (_, (_, _))%zrange =>
if
@@ -312,9 +310,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ -> ℤ)%ptype
- ((projT1 args3) -> s4 -> (projT1 args))%ptype option
- (fun x6 : option => x6)
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
+ ((projT1 args3) -> s4 -> (projT1 args))%ptype
with
| Some (_, (_, _))%zrange =>
if
@@ -368,9 +365,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ -> ℤ)%ptype
- ((projT1 args3) -> s4 -> (projT1 args))%ptype option
- (fun x6 : option => x6)
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
+ ((projT1 args3) -> s4 -> (projT1 args))%ptype
with
| Some (_, (_, _))%zrange =>
if
@@ -435,9 +431,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ -> ℤ)%ptype
- ((projT1 args3) -> s4 -> (projT1 args))%ptype option
- (fun x6 : option => x6)
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
+ ((projT1 args3) -> s4 -> (projT1 args))%ptype
with
| Some (_, (_, _))%zrange =>
if
@@ -483,9 +478,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps (ℤ -> ℤ -> ℤ)%ptype
- ((projT1 args3) -> s4 -> (projT1 args))%ptype option
- (fun x6 : option => x6)
+ pattern.type.unify_extracted (ℤ -> ℤ -> ℤ)%ptype
+ ((projT1 args3) -> s4 -> (projT1 args))%ptype
with
| Some (_, (_, _))%zrange =>
if
@@ -594,10 +588,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> s4) -> (projT1 args))%ptype
- option (fun x6 : option => x6)
with
| Some (_, _, _)%zrange =>
if
@@ -652,10 +644,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> s4) -> (projT1 args))%ptype
- option (fun x6 : option => x6)
with
| Some (_, _, _)%zrange =>
if
@@ -721,11 +711,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
(((projT1 args4) -> s4) ->
- (projT1 args0) -> s8)%ptype option
- (fun x10 : option => x10)
+ (projT1 args0) -> s8)%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -736,12 +725,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s4
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
fv <- (x10 <- (if
((let (x10, _) := xv in
x10) =?
@@ -817,11 +804,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
(((projT1 args4) -> s4) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -832,10 +818,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s4
- ℤ;
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x10 <- (if
@@ -916,11 +900,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
(((projT1 args4) -> s4) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -931,10 +914,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s4
- ℤ;
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x10 <- (if
@@ -1024,10 +1005,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
((s4 -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x6 : option => x6)
with
| Some (_, _, _)%zrange =>
if
@@ -1082,10 +1061,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
((s4 -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x6 : option => x6)
with
| Some (_, _, _)%zrange =>
if
@@ -1151,11 +1128,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
((s4 -> (projT1 args3)) ->
- (projT1 args0) -> s8)%ptype option
- (fun x10 : option => x10)
+ (projT1 args0) -> s8)%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -1164,14 +1140,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s4 -> (projT1 args3)) ->
(projT1 args0) -> s8)%ptype
then
- v <- type.try_make_transport_cps s4
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args3);
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
fv <- (x10 <- (if
((let (x10, _) := xv in
x10) =?
@@ -1247,11 +1221,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
((s4 -> (projT1 args3)) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -1260,12 +1233,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s4 -> (projT1 args3)) ->
s8 -> (projT1 args))%ptype
then
- v <- type.try_make_transport_cps s4
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args3);
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x10 <- (if
@@ -1346,11 +1317,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
((s4 -> (projT1 args3)) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -1359,12 +1329,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s4 -> (projT1 args3)) ->
s8 -> (projT1 args))%ptype
then
- v <- type.try_make_transport_cps s4
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args3);
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x10 <- (if
@@ -1456,10 +1424,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
((s4 -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x6 : option => x6)
with
| Some (_, _, _)%zrange =>
if
@@ -1505,10 +1471,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args3 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
((s4 -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x6 : option => x6)
with
| Some (_, _, _)%zrange =>
if
@@ -1566,11 +1530,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
((s4 -> (projT1 args3)) ->
- (projT1 args0) -> s8)%ptype option
- (fun x10 : option => x10)
+ (projT1 args0) -> s8)%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -1579,14 +1542,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s4 -> (projT1 args3)) ->
(projT1 args0) -> s8)%ptype
then
- v <- type.try_make_transport_cps s4
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args3);
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
fv <- (x10 <- (if
((let (x10, _) := xv0 in
x10) =?
@@ -1650,11 +1611,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
((s4 -> (projT1 args3)) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -1663,12 +1623,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s4 -> (projT1 args3)) ->
s8 -> (projT1 args))%ptype
then
- v <- type.try_make_transport_cps s4
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args3);
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x10 <- (if
@@ -1737,11 +1695,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args6 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_mul;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
((s4 -> (projT1 args3)) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -1750,12 +1707,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s4 -> (projT1 args3)) ->
s8 -> (projT1 args))%ptype
then
- v <- type.try_make_transport_cps s4
- ℤ;
+ v <- type.try_make_transport_cps s4 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args3);
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x10 <- (if
@@ -1928,11 +1883,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x7 : option => x7)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -1943,8 +1897,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
xv1 <- ident.unify pattern.ident.Literal
@@ -1995,10 +1948,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> (projT1 args0)) ->
- s6)%ptype option (fun x8 : option => x8)
+ s6)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2009,12 +1962,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
- v0 <- type.try_make_transport_cps s6
- ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
fv <- (x8 <- (if
((let (x8, _) := xv in x8) =?
2
@@ -2067,11 +2018,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> s6) ->
- (projT1 args))%ptype option
- (fun x8 : option => x8)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2082,10 +2032,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
- v0 <- type.try_make_transport_cps s6
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x8 <- (if
@@ -2132,10 +2080,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> s6) -> s7)%ptype
- option (fun x9 : option => x9)
with
| Some (_, _, _, _)%zrange =>
if
@@ -2145,12 +2092,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
- v0 <- type.try_make_transport_cps s6
- ℤ;
- v1 <- type.try_make_transport_cps s7
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
+ v1 <- type.try_make_transport_cps s7 ℤ;
fv <- (x9 <- (if
((let (x9, _) := xv in x9) =?
2
@@ -2221,11 +2165,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x7 : option => x7)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2236,8 +2179,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
xv1 <- ident.unify pattern.ident.Literal
@@ -2282,10 +2224,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> (projT1 args0)) ->
- s6)%ptype option (fun x8 : option => x8)
+ s6)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2296,12 +2238,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
- v0 <- type.try_make_transport_cps s6
- ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
fv <- (x8 <- (if
((let (x8, _) := xv in x8) =?
1) &&
@@ -2348,11 +2288,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> s6) ->
- (projT1 args))%ptype option
- (fun x8 : option => x8)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2363,10 +2302,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
- v0 <- type.try_make_transport_cps s6
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x8 <- (if
@@ -2407,10 +2344,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s5) -> s6) -> s7)%ptype
- option (fun x9 : option => x9)
with
| Some (_, _, _, _)%zrange =>
if
@@ -2420,12 +2356,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args2);
- v <- type.try_make_transport_cps s5
- ℤ;
- v0 <- type.try_make_transport_cps s6
- ℤ;
- v1 <- type.try_make_transport_cps s7
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
+ v1 <- type.try_make_transport_cps s7 ℤ;
fv <- (x9 <- (if
((let (x9, _) := xv in x9) =?
1) &&
@@ -2487,11 +2420,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((s5 -> (projT1 args1)) -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x7 : option => x7)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2500,8 +2432,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((s5 -> (projT1 args1)) ->
(projT1 args0)) -> (projT1 args))%ptype
then
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args1);
xv0 <- ident.unify pattern.ident.Literal
@@ -2548,10 +2479,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((s5 -> (projT1 args1)) -> (projT1 args0)) ->
- s6)%ptype option (fun x8 : option => x8)
+ s6)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2560,14 +2491,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((s5 -> (projT1 args1)) ->
(projT1 args0)) -> s6)%ptype
then
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args1);
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
- v0 <- type.try_make_transport_cps s6
- ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
fv <- (x8 <- (if
((let (x8, _) := xv in x8) =?
1) &&
@@ -2614,11 +2543,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((s5 -> (projT1 args1)) -> s6) ->
- (projT1 args))%ptype option
- (fun x8 : option => x8)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2627,12 +2555,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((s5 -> (projT1 args1)) -> s6) ->
(projT1 args))%ptype
then
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args1);
- v0 <- type.try_make_transport_cps s6
- ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x8 <- (if
@@ -2673,10 +2599,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Z_cast;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((s5 -> (projT1 args1)) -> s6) -> s7)%ptype
- option (fun x9 : option => x9)
with
| Some (_, _, _, _)%zrange =>
if
@@ -2684,14 +2609,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((s5 -> (projT1 args1)) -> s6) -> s7)%ptype
then
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv <- ident.unify pattern.ident.Literal
##(projT2 args1);
- v0 <- type.try_make_transport_cps s6
- ℤ;
- v1 <- type.try_make_transport_cps s7
- ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
+ v1 <- type.try_make_transport_cps s7 ℤ;
fv <- (x9 <- (if
((let (x9, _) := xv in x9) =?
1) &&
@@ -2755,8 +2677,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
end;;
_ <- invert_bind_args idc Raw.ident.Z_zselect;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
- ((s1 -> s0) -> s)%ptype option (fun x3 : option => x3)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ ((s1 -> s0) -> s)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -2788,9 +2710,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args2 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_rshi;
match
- pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) -> s3) -> (projT1 args))%ptype
- option (fun x5 : option => x5)
with
| Some (_, _, _, _)%zrange =>
if
@@ -2873,9 +2794,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args2 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_rshi;
match
- pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x5 : option => x5)
with
| Some (_, _, _, _)%zrange =>
if
@@ -2965,9 +2885,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args2 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_rshi;
match
- pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
- ((((projT1 args2) -> s3) -> s4) -> (projT1 args))%ptype option
- (fun x6 : option => x6)
+ pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
+ ((((projT1 args2) -> s3) -> s4) -> (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -3137,9 +3056,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ (@expr.LetIn _ _ _ _ _ _ _) _ => None
| _ => None
end;;
- match
- pattern.type.unify_extracted_cps ℤ ℤ option (fun x0 : option => x0)
- with
+ match pattern.type.unify_extracted ℤ ℤ with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ ℤ
then
@@ -3194,12 +3111,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args7) -> (projT1 args6)) ->
(s8 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x10 : option => x10)
+ (projT1 args))%ptype
with
| Some (_, _, (_, _, _))%zrange =>
if
@@ -3216,8 +3132,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args6);
- v <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s8 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -3365,11 +3280,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
(((projT1 args4) -> (projT1 args3)) ->
- s5 -> (projT1 args))%ptype option
- (fun x7 : option => x7)
+ s5 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -3385,8 +3299,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args3);
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -3446,10 +3359,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> s2)%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, _)%zrange =>
if
@@ -3524,12 +3435,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((projT1 args7) ->
(s8 -> (projT1 args0)) ->
(projT1 args)) -> (projT1 args5))%ptype
- option (fun x10 : option => x10)
with
| Some (_, (_, _, _), _)%zrange =>
if
@@ -3543,8 +3453,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args7);
- v <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -3696,11 +3605,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args4) -> s5 -> (projT1 args)) ->
- (projT1 args2))%ptype option
- (fun x7 : option => x7)
+ (projT1 args2))%ptype
with
| Some (_, (_, _), _)%zrange =>
if
@@ -3714,8 +3622,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -3778,10 +3685,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> s2) -> (projT1 args))%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, _)%zrange =>
if
@@ -3837,11 +3742,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args7 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args7) -> s2) ->
(s9 -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x11 : option => x11)
with
| Some (_, _, (_, _, _))%zrange =>
if
@@ -4033,11 +3937,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args7 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((projT1 args7) ->
(s9 -> (projT1 args0)) -> (projT1 args)) ->
- s3)%ptype option (fun x11 : option => x11)
+ s3)%ptype
with
| Some (_, (_, _, _), _)%zrange =>
if
@@ -4227,10 +4131,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
(((projT1 args4) -> s2) -> s6 -> (projT1 args))%ptype
- option (fun x8 : option => x8)
with
| Some (_, _, (_, _))%zrange =>
if
@@ -4315,10 +4218,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args4 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args4) -> s6 -> (projT1 args)) -> s3)%ptype
- option (fun x8 : option => x8)
with
| Some (_, (_, _), _)%zrange =>
if
@@ -4397,10 +4299,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_add_get_carry;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
- (((projT1 args1) -> s2) -> s3)%ptype option
- (fun x5 : option => x5)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args1) -> s2) -> s3)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -4486,12 +4386,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args7) -> (projT1 args6)) ->
(s8 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x10 : option => x10)
+ (projT1 args))%ptype
with
| Some (_, _, (_, _, _))%zrange =>
if
@@ -4508,8 +4407,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args6);
- v <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s8 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -4657,11 +4555,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
(((projT1 args4) -> (projT1 args3)) ->
- s5 -> (projT1 args))%ptype option
- (fun x7 : option => x7)
+ s5 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -4677,8 +4574,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args3);
- v <- type.try_make_transport_cps s5
- ℤ;
+ v <- type.try_make_transport_cps s5 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -4738,10 +4634,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> s2)%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, _)%zrange =>
if
@@ -4792,10 +4686,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> s2) -> (projT1 args))%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, _)%zrange =>
if
@@ -4863,12 +4755,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args7) -> s2) ->
(s9 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x11 : option => x11)
+ (projT1 args))%ptype
with
| Some (_, _, (_, _, _))%zrange =>
if
@@ -4882,10 +4773,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args7);
- v <- type.try_make_transport_cps s2
- ℤ;
- v0 <- type.try_make_transport_cps s9
- ℤ;
+ v <- type.try_make_transport_cps s2 ℤ;
+ v0 <- type.try_make_transport_cps s9 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -5038,11 +4927,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
(((projT1 args4) -> s2) ->
- s6 -> (projT1 args))%ptype option
- (fun x8 : option => x8)
+ s6 -> (projT1 args))%ptype
with
| Some (_, _, (_, _))%zrange =>
if
@@ -5055,10 +4943,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s2
- ℤ;
- v0 <- type.try_make_transport_cps s6
- ℤ;
+ v <- type.try_make_transport_cps s2 ℤ;
+ v0 <- type.try_make_transport_cps s6 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -5122,10 +5008,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
_ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow;
match
- pattern.type.unify_extracted_cps
- ((ℤ -> ℤ) -> ℤ)%ptype
- (((projT1 args1) -> s2) -> s3)%ptype option
- (fun x5 : option => x5)
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
+ (((projT1 args1) -> s2) -> s3)%ptype
with
| Some (_, _, _)%zrange =>
if
@@ -5218,13 +5102,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> (projT1 args7)) ->
(projT1 args6)) ->
(s9 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x11 : option => x11)
+ (projT1 args))%ptype
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -5247,8 +5130,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args6);
- v <- type.try_make_transport_cps s9
- ℤ;
+ v <- type.try_make_transport_cps s9 ℤ;
xv2 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -5416,12 +5298,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> (projT1 args4)) ->
(projT1 args3)) ->
- s6 -> (projT1 args))%ptype option
- (fun x8 : option => x8)
+ s6 -> (projT1 args))%ptype
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -5442,8 +5323,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args3);
- v <- type.try_make_transport_cps s6
- ℤ;
+ v <- type.try_make_transport_cps s6 ℤ;
xv2 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -5520,11 +5400,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) ->
- (projT1 args0)) -> s3)%ptype option
- (fun x5 : option => x5)
+ (projT1 args0)) -> s3)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -5606,12 +5485,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> (projT1 args7)) ->
(s9 -> (projT1 args0)) ->
(projT1 args)) -> (projT1 args5))%ptype
- option (fun x11 : option => x11)
with
| Some (_, _, (_, _, _), _)%zrange =>
if
@@ -5631,8 +5509,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args7);
- v <- type.try_make_transport_cps s9
- ℤ;
+ v <- type.try_make_transport_cps s9 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -5802,12 +5679,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args5) -> (projT1 args4)) ->
s6 -> (projT1 args)) ->
- (projT1 args2))%ptype option
- (fun x8 : option => x8)
+ (projT1 args2))%ptype
with
| Some (_, _, (_, _), _)%zrange =>
if
@@ -5825,8 +5701,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s6
- ℤ;
+ v <- type.try_make_transport_cps s6 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -5907,11 +5782,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) -> s3) ->
- (projT1 args))%ptype option
- (fun x5 : option => x5)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -5979,11 +5853,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> (projT1 args7)) -> s3) ->
(s10 -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x12 : option => x12)
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -5998,10 +5871,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
##(projT2 args8);
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args7);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s10
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s10 ℤ;
xv1 <- ident.unify pattern.ident.Literal
##(projT2 args0);
xv2 <- ident.unify pattern.ident.Literal
@@ -6206,11 +6077,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> (projT1 args7)) ->
(s10 -> (projT1 args0)) -> (projT1 args)) ->
- s4)%ptype option (fun x12 : option => x12)
+ s4)%ptype
with
| Some (_, _, (_, _, _), _)%zrange =>
if
@@ -6224,14 +6095,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
##(projT2 args8);
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args7);
- v <- type.try_make_transport_cps s10
- ℤ;
+ v <- type.try_make_transport_cps s10 ℤ;
xv1 <- ident.unify pattern.ident.Literal
##(projT2 args0);
xv2 <- ident.unify pattern.ident.Literal
##(projT2 args);
- v0 <- type.try_make_transport_cps s4
- ℤ;
+ v0 <- type.try_make_transport_cps s4 ℤ;
fv <- (x12 <- (let
'(r1, r2)%zrange := range
in
@@ -6424,11 +6293,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> (projT1 args4)) -> s3) ->
- s7 -> (projT1 args))%ptype option
- (fun x9 : option => x9)
+ s7 -> (projT1 args))%ptype
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -6441,10 +6309,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
##(projT2 args5);
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s7
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s7 ℤ;
xv1 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x9 <- (let
@@ -6529,11 +6395,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args5) -> (projT1 args4)) ->
- s7 -> (projT1 args)) -> s4)%ptype option
- (fun x9 : option => x9)
+ s7 -> (projT1 args)) -> s4)%ptype
with
| Some (_, _, (_, _), _)%zrange =>
if
@@ -6546,12 +6411,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
##(projT2 args5);
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s7
- ℤ;
+ v <- type.try_make_transport_cps s7 ℤ;
xv1 <- ident.unify pattern.ident.Literal
##(projT2 args);
- v0 <- type.try_make_transport_cps s4
- ℤ;
+ v0 <- type.try_make_transport_cps s4 ℤ;
fv <- (x9 <- (let
'(r1, r2)%zrange := range in
fun (s8 cc : Z)
@@ -6624,10 +6487,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) -> s3) ->
- s4)%ptype option (fun x6 : option => x6)
+ s4)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -6693,11 +6556,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x5 : option => x5)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -6773,13 +6635,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> s3) ->
(projT1 args6)) ->
(s10 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x12 : option => x12)
+ (projT1 args))%ptype
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -6795,13 +6656,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args8);
- v <- type.try_make_transport_cps s3
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args6);
- v0 <- type.try_make_transport_cps s10
- ℤ;
+ v0 <- type.try_make_transport_cps s10 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -6972,12 +6831,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> s3) ->
(projT1 args3)) ->
- s7 -> (projT1 args))%ptype option
- (fun x9 : option => x9)
+ s7 -> (projT1 args))%ptype
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -6991,13 +6849,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args5);
- v <- type.try_make_transport_cps s3
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args3);
- v0 <- type.try_make_transport_cps s7
- ℤ;
+ v0 <- type.try_make_transport_cps s7 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -7078,10 +6934,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> (projT1 args0)) ->
- s4)%ptype option (fun x6 : option => x6)
+ s4)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -7164,12 +7020,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> s3) ->
(s10 -> (projT1 args0)) ->
(projT1 args)) -> (projT1 args5))%ptype
- option (fun x12 : option => x12)
with
| Some (_, _, (_, _, _), _)%zrange =>
if
@@ -7185,10 +7040,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args8);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s10
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s10 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -7361,12 +7214,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args5) -> s3) ->
s7 -> (projT1 args)) ->
- (projT1 args2))%ptype option
- (fun x9 : option => x9)
+ (projT1 args2))%ptype
with
| Some (_, _, (_, _), _)%zrange =>
if
@@ -7380,10 +7232,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args5);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s7
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s7 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -7468,11 +7318,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> s4) ->
- (projT1 args))%ptype option
- (fun x6 : option => x6)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -7539,11 +7388,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> s3) -> s4) ->
(s11 -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x13 : option => x13)
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -7555,12 +7403,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args8);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s4
- ℤ;
- v1 <- type.try_make_transport_cps s11
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s4 ℤ;
+ v1 <- type.try_make_transport_cps s11 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
xv1 <- ident.unify pattern.ident.Literal
@@ -7768,11 +7613,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> s3) ->
(s11 -> (projT1 args0)) -> (projT1 args)) ->
- s5)%ptype option (fun x13 : option => x13)
+ s5)%ptype
with
| Some (_, _, (_, _, _), _)%zrange =>
if
@@ -7784,16 +7629,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args8);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s11
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s11 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args0);
xv1 <- ident.unify pattern.ident.Literal
##(projT2 args);
- v1 <- type.try_make_transport_cps s5
- ℤ;
+ v1 <- type.try_make_transport_cps s5 ℤ;
fv <- (x13 <- (let
'(r1, r2)%zrange := range
in
@@ -7989,11 +7831,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> s3) -> s4) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -8004,12 +7845,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args5);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s4
- ℤ;
- v1 <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s4 ℤ;
+ v1 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
fv <- (x10 <- (let
@@ -8100,11 +7938,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args5) -> s3) ->
- s8 -> (projT1 args)) -> s5)%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args)) -> s5)%ptype
with
| Some (_, _, (_, _), _)%zrange =>
if
@@ -8115,14 +7952,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
then
xv <- ident.unify pattern.ident.Literal
##(projT2 args5);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify pattern.ident.Literal
##(projT2 args);
- v1 <- type.try_make_transport_cps s5
- ℤ;
+ v1 <- type.try_make_transport_cps s5 ℤ;
fv <- (x10 <- (let
'(r1, r2)%zrange := range
in
@@ -8202,10 +8036,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_add_with_get_carry;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> s4) -> s5)%ptype
- option (fun x7 : option => x7)
with
| Some (_, _, _, _)%zrange =>
if
@@ -8307,13 +8140,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> (projT1 args7)) ->
(projT1 args6)) ->
(s9 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x11 : option => x11)
+ (projT1 args))%ptype
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -8336,8 +8168,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args6);
- v <- type.try_make_transport_cps s9
- ℤ;
+ v <- type.try_make_transport_cps s9 ℤ;
xv2 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -8505,12 +8336,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> (projT1 args4)) ->
(projT1 args3)) ->
- s6 -> (projT1 args))%ptype option
- (fun x8 : option => x8)
+ s6 -> (projT1 args))%ptype
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -8531,8 +8361,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args3);
- v <- type.try_make_transport_cps s6
- ℤ;
+ v <- type.try_make_transport_cps s6 ℤ;
xv2 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -8609,11 +8438,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) ->
- (projT1 args0)) -> s3)%ptype option
- (fun x5 : option => x5)
+ (projT1 args0)) -> s3)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -8670,11 +8498,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) -> s3) ->
- (projT1 args))%ptype option
- (fun x5 : option => x5)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -8751,13 +8578,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> (projT1 args7)) ->
s3) ->
(s10 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x12 : option => x12)
+ (projT1 args))%ptype
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -8776,10 +8602,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args7);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s10
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s10 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -8949,11 +8773,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> (projT1 args4)) ->
s3) -> s7 -> (projT1 args))%ptype
- option (fun x9 : option => x9)
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -8970,10 +8793,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args4);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s7
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s7 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -9054,10 +8875,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) -> s3) ->
- s4)%ptype option (fun x6 : option => x6)
+ s4)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -9123,11 +8944,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x5 : option => x5)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -9203,13 +9023,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> s3) ->
(projT1 args6)) ->
(s10 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x12 : option => x12)
+ (projT1 args))%ptype
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -9225,13 +9044,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args8);
- v <- type.try_make_transport_cps s3
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args6);
- v0 <- type.try_make_transport_cps s10
- ℤ;
+ v0 <- type.try_make_transport_cps s10 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -9402,12 +9219,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> s3) ->
(projT1 args3)) ->
- s7 -> (projT1 args))%ptype option
- (fun x9 : option => x9)
+ s7 -> (projT1 args))%ptype
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -9421,13 +9237,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args5);
- v <- type.try_make_transport_cps s3
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args3);
- v0 <- type.try_make_transport_cps s7
- ℤ;
+ v0 <- type.try_make_transport_cps s7 ℤ;
xv1 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -9508,10 +9322,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> (projT1 args0)) ->
- s4)%ptype option (fun x6 : option => x6)
+ s4)%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -9569,11 +9383,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> s4) ->
- (projT1 args))%ptype option
- (fun x6 : option => x6)
+ (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -9650,12 +9463,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype
((((projT1 args8) -> s3) -> s4) ->
(s11 -> (projT1 args0)) ->
- (projT1 args))%ptype option
- (fun x13 : option => x13)
+ (projT1 args))%ptype
with
| Some (_, _, _, (_, _, _))%zrange =>
if
@@ -9670,12 +9482,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args8);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s4
- ℤ;
- v1 <- type.try_make_transport_cps s11
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s4 ℤ;
+ v1 <- type.try_make_transport_cps s11 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args0);
@@ -9848,11 +9657,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
((((projT1 args5) -> s3) -> s4) ->
- s8 -> (projT1 args))%ptype option
- (fun x10 : option => x10)
+ s8 -> (projT1 args))%ptype
with
| Some (_, _, _, (_, _))%zrange =>
if
@@ -9865,12 +9673,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
xv <- ident.unify
pattern.ident.Literal
##(projT2 args5);
- v <- type.try_make_transport_cps s3
- ℤ;
- v0 <- type.try_make_transport_cps s4
- ℤ;
- v1 <- type.try_make_transport_cps s8
- ℤ;
+ v <- type.try_make_transport_cps s3 ℤ;
+ v0 <- type.try_make_transport_cps s4 ℤ;
+ v1 <- type.try_make_transport_cps s8 ℤ;
xv0 <- ident.unify
pattern.ident.Literal
##(projT2 args);
@@ -9955,10 +9760,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
_ <- invert_bind_args idc
Raw.ident.Z_sub_with_get_borrow;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> s3) -> s4) -> s5)%ptype
- option (fun x7 : option => x7)
with
| Some (_, _, _, _)%zrange =>
if
diff --git a/src/nbe_rewrite_head.out b/src/nbe_rewrite_head.out
index bf9101f5e..3c94cc019 100644
--- a/src/nbe_rewrite_head.out
+++ b/src/nbe_rewrite_head.out
@@ -6,10 +6,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℕ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℕ (projT1 args)
then
@@ -27,10 +24,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℕ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℕ (projT1 args)
then
@@ -52,9 +46,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℕ -> ℕ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -85,9 +78,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℕ -> ℕ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -118,9 +110,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℕ -> ℕ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -151,9 +142,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℕ -> ℕ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -184,9 +174,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℕ -> ℕ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -218,7 +207,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) _ =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((('1 * '2)%pbtype -> '1%pbtype) ->
(('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
'2%pbtype)%ptype
@@ -226,7 +215,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((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)
+ s0) -> s)%ptype
with
| Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
@@ -270,7 +259,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) _) x0 =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((('1 * '2)%pbtype -> '2%pbtype) ->
(('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) ->
'2%pbtype)%ptype
@@ -278,7 +267,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((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)
+ s0) -> s)%ptype
with
| Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
@@ -323,7 +312,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x2) x1 =>
args <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((('1%pbtype -> '2%pbtype -> '3%pbtype) ->
('1 * '2)%pbtype -> '3%pbtype) ->
'1%pbtype -> '2%pbtype -> '3%pbtype) ->
@@ -333,7 +322,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((let (x3, _) := args in x3) ->
(let (_, y) := args in y) ->
((let (x3, _) := args in x3) * (let (_, y) := args in y))%etype) ->
- s0) -> s)%ptype option (fun x3 : option => x3)
+ s0) -> s)%ptype
with
| Some
(_, (_, _), (_, _, _), (_, (_, b7)), (_, (_, (_, _)), b9, b8))%zrange =>
@@ -391,13 +380,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((((unit -> '1%pbtype) ->
(unit -> '1%pbtype) -> bool -> '1%pbtype) ->
unit -> '1%pbtype) -> unit -> '1%pbtype) -> bool)%ptype
(((((unit -> T) -> (unit -> T) -> bool -> T) -> unit -> T) ->
- unit -> T) -> (projT1 args))%ptype option
- (fun x2 : option => x2)
+ unit -> T) -> (projT1 args))%ptype
with
| Some (_, _, (_, _, (_, _)), (_, _), (_, b8), _)%zrange =>
if
@@ -438,14 +426,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((((unit -> '1%pbtype) ->
(ℕ -> '1%pbtype -> '1%pbtype) -> ℕ -> '1%pbtype) ->
- unit -> '1%pbtype) -> ℕ -> '1%pbtype -> '1%pbtype) ->
- ℕ)%ptype
+ unit -> '1%pbtype) -> ℕ -> '1%pbtype -> '1%pbtype) -> ℕ)%ptype
(((((unit -> P) -> (ℕ -> P -> P) -> ℕ -> P) -> unit -> P) ->
- ℕ -> P -> P) -> (projT1 args))%ptype option
- (fun x2 : option => x2)
+ ℕ -> P -> P) -> (projT1 args))%ptype
with
| Some
(_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), _)%zrange =>
@@ -495,15 +481,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((((('1%pbtype -> '2%pbtype) ->
(ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) ->
ℕ -> '1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) ->
- ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) ->
- ℕ) -> '1%pbtype)%ptype
+ ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> ℕ) ->
+ '1%pbtype)%ptype
((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) ->
- P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) ->
- P)%ptype option (fun x3 : option => x3)
+ P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> P)%ptype
with
| Some
(_, _, (_, (_, _, (_, _)), (_, (_, _))), (_, _),
@@ -512,8 +497,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
type.type_beq base.type base.type.type_beq
((((((b -> b16) ->
(ℕ -> (b -> b16) -> b -> b16) -> ℕ -> b -> b16) ->
- b -> b16) -> ℕ -> (b -> b16) -> b -> b16) -> ℕ) ->
- b)%ptype
+ b -> b16) -> ℕ -> (b -> b16) -> b -> b16) -> ℕ) -> b)%ptype
((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) ->
P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) ->
P)%ptype
@@ -564,7 +548,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(x0 : expr A -> expr (list A) -> expr P -> UnderLets (expr P))
(x1 : expr (list A)) =>
((match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((((unit -> '2%pbtype) ->
('1%pbtype ->
(pattern.base.type.list '1) -> '2%pbtype -> '2%pbtype) ->
@@ -573,8 +557,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(pattern.base.type.list '1) -> '2%pbtype -> '2%pbtype) ->
(pattern.base.type.list '1))%ptype
(((((unit -> P) -> (A -> (list A) -> P -> P) -> (list A) -> P) ->
- unit -> P) -> A -> (list A) -> P -> P) -> (list A))%ptype option
- (fun x2 : option => x2)
+ unit -> P) -> A -> (list A) -> P -> P) -> (list A))%ptype
with
| Some
(_, _, (_, (_, (_, _)), (_, _)), (_, _), (_, (_, (_, b12))), b)%zrange =>
@@ -630,7 +613,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.nil;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((((unit -> '2%pbtype) ->
('1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) ->
(pattern.base.type.list '1) -> '2%pbtype) ->
@@ -639,7 +622,6 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(pattern.base.type.list '1))%ptype
(((((unit -> P) -> (A -> (list A) -> P) -> (list A) -> P) ->
unit -> P) -> A -> (list A) -> P) -> (list args))%ptype
- option (fun x2 : option => x2)
with
| Some
(_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), b)%zrange =>
@@ -673,7 +655,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x3) x2 =>
args <- invert_bind_args idc Raw.ident.cons;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((((unit -> '2%pbtype) ->
('1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) ->
(pattern.base.type.list '1) -> '2%pbtype) ->
@@ -685,7 +667,6 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((((unit -> P) -> (A -> (list A) -> P) -> (list A) -> P) ->
unit -> P) -> A -> (list A) -> P) ->
((args -> (list args) -> (list args)) -> s0) -> s)%ptype
- option (fun x4 : option => x4)
with
| Some
(_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)),
@@ -743,9 +724,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @List_length T =>
fun x : expr (list T) =>
(match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((pattern.base.type.list '1) -> ℕ) -> (pattern.base.type.list '1))%ptype
- (((list T) -> ℕ) -> (list T))%ptype option (fun x0 : option => x0)
+ (((list T) -> ℕ) -> (list T))%ptype
with
| Some (_, _, b)%zrange =>
if
@@ -774,9 +755,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℕ -> ℕ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -806,12 +786,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℕ ->
(pattern.base.type.list '1) -> (pattern.base.type.list '1)) ->
ℕ) -> (pattern.base.type.list '1))%ptype
(((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype
- option (fun x1 : option => x1)
with
| Some (_, (_, _), _, b)%zrange =>
if
@@ -845,12 +824,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℕ ->
(pattern.base.type.list '1) -> (pattern.base.type.list '1)) ->
ℕ) -> (pattern.base.type.list '1))%ptype
(((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype
- option (fun x1 : option => x1)
with
| Some (_, (_, _), _, b)%zrange =>
if
@@ -884,10 +862,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((('1%pbtype -> ℕ -> (pattern.base.type.list '1)) -> '1%pbtype) ->
ℕ)%ptype (((A -> ℕ -> (list A)) -> A) -> (projT1 args))%ptype
- option (fun x1 : option => x1)
with
| Some (_, (_, _), b0, _)%zrange =>
if
@@ -917,12 +894,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @List_combine A B =>
fun (x : expr (list A)) (x0 : expr (list B)) =>
(match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((((pattern.base.type.list '1) ->
(pattern.base.type.list '2) -> (pattern.base.type.list ('1 * '2))) ->
(pattern.base.type.list '1)) -> (pattern.base.type.list '2))%ptype
((((list A) -> (list B) -> (list (A * B))) -> (list A)) -> (list B))%ptype
- option (fun x1 : option => x1)
with
| Some (_, (_, (_, _)), b0, b)%zrange =>
if
@@ -957,12 +933,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @List_map A B =>
fun (x : expr A -> UnderLets (expr B)) (x0 : expr (list A)) =>
((match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((('1%pbtype -> '2%pbtype) ->
(pattern.base.type.list '1) -> (pattern.base.type.list '2)) ->
'1%pbtype -> '2%pbtype) -> (pattern.base.type.list '1))%ptype
((((A -> B) -> (list A) -> (list B)) -> A -> B) -> (list A))%ptype
- option (fun x1 : option => x1)
with
| Some (_, _, (_, _), (_, b4), b)%zrange =>
if
@@ -1001,12 +976,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @List_app A =>
fun x x0 : expr (list A) =>
((match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((((pattern.base.type.list '1) ->
(pattern.base.type.list '1) -> (pattern.base.type.list '1)) ->
(pattern.base.type.list '1)) -> (pattern.base.type.list '1))%ptype
((((list A) -> (list A) -> (list A)) -> (list A)) -> (list A))%ptype
- option (fun x1 : option => x1)
with
| Some (_, (_, _), _, b)%zrange =>
if
@@ -1040,11 +1014,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @List_rev A =>
fun x : expr (list A) =>
((match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((pattern.base.type.list '1) -> (pattern.base.type.list '1)) ->
(pattern.base.type.list '1))%ptype
- (((list A) -> (list A)) -> (list A))%ptype option
- (fun x0 : option => x0)
+ (((list A) -> (list A)) -> (list A))%ptype
with
| Some (_, _, b)%zrange =>
if
@@ -1069,13 +1042,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @List_flat_map A B =>
fun (x : expr A -> UnderLets (expr (list B))) (x0 : expr (list A)) =>
((match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((('1%pbtype -> (pattern.base.type.list '2)) ->
(pattern.base.type.list '1) -> (pattern.base.type.list '2)) ->
'1%pbtype -> (pattern.base.type.list '2)) ->
(pattern.base.type.list '1))%ptype
((((A -> (list B)) -> (list A) -> (list B)) -> A -> (list B)) ->
- (list A))%ptype option (fun x1 : option => x1)
+ (list A))%ptype
with
| Some (_, _, (_, _), (_, b4), b)%zrange =>
if
@@ -1118,13 +1091,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @List_partition A =>
fun (x : expr A -> UnderLets (expr bool)) (x0 : expr (list A)) =>
((match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((('1%pbtype -> bool) ->
(pattern.base.type.list '1) ->
(pattern.base.type.list '1 * pattern.base.type.list '1)%pbtype) ->
'1%pbtype -> bool) -> (pattern.base.type.list '1))%ptype
((((A -> bool) -> (list A) -> (list A * list A)%etype) -> A -> bool) ->
- (list A))%ptype option (fun x1 : option => x1)
+ (list A))%ptype
with
| Some (_, _, (_, (_, _)), (_, _), b)%zrange =>
if
@@ -1178,13 +1151,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
fun (x : expr B -> expr A -> UnderLets (expr A)) (x0 : expr A)
(x1 : expr (list B)) =>
((match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((((('2%pbtype -> '1%pbtype -> '1%pbtype) ->
'1%pbtype -> (pattern.base.type.list '2) -> '1%pbtype) ->
'2%pbtype -> '1%pbtype -> '1%pbtype) -> '1%pbtype) ->
(pattern.base.type.list '2))%ptype
(((((B -> A -> A) -> A -> (list B) -> A) -> B -> A -> A) -> A) ->
- (list B))%ptype option (fun x2 : option => x2)
+ (list B))%ptype
with
| Some (_, (_, _), (_, (_, _)), (_, (_, _)), b0, b)%zrange =>
if
@@ -1234,13 +1207,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((((ℕ ->
('1%pbtype -> '1%pbtype) ->
(pattern.base.type.list '1) -> (pattern.base.type.list '1)) ->
ℕ) -> '1%pbtype -> '1%pbtype) -> (pattern.base.type.list '1))%ptype
((((ℕ -> (T -> T) -> (list T) -> (list T)) -> (projT1 args)) ->
- T -> T) -> (list T))%ptype option (fun x2 : option => x2)
+ T -> T) -> (list T))%ptype
with
| Some (_, (_, _, (_, _)), _, (_, _), b)%zrange =>
if
@@ -1284,11 +1257,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| @expr.Ident _ _ _ t idc =>
args <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((('1%pbtype -> (pattern.base.type.list '1) -> ℕ -> '1%pbtype) ->
'1%pbtype) -> (pattern.base.type.list '1)) -> ℕ)%ptype
((((T -> (list T) -> ℕ -> T) -> T) -> (list T)) ->
- (projT1 args))%ptype option (fun x2 : option => x2)
+ (projT1 args))%ptype
with
| Some (_, (_, (_, _)), _, b0, _)%zrange =>
if
@@ -1329,9 +1302,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1362,9 +1334,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1395,9 +1366,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1428,9 +1398,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1457,10 +1426,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℤ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ (projT1 args)
then
@@ -1482,9 +1448,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1515,9 +1480,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1544,10 +1508,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℤ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ (projT1 args)
then
@@ -1565,10 +1526,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℤ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ (projT1 args)
then
@@ -1590,9 +1548,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1623,9 +1580,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1656,9 +1612,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1685,10 +1640,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℕ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℕ (projT1 args)
then
@@ -1706,10 +1658,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℤ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ (projT1 args)
then
@@ -1731,9 +1680,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1764,9 +1712,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1797,9 +1744,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1830,9 +1776,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1859,10 +1804,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((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
+ match pattern.type.unify_extracted ℤ (projT1 args) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ (projT1 args)
then
@@ -1884,9 +1826,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -1920,9 +1861,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
args1 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x2 : option => x2)
with
| Some (_, _, _)%zrange =>
if
@@ -1967,9 +1907,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
args1 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x2 : option => x2)
with
| Some (_, _, _)%zrange =>
if
@@ -2014,9 +1953,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
args1 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x2 : option => x2)
with
| Some (_, _, _)%zrange =>
if
@@ -2061,11 +1999,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) ->
- (projT1 args0)) -> (projT1 args))%ptype option
- (fun x3 : option => x3)
+ (projT1 args0)) -> (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2117,9 +2054,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
args1 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x2 : option => x2)
with
| Some (_, _, _)%zrange =>
if
@@ -2167,11 +2103,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) ->
- (projT1 args0)) -> (projT1 args))%ptype option
- (fun x3 : option => x3)
+ (projT1 args0)) -> (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2223,9 +2158,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
args1 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x2 : option => x2)
with
| Some (_, _, _)%zrange =>
if
@@ -2267,9 +2201,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args0 <- invert_bind_args idc0 Raw.ident.Literal;
args1 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
+ pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x2 : option => x2)
with
| Some (_, _, _)%zrange =>
if
@@ -2314,11 +2247,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args1 <- invert_bind_args idc0 Raw.ident.Literal;
args2 <- invert_bind_args idc Raw.ident.Literal;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
((((projT1 args2) -> (projT1 args1)) ->
- (projT1 args0)) -> (projT1 args))%ptype option
- (fun x3 : option => x3)
+ (projT1 args0)) -> (projT1 args))%ptype
with
| Some (_, _, _, _)%zrange =>
if
@@ -2363,9 +2295,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
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 x1 : option => x1)
+ pattern.type.unify_extracted (ℤ -> ℤ)%ptype
+ ((projT1 args0) -> (projT1 args))%ptype
with
| Some (_, _)%zrange =>
if
@@ -2429,7 +2360,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args2 <- invert_bind_args idc0 Raw.ident.pair;
args3 <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) ->
((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype
((((let (x4, _) := args3 in x4) ->
@@ -2439,7 +2370,6 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(let (_, y) := args2 in y) ->
((let (x4, _) := args2 in x4) * (let (_, y) := args2 in y))%etype) ->
(projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange =>
if
@@ -2534,7 +2464,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args2 <- invert_bind_args idc0 Raw.ident.pair;
args3 <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) ->
((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype
((((let (x4, _) := args3 in x4) ->
@@ -2544,7 +2474,6 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(let (_, y) := args2 in y) ->
((let (x4, _) := args2 in x4) * (let (_, y) := args2 in y))%etype) ->
(projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange =>
if
@@ -2636,7 +2565,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
args2 <- invert_bind_args idc0 Raw.ident.pair;
args3 <- invert_bind_args idc Raw.ident.pair;
match
- pattern.type.unify_extracted_cps
+ pattern.type.unify_extracted
((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) ->
((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype
((((let (x4, _) := args3 in x4) ->
@@ -2646,7 +2575,6 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(let (_, y) := args2 in y) ->
((let (x4, _) := args2 in x4) * (let (_, y) := args2 in y))%etype) ->
(projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype
- option (fun x4 : option => x4)
with
| Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange =>
if
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 09:24:34 +0000