From 25c3428cebabf4c0cf19aa20cf6857560052e849 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 31 Jan 2019 18:52:33 -0500 Subject: Uncps unify_extracted We never used the cps form, and this form is easier to read. --- src/Rewriter.v | 107 ++--- src/RewriterWf1.v | 29 -- src/arith_rewrite_head.out | 202 +++++----- src/arith_with_casts_rewrite_head.out | 204 ++++------ src/fancy_with_casts_rewrite_head.out | 722 +++++++++++++--------------------- src/nbe_rewrite_head.out | 282 +++++-------- 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 -- cgit v1.2.3