aoc2023/lib/list.quox
2023-12-01 18:52:23 +01:00

163 lines
5.2 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

load "nat.quox";
load "maybe.quox";
load "bool.quox";
namespace vec {
def0 Vec : → ★ → ★ =
λ n A ⇒
caseω n return ★ of {
zero ⇒ {nil};
succ _, 0.Tail ⇒ A × Tail
};
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)
}
};
-- haha gross
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)
}
};
#[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)
}
}
}
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 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) → 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
};
-- [fixme] List A <: List¹ A should be automatic, imo
#[compile-scheme "(lambda (xs) xs)"]
def up : 0.(A : ★) → List A → List¹ A =
λ A xs ⇒
case xs return List¹ A of { (len, elems) ⇒
case nat.dup! len return List¹ A of { [p] ⇒
caseω p return List¹ A of { (lenω, eq0) ⇒
case eq0 return List¹ A of { [eq] ⇒
(lenω, vec.up A lenω (coe (𝑖 ⇒ Vec (eq @𝑖) A) @1 @0 elems))
}
}
}
};
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));
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 (list)
(let loop [(acc '()) (list (cdr list))]
(if (pair? list)
(loop (cons (car list) acc) (cdr list))
(reverse acc))))"]
postulate to-scheme : 0.(A : ★) → List A → SchemeList A
}
def0 List = list.List;