nbe_rewrite_head = match idc in (ident t) return (Compile.value' true t) with | @ident.Literal t v => match t as t0 return (base.base_interp t0 -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base t0))) with | base.type.unit => fun v0 : unit => UnderLets.Base (##v0)%expr | base.type.Z => fun v0 : Z => UnderLets.Base (##v0)%expr | base.type.bool => fun v0 : bool => UnderLets.Base (##v0)%expr | base.type.nat => fun v0 : nat => UnderLets.Base (##v0)%expr end v | ident.Nat_succ => fun x : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Some (UnderLets.Base (##(Nat.succ args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Nat_succ)%expr @ x)%expr_pat)%option | ident.Nat_pred => fun x : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Some (UnderLets.Base (##(Nat.pred args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Nat_pred)%expr @ x)%expr_pat)%option | ident.Nat_max => fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralNat; Some (UnderLets.Base (##(Nat.max args args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Nat_max)%expr @ x @ x0)%expr_pat)%option | ident.Nat_mul => fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralNat; Some (UnderLets.Base (##(args * args0)%nat)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Nat_mul)%expr @ x @ x0)%expr_pat)%option | ident.Nat_add => fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralNat; Some (UnderLets.Base (##(args + args0)%nat)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Nat_add)%expr @ x @ x0)%expr_pat)%option | ident.Nat_sub => fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralNat; Some (UnderLets.Base (##(args - args0)%nat)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Nat_sub)%expr @ x @ x0)%expr_pat)%option | @ident.nil t => UnderLets.Base []%expr_pat | @ident.cons t => fun (x : defaults.expr (type.base t)) (x0 : defaults.expr (type.base (base.type.list t))) => UnderLets.Base (x :: x0)%expr_pat | @ident.pair A B => fun (x : defaults.expr (type.base A)) (x0 : defaults.expr (type.base B)) => UnderLets.Base (x, x0)%expr_pat | @ident.fst A B => fun x : defaults.expr (type.base (A * B)%etype) => ((match x with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match s0 as t2 return (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) with | type.base t2 => fun v : defaults.expr (type.base t2) => match s as t3 return (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) with | type.base t3 => fun _ : defaults.expr (type.base t3) => Some (base.try_make_transport_cps t2 A (fun a : option (defaults.expr (type.base t2) -> defaults.expr (type.base A)) => match a with | Some x' => UnderLets.Base (x' v) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.fst) @ (??, ??)) (#(ident.fst)%expr @ x)%expr_pat) end)) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x0) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x1) | @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);;; UnderLets.Base (#(ident.fst)%expr @ x)%expr_pat)%option | @ident.snd A B => fun x : defaults.expr (type.base (A * B)%etype) => ((match x with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match s0 as t2 return (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base B)))) with | type.base t2 => fun _ : defaults.expr (type.base t2) => match s as t3 return (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base B)))) with | type.base t3 => fun v0 : defaults.expr (type.base t3) => Some (base.try_make_transport_cps t3 B (fun a : option (defaults.expr (type.base t3) -> defaults.expr (type.base B)) => match a with | Some x' => UnderLets.Base (x' v0) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.snd) @ (??, ??)) (#(ident.snd)%expr @ x)%expr_pat) end)) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x0) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x1) | @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);;; UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat)%option | @ident.prod_rect A B T => fun (x : defaults.expr (type.base A) -> defaults.expr (type.base B) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base T))) (x0 : defaults.expr (type.base (A * B)%etype)) => ((match x0 with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x2) x1 => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match s0 as t2 return (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) with | type.base t2 => fun v : defaults.expr (type.base t2) => match s as t3 return (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) with | type.base t3 => fun v0 : defaults.expr (type.base t3) => Compile.castbe v (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) (fun x3 : option (defaults.expr (type.base A)) => (x4 <- x3; Some (Compile.castbe v0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) (fun y : option (defaults.expr (type.base B)) => (y0 <- y; Some (Some (fv <-- (e <-- x x4 y0; UnderLets.Base {| anyexpr_ty := T; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) T (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base T)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.prod_rect) @ ??{?? -> ?? -> ??} @ (??, ??)) (#(ident.prod_rect)%expr @ (λ (x5 : var (type.base A)) (x6 : var (type.base B)), UnderLets.to_expr (x ($x5) ($x6)))%expr @ x0)%expr_pat) end))%under_lets));;; None)));;; None) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x1) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x2) | @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);;; UnderLets.Base (#(ident.prod_rect)%expr @ (λ (x1 : var (type.base A))(x2 : var (type.base B)), UnderLets.to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat)%option | @ident.bool_rect T => fun (x x0 : defaults.expr (type.base base.type.unit) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base T))) (x1 : defaults.expr (type.base base.type.bool)) => ((match x1 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralBool; Some (fv <-- (e <-- (if args as b return (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (if b then T else T)))) then x (##tt)%expr else x0 (##tt)%expr); UnderLets.Base {| anyexpr_ty := if args then T else T; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) T (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base T)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.bool_rect) @ ??{() -> ??} @ ??{() -> ??} @ #(pattern.ident.LiteralBool)) (#(ident.bool_rect)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat) end))%under_lets | _ => None end;; None);;; UnderLets.Base (#(ident.bool_rect)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat)%option | @ident.nat_rect P => fun (x : defaults.expr (type.base base.type.unit) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x0 : defaults.expr (type.base base.type.nat) -> defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x1 : defaults.expr (type.base base.type.nat)) => ((match x1 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) (fun S_case : option (defaults.expr (type.base base.type.nat) -> defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) => (S_case0 <- S_case; Some (Some (fv <-- (e <-- nat_rect (fun _ : nat => UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x (##tt)%expr) (fun (n' : nat) (rec : UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) => rec0 <-- rec; S_case0 (##n')%expr rec0) args; UnderLets.Base {| anyexpr_ty := P; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) P (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base P)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.nat_rect) @ ??{() -> ??} @ ??{type.base base.type.nat -> ?? -> ??} @ #(pattern.ident.LiteralNat)) (#(ident.nat_rect)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ (x2 : var (type.base base.type.nat)) (x3 : var (type.base P)), UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat) end))%under_lets));;; None) | _ => None end;; None);;; UnderLets.Base (#(ident.nat_rect)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ (x2 : var (type.base base.type.nat))(x3 : var (type.base P)), UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat)%option | @ident.nat_rect_arrow P Q => fun (x : defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q))) (x0 : defaults.expr (type.base base.type.nat) -> (defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q))) -> defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q))) (x1 : defaults.expr (type.base base.type.nat)) (x2 : defaults.expr (type.base P)) => (match x1 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q)))) (fun S_case : option (defaults.expr (type.base base.type.nat) -> (defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q))) -> defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q))) => (S_case0 <- S_case; Some (Compile.castbe x2 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q)))) (fun v : option (defaults.expr (type.base P)) => (v0 <- v; Some (Some (fv <-- (e <-- nat_rect (fun _ : nat => defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q))) x (fun (n' : nat) (rec : defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q))) (v1 : defaults.expr (type.base P)) => S_case0 (##n')%expr rec v1) args v0; UnderLets.Base {| anyexpr_ty := Q; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) Q (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base Q)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.nat_rect_arrow) @ ??{?? -> ??} @ ??{type.base base.type.nat -> (?? -> ??) -> ?? -> ??} @ #(pattern.ident.LiteralNat) @ ??) (#(ident.nat_rect_arrow)%expr @ (λ x3 : var (type.base P), UnderLets.to_expr (x ($x3)))%expr @ (λ (x3 : var (type.base base.type.nat)) (x4 : var (type.base P -> type.base Q)%ptype) (x5 : var (type.base P)), UnderLets.to_expr (x0 ($x3) (fun x6 : defaults.expr (type.base P) => UnderLets.Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat) end))%under_lets));;; None)));;; None) | _ => None end;;; UnderLets.Base (#(ident.nat_rect_arrow)%expr @ (λ x3 : var (type.base P), UnderLets.to_expr (x ($x3)))%expr @ (λ (x3 : var (type.base base.type.nat))(x4 : var (type.base P -> type.base Q)%ptype) (x5 : var (type.base P)), UnderLets.to_expr (x0 ($x3) (fun x6 : defaults.expr (type.base P) => UnderLets.Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat)%option | @ident.list_rect A P => fun (x : defaults.expr (type.base base.type.unit) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x0 : defaults.expr (type.base A) -> defaults.expr (type.base (base.type.list A)) -> defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x1 : defaults.expr (type.base (base.type.list A))) => ((Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) (fun Pcons : option (defaults.expr (type.base A) -> defaults.expr (type.base (base.type.list A)) -> defaults.expr (type.base P) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) => (Pcons0 <- Pcons; Some (reflect_list_cps x1 (fun ls : option (list (defaults.expr (type.base A))) => (ls0 <- ls; Some (Some (fv <-- (e <-- list_rect (fun _ : list (defaults.expr (type.base A)) => UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x (##tt)%expr) (fun (x2 : defaults.expr (type.base A)) (xs : list (defaults.expr (type.base A))) (rec : UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) => rec' <-- rec; Pcons0 x2 (reify_list xs) rec') ls0; UnderLets.Base {| anyexpr_ty := P; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) P (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base P)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.list_rect) @ ??{() -> ??} @ ??{?? -> ?? -> ?? -> ??} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.list_rect)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ (x2 : var (type.base A))(x3 : var (type.base (base.type.list A))) (x4 : var (type.base P)), UnderLets.to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat) end))%under_lets));;; None)));;; None);; None);;; UnderLets.Base (#(ident.list_rect)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ (x2 : var (type.base A))(x3 : var (type.base (base.type.list A))) (x4 : var (type.base P)), UnderLets.to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat)%option | @ident.list_case A P => fun (x : defaults.expr (type.base base.type.unit) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x0 : defaults.expr (type.base A) -> defaults.expr (type.base (base.type.list A)) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x1 : defaults.expr (type.base (base.type.list A))) => ((match x1 with | @expr.Ident _ _ _ t idc => _ <- pattern.ident.invert_bind_args idc pattern.ident.nil; Some (fv <-- (e <-- x (##tt)%expr; UnderLets.Base {| anyexpr_ty := P; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) P (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base P)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.list_case) @ ??{() -> ??} @ ??{?? -> ?? -> ??} @ []) (#(ident.list_case)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ (x2 : var (type.base A))(x3 : var (type.base (base.type.list A))), UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat) end))%under_lets | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x3) x2 => _ <- pattern.ident.invert_bind_args idc pattern.ident.cons; match s0 as t2 return (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) with | type.base t2 => fun v : defaults.expr (type.base t2) => match s as t3 return (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) with | type.base t3 => fun v0 : defaults.expr (type.base t3) => Compile.castbe v (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) (fun x4 : option (defaults.expr (type.base A)) => (x5 <- x4; Some (Compile.castbe v0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) (fun xs : option (defaults.expr (type.base (base.type.list A))) => (xs0 <- xs; Some (Some (fv <-- (e <-- x0 x5 xs0; UnderLets.Base {| anyexpr_ty := P; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) P (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base P)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.list_case) @ ??{() -> ??} @ ??{?? -> ?? -> ??} @ (?? :: ??)) (#(ident.list_case)%expr @ (λ x6 : var (type.base base.type.unit), UnderLets.to_expr (x ($x6)))%expr @ (λ (x6 : var (type.base A)) (x7 : var (type.base (base.type.list A))), UnderLets.to_expr (x0 ($x6) ($x7)))%expr @ x1)%expr_pat) end))%under_lets));;; None)));;; None) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x2) | (s1 -> d1)%ptype => fun _ : Compile.value' false s1 -> Compile.value' true d1 => None end (Compile.reflect x3) | @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);;; UnderLets.Base (#(ident.list_case)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ (λ (x2 : var (type.base A))(x3 : var (type.base (base.type.list A))), UnderLets.to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat)%option | @ident.List_length T => fun x : defaults.expr (type.base (base.type.list T)) => (reflect_list_cps x (fun xs : option (list (defaults.expr (type.base T))) => (xs0 <- xs; Some (Some (UnderLets.Base (##(length xs0))%expr)));;; None);;; UnderLets.Base (#(ident.List_length)%expr @ x)%expr_pat)%option | ident.List_seq => fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralNat; Some (UnderLets.Base (fold_right (fun (x1 : defaults.expr (type.base base.type.nat)) (xs : defaults.expr (type.base (base.type.list base.type.nat))) => (x1 :: xs)%expr_pat) []%expr_pat (map (fun v : nat => (##v)%expr) (seq args args0)))) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.List_seq)%expr @ x @ x0)%expr_pat)%option | @ident.List_firstn A => fun (x : defaults.expr (type.base base.type.nat)) (x0 : defaults.expr (type.base (base.type.list A))) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; reflect_list_cps x0 (fun xs : option (list (defaults.expr (type.base A))) => (xs0 <- xs; Some (Some (base.try_make_transport_cps A A (fun a : option (defaults.expr (type.base (base.type.list A)) -> defaults.expr (type.base (base.type.list A))) => match a with | Some x' => UnderLets.Base (x' (reify_list (firstn args xs0))) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_firstn) @ #(pattern.ident.LiteralNat) @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_firstn)%expr @ x @ x0)%expr_pat) end))));;; None) | _ => None end;; None);;; UnderLets.Base (#(ident.List_firstn)%expr @ x @ x0)%expr_pat)%option | @ident.List_skipn A => fun (x : defaults.expr (type.base base.type.nat)) (x0 : defaults.expr (type.base (base.type.list A))) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; reflect_list_cps x0 (fun xs : option (list (defaults.expr (type.base A))) => (xs0 <- xs; Some (Some (base.try_make_transport_cps A A (fun a : option (defaults.expr (type.base (base.type.list A)) -> defaults.expr (type.base (base.type.list A))) => match a with | Some x' => UnderLets.Base (x' (reify_list (skipn args xs0))) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_skipn) @ #(pattern.ident.LiteralNat) @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_skipn)%expr @ x @ x0)%expr_pat) end))));;; None) | _ => None end;; None);;; UnderLets.Base (#(ident.List_skipn)%expr @ x @ x0)%expr_pat)%option | @ident.List_repeat A => fun (x : defaults.expr (type.base A)) (x0 : defaults.expr (type.base base.type.nat)) => ((match x0 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Some (base.try_make_transport_cps A A (fun a : option (defaults.expr (type.base (base.type.list A)) -> defaults.expr (type.base (base.type.list A))) => match a with | Some x' => UnderLets.Base (x' (reify_list (repeat x args))) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_repeat) @ ?? @ #(pattern.ident.LiteralNat)) (#(ident.List_repeat)%expr @ x @ x0)%expr_pat) end)) | _ => None end;; None);;; UnderLets.Base (#(ident.List_repeat)%expr @ x @ x0)%expr_pat)%option | @ident.List_combine A B => fun (x : defaults.expr (type.base (base.type.list A))) (x0 : defaults.expr (type.base (base.type.list B))) => (reflect_list_cps x (fun xs : option (list (defaults.expr (type.base A))) => (xs0 <- xs; Some (reflect_list_cps x0 (fun ys : option (list (defaults.expr (type.base B))) => (ys0 <- ys; Some (Some ((trA <-- @base.try_make_transport_cps (fun A0 : base.type => defaults.expr (type.base (base.type.list (A0 * B)))) A A; trB <-- @base.try_make_transport_cps (fun B0 : base.type => defaults.expr (type.base (base.type.list (A * B0)))) B B; return Some (fun v : defaults.expr (type.base (base.type.list (A * B))) => trB (trA v)))%cps (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list (A * B))))) (fun a : option (defaults.expr (type.base (base.type.list (A * B))) -> defaults.expr (type.base (base.type.list (A * B)))) => match a with | Some x' => UnderLets.Base (x' (reify_list (map (fun '(x1, y) => (x1, y)%expr_pat) (combine xs0 ys0)))) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_combine) @ ??{type.base (pattern.base.type.list ??)} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_combine)%expr @ x @ x0)%expr_pat) end))));;; None)));;; None);;; UnderLets.Base (#(ident.List_combine)%expr @ x @ x0)%expr_pat)%option | @ident.List_map A B => fun (x : defaults.expr (type.base A) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base B))) (x0 : defaults.expr (type.base (base.type.list A))) => ((Compile.castbe x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B))))) (fun e : option (defaults.expr (type.base (base.type.list A))) => (e0 <- e; Some (reflect_list_cps e0 (fun ls : option (list (defaults.expr (type.base A))) => (ls0 <- ls; Some (Some (fv <-- (e1 <-- list_rect (fun _ : list (defaults.expr (type.base A)) => UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B)))) (UnderLets.Base []%expr_pat) (fun (x1 : defaults.expr (type.base A)) (_ : list (defaults.expr (type.base A))) (rec : UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B)))) => rec' <-- rec; fx <-- x x1; UnderLets.Base (fx :: rec')%expr_pat) ls0; UnderLets.Base {| anyexpr_ty := base.type.list B; unwrap := e1 |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) (base.type.list B) (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base (base.type.list B))) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_map) @ ??{?? -> ??} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_map)%expr @ (λ x1 : var (type.base A), UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat) end))%under_lets));;; None)));;; None);; None);;; UnderLets.Base (#(ident.List_map)%expr @ (λ x1 : var (type.base A), UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat)%option | @ident.List_app A => fun x x0 : defaults.expr (type.base (base.type.list A)) => ((Compile.castbe x (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list A))))) (fun e : option (defaults.expr (type.base (base.type.list A))) => (e0 <- e; Some (reflect_list_cps e0 (fun ls : option (list (defaults.expr (type.base A))) => (ls0 <- ls; Some (Some (fv <-- (e1 <-- list_rect (fun _ : list (defaults.expr (type.base A)) => UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list A)))) (UnderLets.Base x0) (fun (x1 : defaults.expr (type.base A)) (_ : list (defaults.expr (type.base A))) (rec : UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list A)))) => rec' <-- rec; UnderLets.Base (x1 :: rec')%expr_pat) ls0; UnderLets.Base {| anyexpr_ty := base.type.list A; unwrap := e1 |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) (base.type.list A) (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base (base.type.list A))) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (??{type.base (pattern.base.type.list ??)} ++ ??{type.base (pattern.base.type.list ??)}) (x ++ x0)) end))%under_lets));;; None)));;; None);; None);;; UnderLets.Base (x ++ x0)%expr)%option | @ident.List_rev A => fun x : defaults.expr (type.base (base.type.list A)) => ((reflect_list_cps x (fun xs : option (list (defaults.expr (type.base A))) => (xs0 <- xs; Some (Some (base.try_make_transport_cps A A (fun a : option (defaults.expr (type.base (base.type.list A)) -> defaults.expr (type.base (base.type.list A))) => match a with | Some x' => UnderLets.Base (x' (reify_list (rev xs0))) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_rev) @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_rev)%expr @ x)%expr_pat) end))));;; None);; None);;; UnderLets.Base (#(ident.List_rev)%expr @ x)%expr_pat)%option | @ident.List_flat_map A B => fun (x : defaults.expr (type.base A) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B)))) (x0 : defaults.expr (type.base (base.type.list A))) => ((Compile.castbe x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B))))) (fun e : option (defaults.expr (type.base (base.type.list A))) => (e0 <- e; Some (reflect_list_cps e0 (fun ls : option (list (defaults.expr (type.base A))) => (ls0 <- ls; Some (Some (fv <-- (e1 <-- list_rect (fun _ : list (defaults.expr (type.base A)) => UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B)))) (UnderLets.Base []%expr_pat) (fun (x1 : defaults.expr (type.base A)) (_ : list (defaults.expr (type.base A))) (rec : UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B)))) => rec' <-- rec; fx <-- x x1; UnderLets.Base ($fx ++ rec')%expr) ls0; UnderLets.Base {| anyexpr_ty := base.type.list B; unwrap := e1 |}); fv0 <-- do_again (let (anyexpr_ty, _) := fv in anyexpr_ty) (let (anyexpr_ty, unwrap) as a return (defaults.expr (type.base (let (anyexpr_ty, _) := a in anyexpr_ty))) := fv in unwrap); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) (base.type.list B) (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base (base.type.list B))) => match a with | Some x' => UnderLets.Base (x' fv0) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_flat_map) @ ??{?? -> type.base (pattern.base.type.list ??)} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_flat_map)%expr @ (λ x1 : var (type.base A), UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat) end))%under_lets));;; None)));;; None);; None);;; UnderLets.Base (#(ident.List_flat_map)%expr @ (λ x1 : var (type.base A), UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat)%option | @ident.List_partition A => fun (x : defaults.expr (type.base A) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.bool))) (x0 : defaults.expr (type.base (base.type.list A))) => ((Compile.castbe x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list A * base.type.list A)%etype)))) (fun e : option (defaults.expr (type.base (base.type.list A))) => (e0 <- e; Some (reflect_list_cps e0 (fun ls : option (list (defaults.expr (type.base A))) => (ls0 <- ls; Some (Some (fv <-- (e1 <-- list_rect (fun _ : list (defaults.expr (type.base A)) => UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list A * base.type.list A)%etype))) (UnderLets.Base ([], [])%expr_pat) (fun (x1 : defaults.expr (type.base A)) (_ : list (defaults.expr (type.base A))) (rec : UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list A * base.type.list A)%etype))) => rec' <-- rec; fx <-- id x x1; UnderLets.Base (#(ident.prod_rect)%expr @ (λ g d : defaults.expr (type.base (base.type.list A)), (#(ident.bool_rect)%expr @ (λ _ : defaults.expr (type.base base.type.unit), ($x1 :: $g, $d)%expr_pat) @ (λ _ : defaults.expr (type.base base.type.unit), ($g, $x1 :: $d)%expr_pat) @ $fx)%expr_pat)%expr @ rec')%expr_pat) ls0; UnderLets.Base {| anyexpr_ty := (base.type.list A * base.type.list A)%etype; unwrap := e1 |}); fv0 <-- do_again (let (anyexpr_ty, _) := fv in anyexpr_ty) (let (anyexpr_ty, unwrap) as a return (defaults.expr (type.base (let (anyexpr_ty, _) := a in anyexpr_ty))) := fv in unwrap); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) (base.type.list A * base.type.list A) (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base (base.type.list A * base.type.list A)%etype)) => match a with | Some x' => UnderLets.Base (x' fv0) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_partition) @ ??{?? -> type.base base.type.bool} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_partition)%expr @ (λ x1 : var (type.base A), UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat) end))%under_lets));;; None)));;; None);; None);;; UnderLets.Base (#(ident.List_partition)%expr @ (λ x1 : var (type.base A), UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat)%option | @ident.List_fold_right A B => fun (x : defaults.expr (type.base B) -> defaults.expr (type.base A) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base A))) (x0 : defaults.expr (type.base A)) (x1 : defaults.expr (type.base (base.type.list B))) => ((Compile.castv x (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) (fun f : option (defaults.expr (type.base B) -> defaults.expr (type.base A) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base A))) => (f0 <- f; Some (reflect_list_cps x1 (fun ls : option (list (defaults.expr (type.base B))) => (ls0 <- ls; Some (Some (fv <-- (e <-- list_rect (fun _ : list (defaults.expr (type.base B)) => UnderLets.UnderLets base.type ident var (defaults.expr (type.base A))) (UnderLets.Base x0) (fun (x2 : defaults.expr (type.base B)) (_ : list (defaults.expr (type.base B))) (rec : UnderLets.UnderLets base.type ident var (defaults.expr (type.base A))) => rec' <-- rec; f0 x2 rec') ls0; UnderLets.Base {| anyexpr_ty := A; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) A (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base A)) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_fold_right) @ ??{?? -> ?? -> ??} @ ?? @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_fold_right)%expr @ (λ (x2 : var (type.base B))(x3 : var (type.base A)), UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat) end))%under_lets));;; None)));;; None);; None);;; UnderLets.Base (#(ident.List_fold_right)%expr @ (λ (x2 : var (type.base B))(x3 : var (type.base A)), UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat)%option | @ident.List_update_nth T => fun (x : defaults.expr (type.base base.type.nat)) (x0 : defaults.expr (type.base T) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base T))) (x1 : defaults.expr (type.base (base.type.list T))) => (match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list T))))) (fun f : option (defaults.expr (type.base T) -> UnderLets.UnderLets base.type ident var (defaults.expr (type.base T))) => (f0 <- f; Some (reflect_list_cps x1 (fun ls : option (list (defaults.expr (type.base T))) => (ls0 <- ls; Some (Some (fv <-- (e <-- (retv <---- update_nth args (fun x2 : UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)) => x3 <-- x2; f0 x3) (map UnderLets.Base ls0); UnderLets.Base (reify_list retv)); UnderLets.Base {| anyexpr_ty := base.type.list T; unwrap := e |}); base.try_make_transport_cps (let (anyexpr_ty, _) := fv in anyexpr_ty) (base.type.list T) (fun a : option (defaults.expr (type.base (let (anyexpr_ty, _) := fv in anyexpr_ty)) -> defaults.expr (type.base (base.type.list T))) => match a with | Some x' => UnderLets.Base (x' (let (anyexpr_ty, unwrap) as a0 return (defaults.expr (type.base (let (anyexpr_ty, _) := a0 in anyexpr_ty))) := fv in unwrap)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_update_nth) @ #(pattern.ident.LiteralNat) @ ??{?? -> ??} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_update_nth)%expr @ x @ (λ x2 : var (type.base T), UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat) end))%under_lets));;; None)));;; None) | _ => None end;;; UnderLets.Base (#(ident.List_update_nth)%expr @ x @ (λ x2 : var (type.base T), UnderLets.to_expr (x0 ($x2)))%expr @ x1)%expr_pat)%option | @ident.List_nth_default T => fun (x : defaults.expr (type.base T)) (x0 : defaults.expr (type.base (base.type.list T))) (x1 : defaults.expr (type.base base.type.nat)) => ((match x1 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Compile.castbe x (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) (fun default : option (defaults.expr (type.base T)) => (default0 <- default; Some (reflect_list_cps x0 (fun ls : option (list (defaults.expr (type.base T))) => (ls0 <- ls; Some (Some (base.try_make_transport_cps T T (fun a : option (defaults.expr (type.base T) -> defaults.expr (type.base T)) => match a with | Some x' => UnderLets.Base (x' (nth_default default0 ls0 args)) | None => UnderLets.Base (Compile.ERROR_BAD_REWRITE_RULE (#(pattern.ident.List_nth_default) @ ?? @ ??{type.base (pattern.base.type.list ??)} @ #(pattern.ident.LiteralNat)) (#(ident.List_nth_default)%expr @ x @ x0 @ x1)%expr_pat) end))));;; None)));;; None) | _ => None end;; None);;; UnderLets.Base (#(ident.List_nth_default)%expr @ x @ x0 @ x1)%expr_pat)%option | ident.Z_add => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args + args0)%Z)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x + x0)%expr)%option | ident.Z_mul => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args * args0)%Z)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x * x0)%expr)%option | ident.Z_pow => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args ^ args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_pow)%expr @ x @ x0)%expr_pat)%option | ident.Z_sub => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args - args0)%Z)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x - x0)%expr)%option | ident.Z_opp => fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(- args)%Z)%expr) | _ => None end;; None);;; UnderLets.Base (- x)%expr)%option | ident.Z_div => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args / args0)%Z)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x / x0)%expr)%option | ident.Z_modulo => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args mod args0)%Z)%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x mod x0)%expr)%option | ident.Z_log2 => fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.log2 args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Z_log2)%expr @ x)%expr_pat)%option | ident.Z_log2_up => fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.log2_up args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Z_log2_up)%expr @ x)%expr_pat)%option | ident.Z_eqb => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args =? args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_eqb)%expr @ x @ x0)%expr_pat)%option | ident.Z_leb => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args <=? args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_leb)%expr @ x @ x0)%expr_pat)%option | ident.Z_geb => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(args >=? args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_geb)%expr @ x @ x0)%expr_pat)%option | ident.Z_of_nat => fun x : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Some (UnderLets.Base (##(Z.of_nat args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Z_of_nat)%expr @ x)%expr_pat)%option | ident.Z_to_nat => fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.to_nat args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Z_to_nat)%expr @ x)%expr_pat)%option | ident.Z_shiftr => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.shiftr args args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x >> x0)%expr)%option | ident.Z_shiftl => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.shiftl args args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x << x0)%expr)%option | ident.Z_land => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.land args args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x &' x0)%expr)%option | ident.Z_lor => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.lor args args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (x || x0)%expr)%option | ident.Z_bneg => fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.bneg args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Z_bneg)%expr @ x)%expr_pat)%option | ident.Z_lnot_modulo => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.lnot_modulo args args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_lnot_modulo)%expr @ x @ x0)%expr_pat)%option | ident.Z_mul_split => fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := Definitions.Z.mul_split args args0 args1 in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat)%option | ident.Z_add_get_carry => fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := Definitions.Z.add_get_carry_full args args0 args1 in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat)%option | ident.Z_add_with_carry => fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.add_with_carry args args0 args1))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat)%option | ident.Z_add_with_get_carry => fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := Definitions.Z.add_with_get_carry_full args args0 args1 args2 in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option | ident.Z_sub_get_borrow => fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := Definitions.Z.sub_get_borrow_full args args0 args1 in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat)%option | ident.Z_sub_with_get_borrow => fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := Definitions.Z.sub_with_get_borrow_full args args0 args1 args2 in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option | ident.Z_zselect => fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.zselect args args0 args1))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_zselect)%expr @ x @ x0 @ x1)%expr_pat)%option | ident.Z_add_modulo => fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.add_modulo args args0 args1))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat)%option | ident.Z_rshi => fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.rshi args args0 args1 args2))%expr) | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option | ident.Z_cc_m => fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.cc_m args args0))%expr) | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_cc_m)%expr @ x @ x0)%expr_pat)%option | ident.Z_cast range => fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.cast ident.cast_outside_of_range range args))%expr) | _ => None end;; None);;; UnderLets.Base (#(ident.Z_cast range)%expr @ x)%expr_pat)%option | ident.Z_cast2 range => fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := (let (r1, r2) := range in fun '(x2, x3) => (ident.cast ident.cast_outside_of_range r1 x2, ident.cast ident.cast_outside_of_range r2 x3)) (args0, args1) in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.Z_cast2 range)%expr @ x)%expr_pat)%option | ident.fancy_add log2wordmax imm => fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_add log2wordmax imm))) (args0, args1) in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_add log2wordmax imm)%expr @ x)%expr_pat)%option | ident.fancy_addc log2wordmax imm => fun x : defaults.expr (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_addc log2wordmax imm))) (args1, args2, args3) in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_addc log2wordmax imm)%expr @ x)%expr_pat)%option | ident.fancy_sub log2wordmax imm => fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_sub log2wordmax imm))) (args0, args1) in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_sub log2wordmax imm)%expr @ x)%expr_pat)%option | ident.fancy_subb log2wordmax imm => fun x : defaults.expr (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 pattern.ident.LiteralZ; Some (UnderLets.Base (let '(a, b) := ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_subb log2wordmax imm))) (args1, args2, args3) in ((##a)%expr, (##b)%expr)%expr_pat)) | _ => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_subb log2wordmax imm)%expr @ x)%expr_pat)%option | ident.fancy_mulll log2wordmax => fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_mulll log2wordmax))) (args0, args1)%core))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_mulll log2wordmax)%expr @ x)%expr_pat)%option | ident.fancy_mullh log2wordmax => fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_mullh log2wordmax))) (args0, args1)%core))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_mullh log2wordmax)%expr @ x)%expr_pat)%option | ident.fancy_mulhl log2wordmax => fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_mulhl log2wordmax))) (args0, args1)%core))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_mulhl log2wordmax)%expr @ x)%expr_pat)%option | ident.fancy_mulhh log2wordmax => fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_mulhh log2wordmax))) (args0, args1)%core))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_mulhh log2wordmax)%expr @ x)%expr_pat)%option | ident.fancy_rshi log2wordmax x => fun x0 : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x0 with | (@expr.Ident _ _ _ t idc @ x2 @ x1)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x2 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_rshi log2wordmax x))) (args0, args1)%core))%expr) | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_rshi log2wordmax x)%expr @ x0)%expr_pat)%option | ident.fancy_selc => fun x : defaults.expr (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy ident.fancy_selc)) (args1, args2, args3)%core))%expr) | _ => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_selc)%expr @ x)%expr_pat)%option | ident.fancy_selm log2wordmax => fun x : defaults.expr (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy (ident.fancy_selm log2wordmax))) (args1, args2, args3)%core))%expr) | _ => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_selm log2wordmax)%expr @ x)%expr_pat)%option | ident.fancy_sell => fun x : defaults.expr (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy ident.fancy_sell)) (args1, args2, args3)%core))%expr) | _ => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_sell)%expr @ x)%expr_pat)%option | ident.fancy_addm => fun x : defaults.expr (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp (invert_Some (ident.to_fancy ident.fancy_addm)) (args1, args2, args3)%core))%expr) | _ => None end | _ => None end | _ => None end | _ => None end | _ => None end;; None);;; UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat)%option end : Compile.value' true t