nbe_rewrite_head = match idc in (Compilers.ident t) return (Compile.value' true t) with | @Literal t v => Base (##v)%expr | Nat_succ => fun x : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℕ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Nat.succ (let (x0, _) := idc_args in x0)))%expr) | None => None end | _ => None end;; None);;; Base (#(Nat_succ)%expr @ x)%expr_pat)%option | Nat_pred => fun x : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℕ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Nat.pred (let (x0, _) := idc_args in x0)))%expr) | None => None end | _ => None end;; None);;; Base (#(Nat_pred)%expr @ x)%expr_pat)%option | Nat_max => fun x x0 : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℕ -> ℕ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Nat.max (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Nat_max)%expr @ x @ x0)%expr_pat)%option | Nat_mul => fun x x0 : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℕ -> ℕ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) * (let (x1, _) := idc_args0 in x1))%nat)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Nat_mul)%expr @ x @ x0)%expr_pat)%option | Nat_add => fun x x0 : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℕ -> ℕ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) + (let (x1, _) := idc_args0 in x1))%nat)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Nat_add)%expr @ x @ x0)%expr_pat)%option | Nat_sub => fun x x0 : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℕ -> ℕ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) - (let (x1, _) := idc_args0 in x1))%nat)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Nat_sub)%expr @ x @ x0)%expr_pat)%option | @nil t => Base []%expr_pat | @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat | @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat | @fst A B => fun x : expr (A * B)%etype => ((match x with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) _ => args <- invert_bind_args idc Raw.ident.pair; match pattern.type.unify_extracted_cps ((('1 * '2)%pbtype -> '1%pbtype) -> (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) -> '2%pbtype)%ptype (((A * B)%etype -> A) -> (((let (x2, _) := args in x2) -> (let (_, y) := args in y) -> ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> s0) -> s)%ptype option (fun x2 : option => x2) with | Some (_, _, _, (_, (_, (_, _)), b3, b2)) => _ <- ident.unify pattern.ident.fst fst; _ <- ident.unify pattern.ident.pair pair; v <- type.try_make_transport_cps s0 b3; _ <- type.try_make_transport_cps s b2; v1 <- base.try_make_transport_cps b3 A; v2 <- base.try_make_transport_cps A A; v3 <- base.try_make_transport_cps A A; Some (Base (v3 (v2 (v1 (v (Compile.reflect x1)))))) | None => None end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None | _ => None end;; None);;; Base (#(fst)%expr @ x)%expr_pat)%option | @snd A B => fun x : expr (A * B)%etype => ((match x with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) _) x0 => args <- invert_bind_args idc Raw.ident.pair; match pattern.type.unify_extracted_cps ((('1 * '2)%pbtype -> '2%pbtype) -> (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) -> '2%pbtype)%ptype (((A * B)%etype -> B) -> (((let (x2, _) := args in x2) -> (let (_, y) := args in y) -> ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> s0) -> s)%ptype option (fun x2 : option => x2) with | Some (_, _, _, (_, (_, (_, _)), b3, b2)) => _ <- ident.unify pattern.ident.snd snd; _ <- ident.unify pattern.ident.pair pair; _ <- type.try_make_transport_cps s0 b3; v0 <- type.try_make_transport_cps s b2; v1 <- base.try_make_transport_cps b2 B; v2 <- base.try_make_transport_cps B B; v3 <- base.try_make_transport_cps B B; Some (Base (v3 (v2 (v1 (v0 (Compile.reflect x0)))))) | None => None end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None | _ => None end;; None);;; Base (#(snd)%expr @ x)%expr_pat)%option | @prod_rect A B T => fun (x : expr A -> expr B -> UnderLets (expr T)) (x0 : expr (A * B)%etype) => ((match x0 with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x2) x1 => args <- invert_bind_args idc Raw.ident.pair; match pattern.type.unify_extracted_cps (((('1%pbtype -> '2%pbtype -> '3%pbtype) -> ('1 * '2)%pbtype -> '3%pbtype) -> '1%pbtype -> '2%pbtype -> '3%pbtype) -> (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) -> '2%pbtype)%ptype ((((A -> B -> T) -> (A * B)%etype -> T) -> A -> B -> T) -> (((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) with | Some (_, (_, _), (_, _, _), (_, (_, b7)), (_, (_, (_, _)), b9, b8)) => _ <- ident.unify pattern.ident.prod_rect prod_rect; base.try_make_transport_cps A b9 (fun a13 : option => (fa <- (fun (T0 : Type) (k : option -> T0) => match a13 with | Some x' => base.try_make_transport_cps B b8 (fun a14 : option => fa <- (fun (T1 : Type) (k0 : option -> T1) => match a14 with | Some x'0 => base.try_make_transport_cps T b7 (fun a15 : option => fa <- (fun (T2 : Type) (k1 : option -> T2) => match a15 with | Some x'1 => (return Some (fun v : expr b9 -> expr B -> UnderLets (expr T) => x'1 (x'0 v))) T2 k1 | None => k1 None end); k0 fa) | None => k0 None end); fa0 <- (fun (T1 : Type) (k0 : option -> T1) => match fa with | Some x'0 => (return Some (fun v : expr A -> expr B -> UnderLets (expr T) => x'0 (x' v))) T1 k0 | None => k0 None end); k fa0) | None => k None end); match fa with | Some v => (_ <- ident.unify pattern.ident.pair pair; v0 <- type.try_make_transport_cps s0 b9; v1 <- type.try_make_transport_cps s b8; v2 <- base.try_make_transport_cps b7 T; v3 <- base.try_make_transport_cps T T; v4 <- base.try_make_transport_cps T T; Some (fv <-- v2 (v x (v0 (Compile.reflect x2)) (v1 (Compile.reflect x1))); Base (v4 (v3 fv)))%under_lets)%option | None => None end)%cps) | None => None end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None | _ => None end;; None);;; Base (#(prod_rect)%expr @ (λ (x1 : var A)(x2 : var B), to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat)%option | @bool_rect T => fun (x x0 : expr unit -> UnderLets (expr T)) (x1 : expr bool) => ((match x1 with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((((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) with | Some (_, _, (_, _, (_, _)), (_, _), (_, b8), _) => _ <- ident.unify pattern.ident.bool_rect bool_rect; base.try_make_transport_cps T b8 (fun a9 : option => (fa <- (fun (T0 : Type) (k : option -> T0) => match a9 with | Some x' => (return Some (fun v : expr unit -> UnderLets (expr T) => x' v)) T0 k | None => k None end); match fa with | Some v => base.try_make_transport_cps T b8 (fun a10 : option => fa0 <- (fun (T0 : Type) (k : option -> T0) => match a10 with | Some x' => (return Some (fun v0 : expr unit -> UnderLets (expr T) => x' v0)) T0 k | None => k None end); match fa0 with | Some v0 => (idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); v1 <- base.try_make_transport_cps b8 T; v2 <- base.try_make_transport_cps T T; v3 <- base.try_make_transport_cps T T; Some (fv <-- v1 (if let (x2, _) := idc_args0 in x2 then v x (##tt)%expr else v0 x0 (##tt)%expr); Base (v3 (v2 fv)))%under_lets)%option | None => None end) | None => None end)%cps) | None => None end | _ => None end;; None);;; Base (#(bool_rect)%expr @ (λ x2 : var unit, to_expr (x ($x2)))%expr @ (λ x2 : var unit, to_expr (x0 ($x2)))%expr @ x1)%expr_pat)%option | @nat_rect P => fun (x : expr unit -> UnderLets (expr P)) (x0 : expr ℕ -> expr P -> UnderLets (expr P)) (x1 : expr ℕ) => ((match x1 with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((((unit -> '1%pbtype) -> (ℕ -> '1%pbtype -> '1%pbtype) -> ℕ -> '1%pbtype) -> 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) with | Some (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), _) => _ <- ident.unify pattern.ident.nat_rect nat_rect; base.try_make_transport_cps P b10 (fun a11 : option => (fa <- (fun (T : Type) (k : option -> T) => match a11 with | Some x' => (return Some (fun v : expr unit -> UnderLets (expr P) => x' v)) T k | None => k None end); match fa with | Some v => base.try_make_transport_cps P b10 (fun a12 : option => fa0 <- (fun (T : Type) (k : option -> T) => match a12 with | Some x' => base.try_make_transport_cps P b10 (fun a13 : option => fa0 <- (fun (T0 : Type) (k0 : option -> T0) => match a13 with | Some x'0 => (return Some (fun v0 : expr ℕ -> expr P -> UnderLets (expr P) => x'0 (x' v0))) T0 k0 | None => k0 None end); k fa0) | None => k None end); fa1 <- (fun (T : Type) (k : option -> T) => match fa0 with | Some x' => (return Some (fun v0 : expr ℕ -> expr P -> UnderLets (expr P) => x' v0)) T k | None => k None end); match fa1 with | Some v0 => (idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); v1 <- base.try_make_transport_cps b10 P; v2 <- base.try_make_transport_cps P P; v3 <- base.try_make_transport_cps P P; Some (fv <-- v1 (Datatypes.nat_rect (fun _ : nat => UnderLets (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b10 (PositiveMap.empty base.type))))) (v x (##tt)%expr) (fun (n' : nat) (rec : UnderLets (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b10 (PositiveMap.empty base.type))))) => rec0 <-- rec; v0 x0 (##n')%expr rec0) (let (x2, _) := idc_args0 in x2)); Base (v3 (v2 fv)))%under_lets)%option | None => None end) | None => None end)%cps) | None => None end | _ => None end;; None);;; Base (#(nat_rect)%expr @ (λ x2 : var unit, to_expr (x ($x2)))%expr @ (λ (x2 : var ℕ)(x3 : var P), to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat)%option | @nat_rect_arrow P Q => fun (x : expr P -> UnderLets (expr Q)) (x0 : expr ℕ -> (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q)) (x1 : expr ℕ) (x2 : expr P) => (match x1 with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((((('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 ((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) -> P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> P)%ptype option (fun x3 : option => x3) with | Some (_, _, (_, (_, _, (_, _)), (_, (_, _))), (_, _), (_, (_, _, (_, b16))), _, b) => _ <- ident.unify pattern.ident.nat_rect_arrow nat_rect_arrow; base.try_make_transport_cps P b (fun a17 : option => (fa <- (fun (T : Type) (k : option -> T) => match a17 with | Some x' => base.try_make_transport_cps Q b16 (fun a18 : option => fa <- (fun (T0 : Type) (k0 : option -> T0) => match a18 with | Some x'0 => (return Some (fun v : expr P -> UnderLets (expr Q) => x'0 (x' v))) T0 k0 | None => k0 None end); k fa) | None => k None end); match fa with | Some v => base.try_make_transport_cps P b (fun a18 : option => fa0 <- (fun (T : Type) (k : option -> T) => match a18 with | Some x' => base.try_make_transport_cps Q b16 (fun a19 : option => fa0 <- (fun (T0 : Type) (k0 : option -> T0) => match a19 with | Some x'0 => (return Some (fun v0 : expr ℕ -> (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q) => x'0 (x' v0))) T0 k0 | None => k0 None end); k fa0) | None => k None end); fa1 <- (fun (T : Type) (k : option -> T) => match fa0 with | Some x' => base.try_make_transport_cps P b (fun a19 : option => fa1 <- (fun (T0 : Type) (k0 : option -> T0) => match a19 with | Some x'0 => base.try_make_transport_cps Q b16 (fun a20 : option => fa1 <- (fun (T1 : Type) (k1 : option -> T1) => match a20 with | Some x'1 => (return Some (fun v0 : expr ℕ -> (expr b -> UnderLets (expr b16)) -> expr P -> UnderLets (expr Q) => x'1 (x'0 v0))) T1 k1 | None => k1 None end); k0 fa1) | None => k0 None end); fa2 <- (fun (T0 : Type) (k0 : option -> T0) => match fa1 with | Some x'0 => (return Some (fun v0 : expr ℕ -> (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q) => x'0 (x' v0))) T0 k0 | None => k0 None end); k fa2) | None => k None end); fa2 <- (fun (T : Type) (k : option -> T) => match fa1 with | Some x' => (return Some (fun v0 : expr ℕ -> (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q) => x' v0)) T k | None => k None end); match fa2 with | Some v0 => (idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); v1 <- base.try_make_transport_cps P b; v2 <- base.try_make_transport_cps b16 Q; v3 <- base.try_make_transport_cps Q Q; v4 <- base.try_make_transport_cps Q Q; Some (fv <-- v2 (Datatypes.nat_rect (fun _ : nat => expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b16 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))) -> UnderLets (expr (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b16 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))))) (v x) (fun (n' : nat) (rec : expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b16 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))) -> UnderLets (expr (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b16 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))))) (v5 : expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b16 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) => v0 x0 (##n')%expr rec v5) (let (x3, _) := idc_args0 in x3) (v1 x2)); Base (v4 (v3 fv)))%under_lets)%option | None => None end) | None => None end)%cps) | None => None end | _ => None end;;; Base (#(nat_rect_arrow)%expr @ (λ x3 : var P, to_expr (x ($x3)))%expr @ (λ (x3 : var ℕ)(x4 : var (P -> Q)%ptype)(x5 : var P), to_expr (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat)%option | @list_rect A P => fun (x : expr unit -> UnderLets (expr P)) (x0 : expr A -> expr (list A) -> expr P -> UnderLets (expr P)) (x1 : expr (list A)) => ((match pattern.type.unify_extracted_cps (((((unit -> '2%pbtype) -> ('1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype -> '2%pbtype) -> (pattern.base.type.list '1) -> '2%pbtype) -> unit -> '2%pbtype) -> '1%pbtype -> (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) with | Some (_, _, (_, (_, (_, _)), (_, _)), (_, _), (_, (_, (_, b12))), b) => _ <- ident.unify pattern.ident.list_rect list_rect; base.try_make_transport_cps P b12 (fun a13 : option => (fa <- (fun (T : Type) (k : option -> T) => match a13 with | Some x' => (return Some (fun v : expr unit -> UnderLets (expr P) => x' v)) T k | None => k None end); match fa with | Some v => base.try_make_transport_cps A b (fun a14 : option => fa0 <- (fun (T : Type) (k : option -> T) => match a14 with | Some x' => base.try_make_transport_cps A b (fun a15 : option => fa0 <- (fun (T0 : Type) (k0 : option -> T0) => match a15 with | Some x'0 => base.try_make_transport_cps P b12 (fun a16 : option => fa0 <- (fun (T1 : Type) (k1 : option -> T1) => match a16 with | Some x'1 => base.try_make_transport_cps P b12 (fun a17 : option => fa0 <- (fun (T2 : Type) (k2 : option -> T2) => match a17 with | Some x'2 => (return Some (fun v0 : expr b -> expr (list b) -> expr P -> UnderLets (expr P) => x'2 (x'1 v0))) T2 k2 | None => k2 None end); k1 fa0) | None => k1 None end); fa1 <- (fun (T1 : Type) (k1 : option -> T1) => match fa0 with | Some x'1 => (return Some (fun v0 : expr b -> expr (list A) -> expr P -> UnderLets (expr P) => x'1 (x'0 v0))) T1 k1 | None => k1 None end); k0 fa1) | None => k0 None end); fa1 <- (fun (T0 : Type) (k0 : option -> T0) => match fa0 with | Some x'0 => (return Some (fun v0 : expr A -> expr (list A) -> expr P -> UnderLets (expr P) => x'0 (x' v0))) T0 k0 | None => k0 None end); k fa1) | None => k None end); match fa0 with | Some v0 => v1 <- base.try_make_transport_cps A b; v2 <- base.try_make_transport_cps b12 P; (fv <- v2 (ls <- reflect_list (v1 x1); Some (Datatypes.list_rect (fun _ : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b12 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) => UnderLets (expr (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b12 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))))) (v x (##tt)%expr) (fun (x2 : expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b12 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) (xs : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b12 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))))) (rec : UnderLets (expr (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b12 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))))) => (rec' <-- rec; v0 x0 x2 (reify_list xs) rec')%under_lets) ls)); v3 <- base.try_make_transport_cps P P; v4 <- base.try_make_transport_cps P P; Some (fv0 <-- fv; Base (v4 (v3 fv0)))%under_lets)%option | None => None end) | None => None end)%cps) | None => None end;; None);;; Base (#(list_rect)%expr @ (λ x2 : var unit, to_expr (x ($x2)))%expr @ (λ (x2 : var A)(x3 : var (list A))(x4 : var P), to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat)%option | @list_case A P => fun (x : expr unit -> UnderLets (expr P)) (x0 : expr A -> expr (list A) -> UnderLets (expr P)) (x1 : expr (list A)) => ((match x1 with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.nil; match pattern.type.unify_extracted_cps (((((unit -> '2%pbtype) -> ('1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> (pattern.base.type.list '1) -> '2%pbtype) -> unit -> '2%pbtype) -> '1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> (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) => _ <- ident.unify pattern.ident.list_case list_case; base.try_make_transport_cps P b10 (fun a11 : option => (fa <- (fun (T : Type) (k : option -> T) => match a11 with | Some x' => (return Some (fun v : expr unit -> UnderLets (expr P) => x' v)) T k | None => k None end); match fa with | Some v => base.try_make_transport_cps A b (fun a12 : option => fa0 <- (fun (T : Type) (k : option -> T) => match a12 with | Some x' => base.try_make_transport_cps A b (fun a13 : option => fa0 <- (fun (T0 : Type) (k0 : option -> T0) => match a13 with | Some x'0 => base.try_make_transport_cps P b10 (fun a14 : option => fa0 <- (fun (T1 : Type) (k1 : option -> T1) => match a14 with | Some x'1 => (return Some (fun v0 : expr b -> expr (list A) -> UnderLets (expr P) => x'1 (x'0 v0))) T1 k1 | None => k1 None end); k0 fa0) | None => k0 None end); fa1 <- (fun (T0 : Type) (k0 : option -> T0) => match fa0 with | Some x'0 => (return Some (fun v0 : expr A -> expr (list A) -> UnderLets (expr P) => x'0 (x' v0))) T0 k0 | None => k0 None end); k fa1) | None => k None end); match fa0 with | Some _ => (_ <- ident.unify pattern.ident.nil nil; v1 <- base.try_make_transport_cps b10 P; v2 <- base.try_make_transport_cps P P; v3 <- base.try_make_transport_cps P P; Some (fv <-- v1 (v x (##tt)%expr); Base (v3 (v2 fv)))%under_lets)%option | None => None end) | None => None end)%cps) | None => None end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x3) x2 => args <- invert_bind_args idc Raw.ident.cons; match pattern.type.unify_extracted_cps (((((unit -> '2%pbtype) -> ('1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> (pattern.base.type.list '1) -> '2%pbtype) -> unit -> '2%pbtype) -> '1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> (('1%pbtype -> (pattern.base.type.list '1) -> (pattern.base.type.list '1)) -> '1%pbtype) -> (pattern.base.type.list '1))%ptype (((((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)), (_, (_, _), _, b11)) => _ <- ident.unify pattern.ident.list_case list_case; base.try_make_transport_cps P b10 (fun a15 : option => (fa <- (fun (T : Type) (k : option -> T) => match a15 with | Some x' => (return Some (fun v : expr unit -> UnderLets (expr P) => x' v)) T k | None => k None end); match fa with | Some _ => base.try_make_transport_cps A b11 (fun a16 : option => fa0 <- (fun (T : Type) (k : option -> T) => match a16 with | Some x' => base.try_make_transport_cps A b11 (fun a17 : option => fa0 <- (fun (T0 : Type) (k0 : option -> T0) => match a17 with | Some x'0 => base.try_make_transport_cps P b10 (fun a18 : option => fa0 <- (fun (T1 : Type) (k1 : option -> T1) => match a18 with | Some x'1 => (return Some (fun v0 : expr b11 -> expr (list A) -> UnderLets (expr P) => x'1 (x'0 v0))) T1 k1 | None => k1 None end); k0 fa0) | None => k0 None end); fa1 <- (fun (T0 : Type) (k0 : option -> T0) => match fa0 with | Some x'0 => (return Some (fun v0 : expr A -> expr (list A) -> UnderLets (expr P) => x'0 (x' v0))) T0 k0 | None => k0 None end); k fa1) | None => k None end); match fa0 with | Some v0 => (_ <- ident.unify pattern.ident.cons cons; v1 <- type.try_make_transport_cps s0 b11; v2 <- type.try_make_transport_cps s (list b11); v3 <- base.try_make_transport_cps b10 P; v4 <- base.try_make_transport_cps P P; v5 <- base.try_make_transport_cps P P; Some (fv <-- v3 (v0 x0 (v1 (Compile.reflect x3)) (v2 (Compile.reflect x2))); Base (v5 (v4 fv)))%under_lets)%option | None => None end) | None => None end)%cps) | None => None end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None | _ => None end;; None);;; Base (#(list_case)%expr @ (λ x2 : var unit, to_expr (x ($x2)))%expr @ (λ (x2 : var A)(x3 : var (list A)), to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat)%option | @List_length T => fun x : expr (list T) => (match pattern.type.unify_extracted_cps (((pattern.base.type.list '1) -> ℕ) -> (pattern.base.type.list '1))%ptype (((list T) -> ℕ) -> (list T))%ptype option (fun x0 : option => x0) with | Some (_, _, b) => _ <- ident.unify pattern.ident.List_length List_length; v <- base.try_make_transport_cps T b; x0 <- (xs <- reflect_list (v x); Some (##(length xs))%expr); Some (Base x0) | None => None end;;; Base (#(List_length)%expr @ x)%expr_pat)%option | List_seq => fun x x0 : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℕ -> ℕ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (fold_right (fun (x1 : expr ℕ) (xs : expr (list ℕ)) => (x1 :: xs)%expr_pat) []%expr_pat (map (fun v : nat => (##v)%expr) (seq (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1))))) | None => None end | _ => None end | _ => None end;; None);;; Base (#(List_seq)%expr @ x @ x0)%expr_pat)%option | @List_firstn A => fun (x : expr ℕ) (x0 : expr (list A)) => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((ℕ -> (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) => _ <- ident.unify pattern.ident.List_firstn List_firstn; idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); v <- base.try_make_transport_cps A b; v0 <- base.try_make_transport_cps b A; fv <- v0 (xs <- reflect_list (v x0); Some (Base (reify_list (firstn (let (x1, _) := idc_args0 in x1) xs)))); v1 <- base.try_make_transport_cps A A; v2 <- base.try_make_transport_cps A A; Some (fv0 <-- fv; Base (v2 (v1 fv0)))%under_lets | None => None end | _ => None end;; None);;; Base (#(List_firstn)%expr @ x @ x0)%expr_pat)%option | @List_skipn A => fun (x : expr ℕ) (x0 : expr (list A)) => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((ℕ -> (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) => _ <- ident.unify pattern.ident.List_skipn List_skipn; idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); v <- base.try_make_transport_cps A b; v0 <- base.try_make_transport_cps b A; fv <- v0 (xs <- reflect_list (v x0); Some (Base (reify_list (skipn (let (x1, _) := idc_args0 in x1) xs)))); v1 <- base.try_make_transport_cps A A; v2 <- base.try_make_transport_cps A A; Some (fv0 <-- fv; Base (v2 (v1 fv0)))%under_lets | None => None end | _ => None end;; None);;; Base (#(List_skipn)%expr @ x @ x0)%expr_pat)%option | @List_repeat A => fun (x : expr A) (x0 : expr ℕ) => ((match x0 with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((('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, _) => _ <- ident.unify pattern.ident.List_repeat List_repeat; v <- base.try_make_transport_cps A b0; idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); v0 <- base.try_make_transport_cps b0 A; v1 <- base.try_make_transport_cps A A; v2 <- base.try_make_transport_cps A A; Some (Base (v2 (v1 (v0 (reify_list (repeat (v x) (let (x1, _) := idc_args0 in x1))))))) | None => None end | _ => None end;; None);;; Base (#(List_repeat)%expr @ x @ x0)%expr_pat)%option | @List_combine A B => fun (x : expr (list A)) (x0 : expr (list B)) => (match pattern.type.unify_extracted_cps ((((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) => _ <- ident.unify pattern.ident.List_combine List_combine; v <- base.try_make_transport_cps A b0; v0 <- base.try_make_transport_cps B b; (trA <-- @base.try_make_transport_cps (fun A0 : base.type => option) b0 A; trB <-- @base.try_make_transport_cps (fun B0 : base.type => option) b B; return Some (fun v1 : option => trB (trA v1)))%cps option (fun tr : option => match tr with | Some v1 => x1 <- v1 (xs <- reflect_list (v x); ys <- reflect_list (v0 x0); Some (reify_list (map (fun '(x1, y) => (x1, y)%expr_pat) (combine xs ys)))); (trA <-- @base.try_make_transport_cps (fun A0 : base.type => expr (list (A0 * B))) A A; trB <-- @base.try_make_transport_cps (fun B0 : base.type => expr (list (A * B0))) B B; return Some (fun v2 : expr (list (A * B)) => trB (trA v2)))%cps option (fun tr0 : option => match tr0 with | Some v2 => (trA <-- @base.try_make_transport_cps (fun A0 : base.type => expr (list (A0 * B))) A A; trB <-- @base.try_make_transport_cps (fun B0 : base.type => expr (list (A * B0))) B B; return Some (fun v3 : expr (list (A * B)) => trB (trA v3)))%cps option (fun tr' : option => match tr' with | Some v3 => Some (Base (v3 (v2 x1))) | None => None end) | None => None end) | None => None end) | None => None end;;; Base (#(List_combine)%expr @ x @ x0)%expr_pat)%option | @List_map A B => fun (x : expr A -> UnderLets (expr B)) (x0 : expr (list A)) => ((match pattern.type.unify_extracted_cps (((('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) => _ <- ident.unify pattern.ident.List_map List_map; base.try_make_transport_cps A b (fun a5 : option => (fa <- (fun (T : Type) (k : option -> T) => match a5 with | Some x' => base.try_make_transport_cps B b4 (fun a6 : option => fa <- (fun (T0 : Type) (k0 : option -> T0) => match a6 with | Some x'0 => (return Some (fun v : expr A -> UnderLets (expr B) => x'0 (x' v))) T0 k0 | None => k0 None end); k fa) | None => k None end); match fa with | Some v => v0 <- base.try_make_transport_cps A b; v1 <- base.try_make_transport_cps b4 B; (fv <- v1 (ls <- reflect_list (v0 x0); Some (Datatypes.list_rect (fun _ : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) => UnderLets (expr (list (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))))) (Base []%expr_pat) (fun (x1 : expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) (_ : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))))) (rec : UnderLets (expr (list (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))))) => (rec' <-- rec; fx <-- v x x1; Base (fx :: rec')%expr_pat)%under_lets) ls)); v2 <- base.try_make_transport_cps B B; v3 <- base.try_make_transport_cps B B; Some (fv0 <-- fv; Base (v3 (v2 fv0)))%under_lets)%option | None => None end)%cps) | None => None end;; None);;; Base (#(List_map)%expr @ (λ x1 : var A, to_expr (x ($x1)))%expr @ x0)%expr_pat)%option | @List_app A => fun x x0 : expr (list A) => ((match pattern.type.unify_extracted_cps ((((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) => _ <- ident.unify pattern.ident.List_app List_app; v <- base.try_make_transport_cps A b; v0 <- base.try_make_transport_cps A b; v1 <- base.try_make_transport_cps b A; fv <- v1 (ls <- reflect_list (v x); Some (Datatypes.list_rect (fun _ : Datatypes.list (expr b) => UnderLets (expr (pattern.base.subst_default (pattern.base.type.list '1) (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) (Base (v0 x0)) (fun (x1 : expr b) (_ : Datatypes.list (expr b)) (rec : UnderLets (expr (pattern.base.subst_default (pattern.base.type.list '1) (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) => (rec' <-- rec; Base (x1 :: rec')%expr_pat)%under_lets) ls)); v2 <- base.try_make_transport_cps A A; v3 <- base.try_make_transport_cps A A; Some (fv0 <-- fv; Base (v3 (v2 fv0)))%under_lets | None => None end;; None);;; Base (x ++ x0)%expr)%option | @List_rev A => fun x : expr (list A) => ((match pattern.type.unify_extracted_cps (((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) with | Some (_, _, b) => _ <- ident.unify pattern.ident.List_rev List_rev; v <- base.try_make_transport_cps A b; v0 <- base.try_make_transport_cps b A; fv <- v0 (xs <- reflect_list (v x); Some (Base (reify_list (rev xs)))); v1 <- base.try_make_transport_cps A A; v2 <- base.try_make_transport_cps A A; Some (fv0 <-- fv; Base (v2 (v1 fv0)))%under_lets | None => None end;; None);;; Base (#(List_rev)%expr @ x)%expr_pat)%option | @List_flat_map A B => fun (x : expr A -> UnderLets (expr (list B))) (x0 : expr (list A)) => ((match pattern.type.unify_extracted_cps (((('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) with | Some (_, _, (_, _), (_, b4), b) => _ <- ident.unify pattern.ident.List_flat_map List_flat_map; base.try_make_transport_cps A b (fun a5 : option => (fa <- (fun (T : Type) (k : option -> T) => match a5 with | Some x' => base.try_make_transport_cps B b4 (fun a6 : option => fa <- (fun (T0 : Type) (k0 : option -> T0) => match a6 with | Some x'0 => (return Some (fun v : expr A -> UnderLets (expr (list B)) => x'0 (x' v))) T0 k0 | None => k0 None end); k fa) | None => k None end); match fa with | Some v => v0 <- base.try_make_transport_cps A b; v1 <- base.try_make_transport_cps b4 B; (fv <- v1 (ls <- reflect_list (v0 x0); Some (Datatypes.list_rect (fun _ : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) => UnderLets (expr (list b4))) (Base []%expr_pat) (fun (x1 : expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) (_ : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b4 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))))) (rec : UnderLets (expr (list b4))) => (rec' <-- rec; fx <-- v x x1; Base ($fx ++ rec')%expr)%under_lets) ls)); v2 <- base.try_make_transport_cps B B; v3 <- base.try_make_transport_cps B B; Some (fv0 <-- fv; fv1 <-- do_again (list B) (v2 fv0); Base (v3 fv1))%under_lets)%option | None => None end)%cps) | None => None end;; None);;; Base (#(List_flat_map)%expr @ (λ x1 : var A, to_expr (x ($x1)))%expr @ x0)%expr_pat)%option | @List_partition A => fun (x : expr A -> UnderLets (expr bool)) (x0 : expr (list A)) => ((match pattern.type.unify_extracted_cps (((('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) with | Some (_, _, (_, (_, _)), (_, _), b) => _ <- ident.unify pattern.ident.List_partition List_partition; base.try_make_transport_cps A b (fun a6 : option => (fa <- (fun (T : Type) (k : option -> T) => match a6 with | Some x' => (return Some (fun v : expr A -> UnderLets (expr bool) => x' v)) T (fun fa : option => k fa) | None => k None end); match fa with | Some v => v0 <- base.try_make_transport_cps A b; base.try_make_transport_cps b A (fun a7 : option => fa0 <- (fun (T : Type) (k : option -> T) => match a7 with | Some x' => base.try_make_transport_cps b A (fun a8 : option => fa0 <- (fun (T0 : Type) (k0 : option -> T0) => match a8 with | Some x'0 => (return Some (fun v1 : option => x'0 (x' v1))) T0 k0 | None => k0 None end); k fa0) | None => k None end); match fa0 with | Some v1 => (fv <- v1 (ls <- reflect_list (v0 x0); Some (Datatypes.list_rect (fun _ : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))) => UnderLets (expr (list (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))) * list (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))%etype)) (Base ([], [])%expr_pat) (fun (x1 : expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))) (_ : Datatypes.list (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))) (rec : UnderLets (expr (list (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))) * list (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type))))%etype)) => (rec' <-- rec; fx <-- v x x1; Base (#(prod_rect)%expr @ (λ g d : expr (list (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))), (#(bool_rect)%expr @ (λ _ : expr unit, ($x1 :: $g, $d)%expr_pat) @ (λ _ : expr unit, ($g, $x1 :: $d)%expr_pat) @ $fx)%expr_pat)%expr @ rec')%expr_pat)%under_lets) ls)); base.try_make_transport_cps A A (fun a8 : option => (fa1 <- (fun (T : Type) (k : option -> T) => match a8 with | Some x' => base.try_make_transport_cps A A (fun a9 : option => fa1 <- (fun (T0 : Type) (k0 : option -> T0) => match a9 with | Some x'0 => (return Some (fun v2 : expr (list A * list A)%etype => x'0 (x' v2))) T0 k0 | None => k0 None end); k fa1) | None => k None end); match fa1 with | Some v2 => base.try_make_transport_cps A A (fun a9 : option => fa2 <- (fun (T : Type) (k : option -> T) => match a9 with | Some x' => base.try_make_transport_cps A A (fun a10 : option => fa2 <- (fun (T0 : Type) (k0 : option -> T0) => match a10 with | Some x'0 => (return Some (fun v3 : expr (list A * list A)%etype => x'0 (x' v3))) T0 k0 | None => k0 None end); k fa2) | None => k None end); match fa2 with | Some v3 => Some (fv0 <-- fv; fv1 <-- do_again (list A * list A) (v2 fv0); Base (v3 fv1))%under_lets | None => None end) | None => None end)%cps))%option | None => None end) | None => None end)%cps) | None => None end;; None);;; Base (#(List_partition)%expr @ (λ x1 : var A, to_expr (x ($x1)))%expr @ x0)%expr_pat)%option | @List_fold_right A B => fun (x : expr B -> expr A -> UnderLets (expr A)) (x0 : expr A) (x1 : expr (list B)) => ((match pattern.type.unify_extracted_cps ((((('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) with | Some (_, (_, _), (_, (_, _)), (_, (_, _)), b0, b) => _ <- ident.unify pattern.ident.List_fold_right List_fold_right; base.try_make_transport_cps B b (fun a9 : option => (fa <- (fun (T : Type) (k : option -> T) => match a9 with | Some x' => base.try_make_transport_cps A b0 (fun a10 : option => fa <- (fun (T0 : Type) (k0 : option -> T0) => match a10 with | Some x'0 => base.try_make_transport_cps A b0 (fun a11 : option => fa <- (fun (T1 : Type) (k1 : option -> T1) => match a11 with | Some x'1 => (return Some (fun v : expr b -> expr A -> UnderLets (expr A) => x'1 (x'0 v))) T1 k1 | None => k1 None end); k0 fa) | None => k0 None end); fa0 <- (fun (T0 : Type) (k0 : option -> T0) => match fa with | Some x'0 => (return Some (fun v : expr B -> expr A -> UnderLets (expr A) => x'0 (x' v))) T0 k0 | None => k0 None end); k fa0) | None => k None end); match fa with | Some v => v0 <- base.try_make_transport_cps A b0; v1 <- base.try_make_transport_cps B b; v2 <- base.try_make_transport_cps b0 A; (fv <- v2 (ls <- reflect_list (v1 x1); Some (Datatypes.list_rect (fun _ : Datatypes.list (expr (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b (PositiveMap.add (PositiveSet.rev 1%positive) b0 (PositiveMap.empty base.type))))) => UnderLets (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b (PositiveMap.add (PositiveSet.rev 1%positive) b0 (PositiveMap.empty base.type)))))) (Base (v0 x0)) (fun (x2 : expr (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b (PositiveMap.add (PositiveSet.rev 1%positive) b0 (PositiveMap.empty base.type))))) (_ : Datatypes.list (expr (pattern.base.subst_default '2 (PositiveMap.add (PositiveSet.rev 2%positive) b (PositiveMap.add (PositiveSet.rev 1%positive) b0 (PositiveMap.empty base.type)))))) (rec : UnderLets (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 2%positive) b (PositiveMap.add (PositiveSet.rev 1%positive) b0 (PositiveMap.empty base.type)))))) => (rec' <-- rec; v x x2 rec')%under_lets) ls)); v3 <- base.try_make_transport_cps A A; v4 <- base.try_make_transport_cps A A; Some (fv0 <-- fv; Base (v4 (v3 fv0)))%under_lets)%option | None => None end)%cps) | None => None end;; None);;; Base (#(List_fold_right)%expr @ (λ (x2 : var B)(x3 : var A), to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat)%option | @List_update_nth T => fun (x : expr ℕ) (x0 : expr T -> UnderLets (expr T)) (x1 : expr (list T)) => (match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((((ℕ -> ('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) with | Some (_, (_, _, (_, _)), _, (_, _), b) => _ <- ident.unify pattern.ident.List_update_nth List_update_nth; idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); base.try_make_transport_cps T b (fun a7 : option => (fa <- (fun (T0 : Type) (k : option -> T0) => match a7 with | Some x' => base.try_make_transport_cps T b (fun a8 : option => fa <- (fun (T1 : Type) (k0 : option -> T1) => match a8 with | Some x'0 => (return Some (fun v : expr T -> UnderLets (expr T) => x'0 (x' v))) T1 k0 | None => k0 None end); k fa) | None => k None end); match fa with | Some v => v0 <- base.try_make_transport_cps T b; v1 <- base.try_make_transport_cps b T; (fv <- v1 (ls <- reflect_list (v0 x1); Some (retv <---- update_nth (let (x2, _) := idc_args0 in x2) (fun x2 : UnderLets (expr (pattern.base.subst_default '1 (PositiveMap.add (PositiveSet.rev 1%positive) b (PositiveMap.empty base.type)))) => x3 <-- x2; v x0 x3) (map Base ls); Base (reify_list retv))%under_lets); v2 <- base.try_make_transport_cps T T; v3 <- base.try_make_transport_cps T T; Some (fv0 <-- fv; Base (v3 (v2 fv0)))%under_lets)%option | None => None end)%cps) | None => None end | _ => None end;;; Base (#(List_update_nth)%expr @ x @ (λ x2 : var T, to_expr (x0 ($x2)))%expr @ x1)%expr_pat)%option | @List_nth_default T => fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => ((match x1 with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((('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) with | Some (_, (_, (_, _)), _, b0, _) => _ <- ident.unify pattern.ident.List_nth_default List_nth_default; v <- base.try_make_transport_cps T b0; v0 <- base.try_make_transport_cps T b0; idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); v1 <- base.try_make_transport_cps b0 T; x2 <- v1 (ls <- reflect_list (v0 x0); Some (nth_default (v x) ls (let (x2, _) := idc_args0 in x2))); v2 <- base.try_make_transport_cps T T; v3 <- base.try_make_transport_cps T T; Some (Base (v3 (v2 x2))) | None => None end | _ => None end;; None);;; Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) + (let (x1, _) := idc_args0 in x1))%Z)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x + x0)%expr)%option | Z_mul => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) * (let (x1, _) := idc_args0 in x1))%Z)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x * x0)%expr)%option | Z_pow => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) ^ (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Z_pow)%expr @ x @ x0)%expr_pat)%option | Z_sub => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) - (let (x1, _) := idc_args0 in x1))%Z)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x - x0)%expr)%option | Z_opp => fun x : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℤ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(- (let (x0, _) := idc_args in x0))%Z)%expr) | None => None end | _ => None end;; None);;; Base (- x)%expr)%option | Z_div => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) / (let (x1, _) := idc_args0 in x1))%Z)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x / x0)%expr)%option | Z_modulo => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) mod (let (x1, _) := idc_args0 in x1))%Z)%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x mod x0)%expr)%option | Z_log2 => fun x : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℤ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.log2 (let (x0, _) := idc_args in x0)))%expr) | None => None end | _ => None end;; None);;; Base (#(Z_log2)%expr @ x)%expr_pat)%option | Z_log2_up => fun x : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℤ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.log2_up (let (x0, _) := idc_args in x0)))%expr) | None => None end | _ => None end;; None);;; Base (#(Z_log2_up)%expr @ x)%expr_pat)%option | Z_eqb => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) =? (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Z_eqb)%expr @ x @ x0)%expr_pat)%option | Z_leb => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) <=? (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Z_leb)%expr @ x @ x0)%expr_pat)%option | Z_geb => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##((let (x1, _) := idc_args in x1) >=? (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Z_geb)%expr @ x @ x0)%expr_pat)%option | Z_of_nat => fun x : expr ℕ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℕ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.of_nat (let (x0, _) := idc_args in x0)))%expr) | None => None end | _ => None end;; None);;; Base (#(Z_of_nat)%expr @ x)%expr_pat)%option | Z_to_nat => fun x : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℤ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.to_nat (let (x0, _) := idc_args in x0)))%expr) | None => None end | _ => None end;; None);;; Base (#(Z_to_nat)%expr @ x)%expr_pat)%option | Z_shiftr => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.shiftr (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x >> x0)%expr)%option | Z_shiftl => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.shiftl (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x << x0)%expr)%option | Z_land => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.land (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x &' x0)%expr)%option | Z_lor => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Z.lor (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (x || x0)%expr)%option | Z_bneg => fun x : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => args <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ℤ (projT1 args) option (fun x0 : option => x0) with | Some _ => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Definitions.Z.bneg (let (x0, _) := idc_args in x0)))%expr) | None => None end | _ => None end;; None);;; Base (#(Z_bneg)%expr @ x)%expr_pat)%option | Z_lnot_modulo => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Definitions.Z.lnot_modulo (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Z_lnot_modulo)%expr @ x @ x0)%expr_pat)%option | Z_mul_split => fun x x0 x1 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => args <- invert_bind_args idc1 Raw.ident.Literal; args0 <- invert_bind_args idc0 Raw.ident.Literal; args1 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x2 : option => x2) with | Some (_, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (let '(a1, b1) := Definitions.Z.mul_split (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2) in ((##a1)%expr, (##b1)%expr)%expr_pat)) | None => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_get_carry => fun x x0 x1 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => args <- invert_bind_args idc1 Raw.ident.Literal; args0 <- invert_bind_args idc0 Raw.ident.Literal; args1 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x2 : option => x2) with | Some (_, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (let '(a1, b1) := Definitions.Z.add_get_carry_full (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2) in ((##a1)%expr, (##b1)%expr)%expr_pat)) | None => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_with_carry => fun x x0 x1 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => args <- invert_bind_args idc1 Raw.ident.Literal; args0 <- invert_bind_args idc0 Raw.ident.Literal; args1 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x2 : option => x2) with | Some (_, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Definitions.Z.add_with_carry (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2)))%expr) | None => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_with_get_carry => fun x x0 x1 x2 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => match x2 with | @expr.Ident _ _ _ t2 idc2 => args <- invert_bind_args idc2 Raw.ident.Literal; args0 <- invert_bind_args idc1 Raw.ident.Literal; args1 <- invert_bind_args idc0 Raw.ident.Literal; args2 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype ((((projT1 args2) -> (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x3 : option => x3) with | Some (_, _, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args2); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args2 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (let '(a2, b2) := Definitions.Z.add_with_get_carry_full (let (x3, _) := idc_args in x3) (let (x3, _) := idc_args0 in x3) (let (x3, _) := idc_args1 in x3) (let (x3, _) := idc_args2 in x3) in ((##a2)%expr, (##b2)%expr)%expr_pat)) | None => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option | Z_sub_get_borrow => fun x x0 x1 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => args <- invert_bind_args idc1 Raw.ident.Literal; args0 <- invert_bind_args idc0 Raw.ident.Literal; args1 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x2 : option => x2) with | Some (_, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (let '(a1, b1) := Definitions.Z.sub_get_borrow_full (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2) in ((##a1)%expr, (##b1)%expr)%expr_pat)) | None => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_sub_with_get_borrow => fun x x0 x1 x2 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => match x2 with | @expr.Ident _ _ _ t2 idc2 => args <- invert_bind_args idc2 Raw.ident.Literal; args0 <- invert_bind_args idc1 Raw.ident.Literal; args1 <- invert_bind_args idc0 Raw.ident.Literal; args2 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype ((((projT1 args2) -> (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x3 : option => x3) with | Some (_, _, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args2); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args2 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (let '(a2, b2) := Definitions.Z.sub_with_get_borrow_full (let (x3, _) := idc_args in x3) (let (x3, _) := idc_args0 in x3) (let (x3, _) := idc_args1 in x3) (let (x3, _) := idc_args2 in x3) in ((##a2)%expr, (##b2)%expr)%expr_pat)) | None => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option | Z_zselect => fun x x0 x1 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => args <- invert_bind_args idc1 Raw.ident.Literal; args0 <- invert_bind_args idc0 Raw.ident.Literal; args1 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x2 : option => x2) with | Some (_, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Definitions.Z.zselect (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2)))%expr) | None => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_zselect)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_modulo => fun x x0 x1 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => args <- invert_bind_args idc1 Raw.ident.Literal; args0 <- invert_bind_args idc0 Raw.ident.Literal; args1 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x2 : option => x2) with | Some (_, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Definitions.Z.add_modulo (let (x2, _) := idc_args in x2) (let (x2, _) := idc_args0 in x2) (let (x2, _) := idc_args1 in x2)))%expr) | None => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_rshi => fun x x0 x1 x2 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => match x1 with | @expr.Ident _ _ _ t1 idc1 => match x2 with | @expr.Ident _ _ _ t2 idc2 => args <- invert_bind_args idc2 Raw.ident.Literal; args0 <- invert_bind_args idc1 Raw.ident.Literal; args1 <- invert_bind_args idc0 Raw.ident.Literal; args2 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype ((((projT1 args2) -> (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype option (fun x3 : option => x3) with | Some (_, _, _, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args2); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args2 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Definitions.Z.rshi (let (x3, _) := idc_args in x3) (let (x3, _) := idc_args0 in x3) (let (x3, _) := idc_args1 in x3) (let (x3, _) := idc_args2 in x3)))%expr) | None => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option | Z_cc_m => fun x x0 : expr ℤ => ((match x with | @expr.Ident _ _ _ t idc => match x0 with | @expr.Ident _ _ _ t0 idc0 => args <- invert_bind_args idc0 Raw.ident.Literal; args0 <- invert_bind_args idc Raw.ident.Literal; match pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype ((projT1 args0) -> (projT1 args))%ptype option (fun x1 : option => x1) with | Some (_, _) => idc_args <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args0 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(Definitions.Z.cc_m (let (x1, _) := idc_args in x1) (let (x1, _) := idc_args0 in x1)))%expr) | None => None end | _ => None end | _ => None end;; None);;; Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat)%option | Z_cast range => fun x : expr ℤ => Base (#(Z_cast range)%expr @ x)%expr_pat | Z_cast2 range => fun x : expr (ℤ * ℤ)%etype => Base (#(Z_cast2 range)%expr @ x)%expr_pat | fancy_add log2wordmax imm => fun x : expr (ℤ * ℤ)%etype => Base (#(fancy_add log2wordmax imm)%expr @ x)%expr_pat | fancy_addc log2wordmax imm => fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_addc log2wordmax imm)%expr @ x)%expr_pat | fancy_sub log2wordmax imm => fun x : expr (ℤ * ℤ)%etype => Base (#(fancy_sub log2wordmax imm)%expr @ x)%expr_pat | fancy_subb log2wordmax imm => fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_subb log2wordmax imm)%expr @ x)%expr_pat | fancy_mulll log2wordmax => fun x : expr (ℤ * ℤ)%etype => Base (#(fancy_mulll log2wordmax)%expr @ x)%expr_pat | fancy_mullh log2wordmax => fun x : expr (ℤ * ℤ)%etype => Base (#(fancy_mullh log2wordmax)%expr @ x)%expr_pat | fancy_mulhl log2wordmax => fun x : expr (ℤ * ℤ)%etype => Base (#(fancy_mulhl log2wordmax)%expr @ x)%expr_pat | fancy_mulhh log2wordmax => fun x : expr (ℤ * ℤ)%etype => Base (#(fancy_mulhh log2wordmax)%expr @ x)%expr_pat | fancy_rshi log2wordmax x => fun x0 : expr (ℤ * ℤ)%etype => Base (#(fancy_rshi log2wordmax x)%expr @ x0)%expr_pat | fancy_selc => fun x : expr (ℤ * ℤ * ℤ)%etype => ((match x with | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.Ident _ _ _ t3 idc3)%expr_pat => args <- invert_bind_args idc3 Raw.ident.Literal; args0 <- invert_bind_args idc2 Raw.ident.Literal; args1 <- invert_bind_args idc1 Raw.ident.Literal; args2 <- invert_bind_args idc0 Raw.ident.pair; args3 <- invert_bind_args idc Raw.ident.pair; match pattern.type.unify_extracted_cps ((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) -> ((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype ((((let (x4, _) := args3 in x4) -> (let (_, y) := args3 in y) -> ((let (x4, _) := args3 in x4) * (let (_, y) := args3 in y))%etype) -> (((let (x4, _) := args2 in x4) -> (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 (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _) => _ <- ident.unify pattern.ident.pair pair; _ <- ident.unify pattern.ident.pair pair; idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args2 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args3 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(fancy.interp (invert_Some (to_fancy fancy_selc)) (let (x4, _) := idc_args1 in x4, let (x4, _) := idc_args2 in x4, let (x4, _) := idc_args3 in x4)%core))%expr) | None => None end | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ ($_)%expr)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.Abs _ _ _ _ _ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ (_ @ _))%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ ($_)%expr) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ (_ @ _)) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ (_ @ _) @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (#(_) @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (($_)%expr @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (($_)%expr @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (_ @ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; None);;; Base (#(fancy_selc)%expr @ x)%expr_pat)%option | fancy_selm log2wordmax => fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_selm log2wordmax)%expr @ x)%expr_pat | fancy_sell => fun x : expr (ℤ * ℤ * ℤ)%etype => ((match x with | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.Ident _ _ _ t3 idc3)%expr_pat => args <- invert_bind_args idc3 Raw.ident.Literal; args0 <- invert_bind_args idc2 Raw.ident.Literal; args1 <- invert_bind_args idc1 Raw.ident.Literal; args2 <- invert_bind_args idc0 Raw.ident.pair; args3 <- invert_bind_args idc Raw.ident.pair; match pattern.type.unify_extracted_cps ((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) -> ((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype ((((let (x4, _) := args3 in x4) -> (let (_, y) := args3 in y) -> ((let (x4, _) := args3 in x4) * (let (_, y) := args3 in y))%etype) -> (((let (x4, _) := args2 in x4) -> (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 (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _) => _ <- ident.unify pattern.ident.pair pair; _ <- ident.unify pattern.ident.pair pair; idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args2 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args3 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(fancy.interp (invert_Some (to_fancy fancy_sell)) (let (x4, _) := idc_args1 in x4, let (x4, _) := idc_args2 in x4, let (x4, _) := idc_args3 in x4)%core))%expr) | None => None end | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ ($_)%expr)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.Abs _ _ _ _ _ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ (_ @ _))%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ ($_)%expr) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ (_ @ _)) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ (_ @ _) @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (#(_) @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (($_)%expr @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (($_)%expr @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (_ @ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; None);;; Base (#(fancy_sell)%expr @ x)%expr_pat)%option | fancy_addm => fun x : expr (ℤ * ℤ * ℤ)%etype => ((match x with | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.Ident _ _ _ t3 idc3)%expr_pat => args <- invert_bind_args idc3 Raw.ident.Literal; args0 <- invert_bind_args idc2 Raw.ident.Literal; args1 <- invert_bind_args idc1 Raw.ident.Literal; args2 <- invert_bind_args idc0 Raw.ident.pair; args3 <- invert_bind_args idc Raw.ident.pair; match pattern.type.unify_extracted_cps ((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) -> ((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype ((((let (x4, _) := args3 in x4) -> (let (_, y) := args3 in y) -> ((let (x4, _) := args3 in x4) * (let (_, y) := args3 in y))%etype) -> (((let (x4, _) := args2 in x4) -> (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 (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _) => _ <- ident.unify pattern.ident.pair pair; _ <- ident.unify pattern.ident.pair pair; idc_args1 <- ident.unify pattern.ident.Literal ##(projT2 args1); idc_args2 <- ident.unify pattern.ident.Literal ##(projT2 args0); idc_args3 <- ident.unify pattern.ident.Literal ##(projT2 args); Some (Base (##(fancy.interp (invert_Some (to_fancy fancy_addm)) (let (x4, _) := idc_args1 in x4, let (x4, _) := idc_args2 in x4, let (x4, _) := idc_args3 in x4)%core))%expr) | None => None end | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ ($_)%expr)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.Abs _ _ _ _ _ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ (_ @ _))%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident _ _ _ t2 idc2) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ ($_)%expr) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ _ _ _ _ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ (_ @ _)) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.LetIn _ _ _ _ _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ (_ @ _) @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t idc @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (#(_) @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (($_)%expr @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (($_)%expr @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (_ @ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t idc @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; None);;; Base (#(fancy_addm)%expr @ x)%expr_pat)%option end : Compile.value' true t