load "misc.quox"
load "nat.quox"
load "maybe.quox"
load "bool.quox"
load "qty.quox"

namespace vec {

def0 Vec : ℕ → ★ → ★ =
  λ n A ⇒
  caseω n return ★ of {
    zero           ⇒ {nil};
    succ _, 0.Tail ⇒ A × Tail
  }

def drop-nil-dep : 0.(A : ★) → 0.(P : Vec 0 A → ★) →
                   (xs : Vec 0 A) → P 'nil → P xs =
  λ A P xs p ⇒ case xs return xs' ⇒ P xs' of { 'nil ⇒ p }

def drop-nil : 0.(A B : ★) → Vec 0 A → B → B =
  λ A B ⇒ drop-nil-dep A (λ _ ⇒ B)

def match-dep :
    0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
    ω.(P 0 'nil) →
    ω.((n : ℕ) → (x : A) → (xs : Vec n A) → P (succ n) (x, xs)) →
    (n : ℕ) → (xs : Vec n A) → P n xs =
  λ A P pn pc n ⇒
    case n return n' ⇒ (xs : Vec n' A) → P n' xs of {
      0 ⇒ λ nil ⇒ drop-nil-dep A (P 0) nil pn;
      succ len ⇒ λ cons ⇒
        case cons return cons' ⇒ P (succ len) cons' of {
          (first, rest) ⇒ pc len first rest
        }
    }

def match-depω :
    0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
    ω.(P 0 'nil) →
    ω.(ω.(n : ℕ) → ω.(x : A) → ω.(xs : Vec n A) → P (succ n) (x, xs)) →
    ω.(n : ℕ) → ω.(xs : Vec n A) → P n xs =
  λ A P pn pc n ⇒
    caseω n return n' ⇒ ω.(xs : Vec n' A) → P n' xs of {
      0 ⇒ λ nil ⇒ drop-nil-dep A (P 0) nil pn;
      succ len ⇒ λ cons ⇒
        caseω cons return cons' ⇒ P (succ len) cons' of {
          (first, rest) ⇒ pc len first rest
        }
    }
def match-dep# = match-depω

def elim : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
           P 0 'nil →
           ω.((x : A) → 0.(n : ℕ) → 0.(xs : Vec n A) →
              P n xs → P (succ n) (x, xs)) →
           (n : ℕ) → (xs : Vec n A) → P n xs =
  λ A P pn pc n ⇒
    case n return n' ⇒ (xs' : Vec n' A) → P n' xs' of {
      zero ⇒ λ nil ⇒
        case nil return nil' ⇒ P 0 nil' of { 'nil ⇒ pn };
      succ n, IH ⇒ λ cons ⇒
        case cons return cons' ⇒ P (succ n) cons' of {
          (first, rest) ⇒ pc first n rest (IH rest)
        }
    }

