aoc2023/day9.tooslow.quox

89 lines
2.8 KiB
Text
Raw Permalink Normal View History

2023-12-12 14:37:05 -05:00
load "bool.quox"
load "list.quox"
load "maybe.quox"
load "int.quox"
def zz = int.zero
def step : ω.(List ) → List =
λ xs ⇒
list.zip-with-uneven (λ m n ⇒ int.minus n m)
xs (list.tail-or-nil xs)
def all-zero : ω.(List ) → Bool =
list.foldlω Bool 'true (λ b n ⇒ bool.and b (int.eq n zz))
def last : 0.(A : ★) → ω.(List A) → Maybe A =
λ A ⇒ list.foldrω A (Maybe A) (Nothing A) (λ x y ⇒ maybe.or A y (Just A x))
def0 last-ok : last (4, 1, 4, 8, 5, 'nil) ≡ Just 5 : Maybe =
δ 𝑖 ⇒ Just 5
def last-or-0 : ω.(List ) → =
λ xs ⇒ maybe.fold zz (λ x ⇒ x) (last xs)
{-
def next-entries : ω.(List ) → List =
λ xs ⇒
letω fuel = fst xs in
caseω fuel return ω.(List ) → List of {
0 ⇒ λ _ ⇒ list.Nil ;
succ _, ω.rec ⇒ λ this ⇒
bool.if (List ) (all-zero this) (list.Nil )
(letω next : List = step this in
letω rest : List = rec next in
letω new : = nat.plus (last-or-0 this) (head-or-0 rest) in
list.Cons new rest)
} xs
-}
def next-entry : ω.(List ) → =
λ xs ⇒
letω fuel = fst xs in
letω xs = list.map int.from- xs in
let result : =
caseω fuel return ω.(List ) → of {
0 ⇒ λ _ ⇒ zz;
succ _, ω.rec ⇒ λ this ⇒
bool.if (all-zero this) zz
(letω next : List = step this in
letω diff : = rec next in
int.plus diff (last-or-0 this))
} xs in
int.abs result
def0 ok-1 : next-entry (6, 0, 3, 6, 9, 12, 15, 'nil) ≡ 18 : = δ _ ⇒ 18
def0 ok-2 : next-entry (6, 1, 3, 6, 10, 15, 21, 'nil) ≡ 28 : = δ _ ⇒ 28
def0 ok-3 : next-entry (6, 10, 13, 16, 21, 30, 45, 'nil) ≡ 68 : = δ _ ⇒ 68
load "io.quox"
load "string.quox"
def read-file : ω.String → IO [ω.List (List )] =
λ path ⇒
letω split-lines : ω.String → List String =
string.split (λ c ⇒ char.eq c char.newline);
split-numbers : ω.String → List = λ str ⇒
let words = string.split char.ws? str in
list.map String string.to--or-0 words;
split-file : ω.String → [ω. List (List )] = λ str ⇒
[list.mapω String (List ) split-numbers (split-lines str)] in
io.mapω String [ω.List (List )] split-file (io.read-fileω path)
def FILE : String = "in/day9"
-- #[main]
def doot =
io.bindω (List (List )) True
(read-file FILE)
(λ lists ⇒ io.dump (List (List )) lists)
#[main]
def part1 =
io.bindω (List (List )) True
(read-file FILE)
(λ lists ⇒ io.dump (list.sum (list.mapω (List ) next-entry lists)))