def elim2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★) →
            P 0 'nil 'nil →
            ω.((x : A) → (y : B) → 0.(n : ℕ) →
               0.(xs : Vec n A) → 0.(ys : Vec n B) →
               P n xs ys → P (succ n) (x, xs) (y, ys)) →
            (n : ℕ) → (xs : Vec n A) → (ys : Vec n B) → P n xs ys =
  λ A B P pn pc n ⇒
    case n return n' ⇒ (xs : Vec n' A) → (ys : Vec n' B) → P n' xs ys of {
      zero ⇒ λ nila nilb ⇒
        drop-nil-dep A (λ n ⇒ P 0 n nilb) nila
          (drop-nil-dep B (λ n ⇒ P 0 'nil n) nilb pn);
      succ n, IH ⇒ λ consa consb ⇒
        case consa return consa' ⇒ P (succ n) consa' consb of { (a, as) ⇒
          case consb return consb' ⇒ P (succ n) (a, as) consb' of { (b, bs) ⇒
            pc a b n as bs (IH as bs)
          }
        }
    }

def elim2-uneven :
    0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →
    -- both nil
    ω.(P 0 0 'nil 'nil) →
    -- first nil
    ω.((y : B) → 0.(n : ℕ) → 0.(ys : Vec n B) →
       P 0 n 'nil ys → P 0 (succ n) 'nil (y, ys)) →
    -- second nil
    ω.((x : A) → 0.(m : ℕ) → 0.(xs : Vec m A) →
       P m 0 xs 'nil → P (succ m) 0 (x, xs) 'nil) →
    -- both cons
    ω.((x : A) → (y : B) → 0.(m n : ℕ) →
       0.(xs : Vec m A) → 0.(ys : Vec n B) →
       P m n xs ys → P (succ m) (succ n) (x, xs) (y, ys)) →
    (m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) → P m n xs ys =
  λ A B P pnn pnc pcn pcc ⇒
    nat.elim-pair (λ m n ⇒ (xs : Vec m A) → (ys : Vec n B) → P m n xs ys)
      (λ xnil ynil ⇒
        let0 Ret = P 0 0 'nil 'nil in
        drop-nil A Ret xnil (drop-nil B Ret ynil pnn))
      (λ n IH xnil yys ⇒
        case yys return yys' ⇒ P 0 (succ n) 'nil yys' of { (y, ys) ⇒
          pnc y n ys (IH xnil ys)
        })
      (λ m IH xxs ynil ⇒
        case xxs return xxs' ⇒ P (succ m) 0 xxs' 'nil of { (x, xs) ⇒
          pcn x m xs (IH xs ynil)
        })
      (λ m n IH xxs yys ⇒
        case xxs return xxs' ⇒ P (succ m) (succ n) xxs'    yys  of { (x, xs) ⇒
        case yys return yys' ⇒ P (succ m) (succ n) (x, xs) yys' of { (y, ys) ⇒
          pcc x y m n xs ys (IH xs ys)
        }})

-- haha gross
def elimω : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
            ω.(P 0 'nil) →
            ω.(ω.(x : A) → ω.(n : ℕ) → ω.(xs : Vec n A) →
               ω.(P n xs) → P (succ n) (x, xs)) →
            ω.(n : ℕ) → ω.(xs : Vec n A) → P n xs =
  λ A P pn pc n ⇒
    caseω n return n' ⇒ ω.(xs' : Vec n' A) → P n' xs' of {
      zero         ⇒ λ _ ⇒ pn;
      succ n, ω.IH ⇒ λ xxs ⇒
        letω x = fst xxs; xs = snd xxs in pc x n xs (IH xs)
    }

def elimω2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★) →
             ω.(P 0 'nil 'nil) →
             ω.(ω.(x : A) → ω.(y : B) → ω.(n : ℕ) →
                ω.(xs : Vec n A) → ω.(ys : Vec n B) →
                ω.(P n xs ys) → P (succ n) (x, xs) (y, ys)) →
             ω.(n : ℕ) → ω.(xs : Vec n A) → ω.(ys : Vec n B) → P n xs ys =
  λ A B P pn pc n ⇒
    caseω n return n' ⇒ ω.(xs : Vec n' A) → ω.(ys : Vec n' B) → P n' xs ys of {
      zero         ⇒ λ _ _ ⇒ pn;
      succ n, ω.IH ⇒ λ xxs yys ⇒
        letω x = fst xxs; xs = snd xxs; y = fst yys; ys = snd yys in
        pc x y n xs ys (IH xs ys)
    }

{-
postulate elimP :
    ω.(π : NzQty) → ω.(ρₙ ρₗ : Qty) →
    0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
    FunNz π (P 0 'nil)
    (Fun 'any
        (FUN-NZ π A (λ x ⇒ FUN ρₙ ℕ (λ n ⇒ FUN ρₗ (Vec n A) (λ xs ⇒
            FunNz π (P n xs) (P (succ n) (x, xs))))))
    (FUN-NZ π ℕ (λ n ⇒ FUN-NZ π (Vec n A) (λ xs ⇒ P n xs))))
{-
  =
  λ π ρₙ ρₗ A P ⇒ uhhhhhhhhhhhhhhhhhhh
-}
-}

def elimω2-uneven :
    0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →
    -- both nil
    ω.(P 0 0 'nil 'nil) →
    -- first nil
    ω.(ω.(y : B) → ω.(n : ℕ) → ω.(ys : Vec n B) →
       ω.(P 0 n 'nil ys) → P 0 (succ n) 'nil (y, ys)) →
    -- second nil
    ω.(ω.(x : A) → ω.(m : ℕ) → ω.(xs : Vec m A) →
       ω.(P m 0 xs 'nil) → P (succ m) 0 (x, xs) 'nil) →
    -- both cons
    ω.(ω.(x : A) → ω.(y : B) → ω.(m n : ℕ) →
       ω.(xs : Vec m A) → ω.(ys : Vec n B) →
       ω.(P m n xs ys) → P (succ m) (succ n) (x, xs) (y, ys)) →
    ω.(m n : ℕ) → ω.(xs : Vec m A) → ω.(ys : Vec n B) → P m n xs ys =
  λ A B P pnn pnc pcn pcc ⇒
    nat.elim-pairω (λ m n ⇒ ω.(xs : Vec m A) → ω.(ys : Vec n B) → P m n xs ys)
      (λ _ _ ⇒ pnn)
      (λ n IH xnil yys ⇒
        letω y = fst yys; ys = snd yys in pnc y n ys (IH xnil ys))
      (λ m IH xxs ynil ⇒
        letω x = fst xxs; xs = snd xxs in pcn x m xs (IH xs ynil))
      (λ m n IH xxs yys ⇒
        letω x = fst xxs; xs = snd xxs; y = fst yys; ys = snd yys in
        pcc x y m n xs ys (IH xs ys))

def zip-with : 0.(A B C : ★) → ω.(A → B → C) →
               (n : ℕ) → Vec n A → Vec n B → Vec n C =
  λ A B C f ⇒
    elim2 A B (λ n _ _ ⇒ Vec n C) 'nil (λ a b _ _ _ abs ⇒ (f a b, abs))

def zip-withω : 0.(A B C : ★) → ω.(ω.A → ω.B → C) →
                ω.(n : ℕ) → ω.(Vec n A) → ω.(Vec n B) → Vec n C =
  λ A B C f ⇒
    elimω2 A B (λ n _ _ ⇒ Vec n C) 'nil (λ a b _ _ _ abs ⇒ (f a b, abs))


namespace zip-with {
  def0 Failure : (A B : ★) → (m n : ℕ) → Vec m A → Vec n B → ★ =
    λ A B m n xs ys ⇒
    Sing (Vec m A) xs × Sing (Vec n B) ys × [0. Not (m ≡ n : ℕ)]

  def0 Success : (C : ★) → (m n : ℕ) → ★ =
    λ C m n ⇒ Vec n C × [0. m ≡ n : ℕ]

  def0 Result : (A B C : ★) → (m n : ℕ) → Vec m A → Vec n B → ★ =
    λ A B C m n xs ys ⇒
    Either (Failure A B m n xs ys) (Success C m n)

  def zip-with-hetω : 0.(A B C : ★) → ω.(A → B → C) →
                      ω.(m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) →
                      Result A B C m n xs ys =
    λ A B C f m n xs ys ⇒
      let0 TNo  : Vec m A → Vec n B → ★ = Failure A B m n;
           TYes : ★ = Success C m n;
           TRes : Vec m A → Vec n B → ★ = λ xs ys ⇒ Either (TNo xs ys) TYes in
      dec.elim (m ≡ n : ℕ)
        (λ _ ⇒ (xs : Vec m A) → (ys : Vec n B) → TRes xs ys)
        (λ eq xs ys ⇒
          let zs : Vec n C =
            zip-with A B C f n (coe (𝑖 ⇒ Vec (eq @𝑖) A) xs) ys in
          Right (TNo xs ys) TYes (zs, [eq]))
        (λ neq xs ys ⇒ Left (TNo xs ys) TYes
          (sing (Vec m A) xs, sing (Vec n B) ys, [neq]))
        (nat.eq? m n) xs ys

  def zip-with-het : 0.(A B C : ★) → ω.(A → B → C) →
                     (m n : ℕ) → (xs : Vec m A) → (ys : Vec n B) →
                     Result A B C m n xs ys =
    λ A B C f m n ⇒
      let0 Ret : ℕ → ℕ → ★ =
             λ m n ⇒ (xs : Vec m A) → (ys : Vec n B) → Result A B C m n xs ys in
      dup.elim ℕ m (λ m' ⇒ Ret m' n)
        (λ m ⇒ dup.elim ℕ n (λ n' ⇒ Ret m n')
          (λ n ⇒ zip-with-hetω A B C f m n) (nat.dup! n))
        (nat.dup! m)
}
def0 ZipWith = zip-with.Result
def zip-with-het = zip-with.zip-with-het
def zip-with-hetω = zip-with.zip-with-hetω

#[compile-scheme "(lambda% (n xs) xs)"]
def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A =
  λ A n ⇒
    case n return n' ⇒ Vec n' A → Vec¹ n' A of {
      zero ⇒ λ xs ⇒
        case xs return Vec¹ 0 A of { 'nil ⇒ 'nil };
      succ n', f' ⇒ λ xs ⇒
        case xs return Vec¹ (succ n') A of {
          (first, rest) ⇒ (first, f' rest)
        }
    }

def append : 0.(A : ★) → (m : ℕ) → 0.(n : ℕ) →
             Vec m A → Vec n A → Vec (nat.plus m n) A =
  λ A m n xs ys ⇒
    elim A (λ m _ ⇒ Vec (nat.plus m n) A) ys (λ x _ _ xsys ⇒ (x, xsys)) m xs

}

def0 Vec = vec.Vec


namespace list {

def0 List : ★ → ★ =
  λ A ⇒ (len : ℕ) × Vec len A

def Nil : 0.(A : ★) → List A =
  λ A ⇒ (0, 'nil)

def Cons : 0.(A : ★) → A → List A → List A =
  λ A x xs ⇒ case xs return List A of { (len, elems) ⇒ (succ len, x, elems) }

def single : 0.(A : ★) → A → List A =
  λ A x ⇒ Cons A x (Nil A)

def elim : 0.(A : ★) → 0.(P : List A → ★) →
           P (Nil A) →
           ω.((x : A) → 0.(xs : List A) → P xs → P (Cons A x xs)) →
           (xs : List A) → P xs =
  λ A P pn pc xs ⇒
    case xs return xs' ⇒ P xs' of { (len, elems) ⇒
      vec.elim A (λ n xs ⇒ P (n, xs))
        pn (λ x n xs IH ⇒ pc x (n, xs) IH)
        len elems
    }

def elimω : 0.(A : ★) → 0.(P : List A → ★) →
            ω.(P (Nil A)) →
            ω.(ω.(x : A) → ω.(xs : List A) → ω.(P xs) → P (Cons A x xs)) →
            ω.(xs : List A) → P xs =
  λ A P pn pc xs ⇒
    caseω xs return xs' ⇒ P xs' of { (len, elems) ⇒
      vec.elimω A (λ n xs ⇒ P (n, xs))
        pn (λ x n xs IH ⇒ pc x (n, xs) IH)
        len elems
    }

def elim2 : 0.(A B : ★) → 0.(P : List A → List B → ★) →
            ω.(P (Nil A) (Nil B)) →
            ω.((y : B) → 0.(ys : List B) →
               P (Nil A) ys → P (Nil A) (Cons B y ys)) →
            ω.((x : A) → 0.(xs : List A) →
               P xs (Nil B) → P (Cons A x xs) (Nil B)) →
            ω.((x : A) → 0.(xs : List A) → (y : B) → 0.(ys : List B) →
               P xs ys → P (Cons A x xs) (Cons B y ys)) →
            (xs : List A) → (ys : List B) → P xs ys =
  λ A B P pnn pnc pcn pcc xs ys ⇒
    case xs return xs' ⇒ P xs'     ys  of { (m, xs) ⇒
    case ys return ys' ⇒ P (m, xs) ys' of { (n, ys) ⇒
      vec.elim2-uneven A B (λ m n xs ys ⇒ P (m, xs) (n, ys))
        pnn
        (λ y n ys IH ⇒ pnc y (n, ys) IH)
        (λ x m xs IH ⇒ pcn x (m, xs) IH)
        (λ x y m n xs ys IH ⇒ pcc x (m, xs) y (n, ys) IH)
        m n xs ys
    }}

def elimω2 : 0.(A B : ★) → 0.(P : List A → List B → ★) →
             ω.(P (Nil A) (Nil B)) →
             ω.(ω.(y : B) → ω.(ys : List B) →
                ω.(P (Nil A) ys) → P (Nil A) (Cons B y ys)) →
             ω.(ω.(x : A) → ω.(xs : List A) →
                ω.(P xs (Nil B)) → P (Cons A x xs) (Nil B)) →
             ω.(ω.(x : A) → ω.(xs : List A) → ω.(y : B) → ω.(ys : List B) →
                ω.(P xs ys) → P (Cons A x xs) (Cons B y ys)) →
             ω.(xs : List A) → ω.(ys : List B) → P xs ys =
  λ A B P pnn pnc pcn pcc xs ys ⇒
    caseω xs return xs' ⇒ P xs'     ys  of { (m, xs) ⇒
    caseω ys return ys' ⇒ P (m, xs) ys' of { (n, ys) ⇒
      vec.elimω2-uneven A B (λ m n xs ys ⇒ P (m, xs) (n, ys))
        pnn
        (λ y n ys IH ⇒ pnc y (n, ys) IH)
        (λ x m xs IH ⇒ pcn x (m, xs) IH)
        (λ x y m n xs ys IH ⇒ pcc x (m, xs) y (n, ys) IH)
        m n xs ys
    }}

def as-vec : 0.(A : ★) → 0.(P : List A → ★) → (xs : List A) →
             (ω.(n : ℕ) → (xs : Vec n A) → P (n, xs)) → P xs =
  λ A P xs f ⇒
    case xs return xs' ⇒ P xs' of { (n, xs) ⇒
      dup.elim ℕ n (λ n' ⇒ (xs : Vec n' A) → P (n', xs)) f (nat.dup! n) xs
    }

def match-dep :
    0.(A : ★) → 0.(P : List A → ★) →
    ω.(P (Nil A)) → ω.((x : A) → (xs : List A) → P (Cons A x xs)) →
    (xs : List A) → P xs =
  λ A P pn pc xs ⇒
    case xs return xs' ⇒ P xs' of {
      (len, elems) ⇒
        vec.match-dep A (λ n xs ⇒ P (n, xs)) pn (λ n x xs ⇒ pc x (n, xs))
          len elems
    }

def match-depω :
    0.(A : ★) → 0.(P : List A → ★) →
    ω.(P (Nil A)) →
    ω.(ω.(x : A) → ω.(xs : List A) → P (Cons A x xs)) →
    ω.(xs : List A) → P xs =
  λ A P pn pc xs ⇒
    vec.match-depω A (λ n xs ⇒ P (n, xs)) pn (λ n x xs ⇒ pc x (n, xs))
                   (fst xs) (snd xs)
def match-dep# = match-depω

def match : 0.(A B : ★) → ω.B → ω.(A → List A → B) → List A → B =
  λ A B ⇒ match-dep A (λ _ ⇒ B)

def matchω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.(List A) → B) → ω.(List A) → B =
  λ A B ⇒ match-depω A (λ _ ⇒ B)
def match# = matchω


def up : 0.(A : ★) → List A → List¹ A =
  λ A xs ⇒
  case xs return List¹ A of { (len, elems) ⇒
    dup.elim'¹ ℕ len (λ _ ⇒ List¹ A)
      (λ len eq ⇒ (len, vec.up A len (coe (𝑖 ⇒ Vec (eq @𝑖) A) @1 @0 elems)))
      (nat.dup! len)
  }

def foldr : 0.(A B : ★) → B → ω.(A → B → B) → List A → B =
  λ A B z f xs ⇒ elim A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs

def foldl : 0.(A B : ★) → B → ω.(B → A → B) → List A → B =
  λ A B z f xs ⇒
    foldr A (B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z

def map : 0.(A B : ★) → ω.(A → B) → List A → List B =
  λ A B f ⇒ foldr A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys)


-- ugh
def foldrω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.B → B) → ω.(List A) → B =
  λ A B z f xs ⇒ elimω A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs

def foldlω : 0.(A B : ★) → ω.B → ω.(ω.B → ω.A → B) → ω.(List A) → B =
  λ A B z f xs ⇒
    foldrω A (ω.B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z

def mapω : 0.(A B : ★) → ω.(ω.A → B) → ω.(List A) → List B =
  λ A B f ⇒ foldrω A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys)


def0 All : (A : ★) → (P : A → ★) → List A → ★ =
  λ A P xs ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps) (up A xs)

def append : 0.(A : ★) → List A → List A → List A =
  λ A xs ys ⇒ foldr A (List A) ys (Cons A) xs

def reverse : 0.(A : ★) → List A → List A =
  λ A ⇒ foldl A (List A) (Nil A) (λ xs x ⇒ Cons A x xs)


def find : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → Maybe A =
  λ A p ⇒
    foldlω A (Maybe A) (Nothing A) (λ m x ⇒ maybe.or A m (maybe.check A p x))

def cons-first : 0.(A : ★) → ω.A → List (List A) → List (List A) =
  λ A x ⇒
    match (List A) (List (List A))
      (single (List A) (single A x))
      (λ xs xss ⇒ Cons (List A) (Cons A x xs) xss)

def split : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List (List A) =
  λ A p ⇒
    foldrω A (List (List A))
      (Nil (List A))
      (λ x xss ⇒ bool.if (List (List A)) (p x)
          (Cons (List A) (Nil A) xss)
          (cons-first A x xss))

def break : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List A × List A =
  λ A p xs ⇒
  let0 Lst = List A; Lst2 = (Lst × Lst) ∷ ★; State = Either Lst Lst2 in
  letω LeftS = Left Lst Lst2; RightS = Right Lst Lst2 in
  letω res =
    foldlω A State
      (LeftS (Nil A))
      (λ acc x ⇒
        either.foldω Lst Lst2 State
          (λ xs ⇒ bool.if State (p x)
            (RightS (xs, list.single A x))
            (LeftS  (Cons A x xs)))
          (λ xsys ⇒
            RightS (fst xsys, Cons A x (snd xsys))) acc)
      xs ∷ State in
  letω res =
    either.fold Lst Lst2 Lst2 (λ xs ⇒ (Nil A, xs)) (λ xsys ⇒ xsys) res in
  (reverse A (fst res), reverse A (snd res))

def uncons : 0.(A : ★) → List A → Maybe (A × List A) =
  λ A ⇒
    match A (Maybe (A × List A))
      (Nothing (A × List A))
      (λ x xs ⇒ Just (A × List A) (x, xs))

def head : 0.(A : ★) → ω.(List A) → Maybe A =
  λ A ⇒ matchω A (Maybe A) (Nothing A) (λ x _ ⇒ Just A x)

def tail : 0.(A : ★) → ω.(List A) → Maybe (List A) =
  λ A ⇒ matchω A (Maybe (List A)) (Nothing (List A)) (λ _ xs ⇒ Just (List A) xs)

def tail-or-nil : 0.(A : ★) → ω.(List A) → List A =
  λ A ⇒ matchω A (List A) (Nil A) (λ _ xs ⇒ xs)

-- slip (xs, [])      = (xs, [])
-- slip (xs, y :: ys) = (y :: xs, ys)
def slip : 0.(A : ★) → List A × List A → List A × List A =
  λ A xsys ⇒
    case xsys return List A × List A of { (xs, ys) ⇒
      match A (List A → List A × List A)
        (λ      xs ⇒ (xs, Nil A))
        (λ y ys xs ⇒ (Cons A y xs, ys))
        ys xs
    }

def split-at' : 0.(A : ★) → ℕ → List A → List A × List A =
  λ A n xs ⇒
    (case n return List A × List A → List A × List A of {
      0         ⇒ λ xsys ⇒ xsys;
      succ _, f ⇒ λ xsys ⇒ f (slip A xsys)
    }) (Nil A, xs)

def split-at : 0.(A : ★) → ℕ → List A → List A × List A =
  λ A n xs ⇒
    case split-at' A n xs return List A × List A of {
      (xs', ys) ⇒ (reverse A xs', ys)
    }

def filter : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → List A =
  λ A p ⇒
    foldrω A (List A)
      (Nil A)
      (λ x xs ⇒ bool.if (List A) (p x) (Cons A x xs) xs)

def length : 0.(A : ★) → ω.(List A) → ℕ =
  λ A xs ⇒ fst xs


namespace zip-with {
  def0 VFailure = vec.zip-with.Failure
  def0 VSuccess = vec.zip-with.Success

  def0 Failure : (A B : ★) → List A → List B → ★ =
    λ A B xs ys ⇒ VFailure A B (fst xs) (fst ys) (snd xs) (snd ys)

  def0 Result : (A B C : ★) → List A → List B → ★ =
    λ A B C xs ys ⇒ Either (Failure A B xs ys) (List C)

  def zip-with : 0.(A B C : ★) → ω.(A → B → C) →
                 (xs : List A) → (ys : List B) →
                 Result A B C xs ys =
    λ A B C f xs ys ⇒
    let0 Ret = Result A B C in
    as-vec A (λ xs' ⇒ Ret xs'     ys)  xs (λ m xs ⇒
    as-vec B (λ ys' ⇒ Ret (m, xs) ys') ys (λ n ys ⇒
    let0 Err = Failure A B (m, xs) (n, ys) in
    either.fold Err (VSuccess C m n) (Ret (m, xs) (n, ys))
      (λ no ⇒ Left Err (List C) no)
      (λ yes ⇒ case yes return Ret (m, xs) (n, ys) of { (vec, prf) ⇒
        Right Err (List C) (drop0 (m ≡ n : ℕ) (List C) prf (n, vec))
      })
      (vec.zip-with-hetω A B C f m n xs ys)))
}
def0 ZipWith = zip-with.Result
def zip-with = zip-with.zip-with

def zip-withω : 0.(A B C : ★) → ω.(ω.A → ω.B → C) →
                ω.(xs : List A) → ω.(ys : List B) →
                Either [0. Not (fst xs ≡ fst ys : ℕ)] (List C) =
  λ A B C f xs ys ⇒
    letω m = fst xs; xs = snd xs;
         n = fst ys; ys = snd ys in
    let0 Err : ★ = [0. Not (m ≡ n : ℕ)] in
    dec.elim (m ≡ n : ℕ) (λ _ ⇒ Either Err (List C))
      (λ mn ⇒
        letω xs = coe (𝑖 ⇒ Vec (mn @𝑖) A) xs in
        Right Err (List C) (n, vec.zip-withω A B C f n xs ys))
      (λ nmn ⇒ Left Err (List C) [nmn])
      (nat.eq? m n)
def zip-with# = zip-withω


def zip-with-uneven :
    0.(A B C : ★) → ω.(ω.A → ω.B → C) → ω.(List A) → ω.(List B) → List C =
  λ A B C f xs ys ⇒
    caseω nat.min (fst xs) (fst ys)
    return ω.(List A) → ω.(List B) → List C of {
      0             ⇒ λ _ _ ⇒ Nil C;
      succ _, ω.fih ⇒ λ xs ys ⇒
        maybe.foldω (A × List A) (List C) (Nil C)
          (λ xxs ⇒ maybe.foldω (B × List B) (List C) (Nil C)
            (λ yys ⇒ Cons C (f (fst xxs) (fst yys)) (fih (snd xxs) (snd yys)))
            (list.uncons B ys))
          (list.uncons A xs)
    } xs ys


def sum     : List ℕ → ℕ = foldl ℕ ℕ 0 nat.plus
def product : List ℕ → ℕ = foldl ℕ ℕ 1 nat.times


namespace mergesort {
  def deal : 0.(A : ★) → List A → List A × List A =
    λ A ⇒
    let0 One = List A; Pair : ★ = One × One in
    foldl A Pair (Nil A, Nil A)
      (pair.uncurry' One One (A → Pair) (λ ys zs x ⇒ (Cons A x zs, ys)))

}


postulate0 SchemeList : ★ → ★

#[compile-scheme
  "(lambda (list) (cons (length list) (fold-right cons 'nil list)))"]
postulate from-scheme : 0.(A : ★) → SchemeList A → List A

#[compile-scheme
 "(lambda (lst)
    (do [(lst (cdr lst) (cdr lst))
         (acc '()       (cons (car lst) acc))]
      [(equal? lst 'nil) (reverse acc)]))"]
postulate to-scheme : 0.(A : ★) → List A → SchemeList A

}

def0 List = list.List