94 lines
2.5 KiB
Plaintext
94 lines
2.5 KiB
Plaintext
load "list.quox"
|
||
load "nat.quox"
|
||
load "io.quox"
|
||
|
||
postulate0 Char : ★
|
||
|
||
namespace char {
|
||
#[compile-scheme "char->integer"]
|
||
postulate ord : Char → ℕ
|
||
|
||
#[compile-scheme "integer->char"]
|
||
postulate chr : ℕ → Char
|
||
|
||
#[compile-scheme "(lambda (c) (cons c 'erased))"]
|
||
postulate dup! : (c : Char) → [ω.Sing Char c]
|
||
|
||
def dup : Char → [ω.Char] =
|
||
λ c ⇒ appω (Sing Char c) Char (λ c' ⇒ sing.val Char c c') (dup! c);
|
||
|
||
def le : ω.Char → ω.Char → Bool =
|
||
λ x y ⇒ nat.le (ord x) (ord y)
|
||
|
||
def between : ω.Char → ω.Char → ω.Char → Bool =
|
||
λ lo hi c ⇒
|
||
case dup c return Bool of { [c] ⇒ bool.and (le lo c) (le c hi) }
|
||
|
||
def is-digit : ω.Char → Bool =
|
||
between (chr 0x30) (chr 0x39)
|
||
|
||
def digit : Char → ℕ =
|
||
λ c ⇒ nat.minus (ord c) 0x30
|
||
|
||
#[compile-scheme "(lambda (c) (builtin-io (display c) (newline)))"]
|
||
postulate println : Char → IO True
|
||
}
|
||
|
||
namespace string {
|
||
#[compile-scheme "string->list"]
|
||
postulate prim-to-list : String → list.SchemeList Char
|
||
|
||
def to-list : String → List Char =
|
||
λ str ⇒ list.from-scheme Char (prim-to-list str)
|
||
|
||
#[compile-scheme "(lambda (str) str)"]
|
||
postulate dup : String → [ω.String]
|
||
}
|
||
|
||
|
||
|
||
def find-first-last :
|
||
0.(A : ★) →
|
||
ω.(ω.A → Bool) →
|
||
ω.(List A) → Maybe (A × A) =
|
||
λ A p xs ⇒
|
||
maybe.pair A A
|
||
(list.find A p xs)
|
||
(list.find A p (list.reverse A xs))
|
||
|
||
def for-io : 0.(A : ★) → ω.(A → IO True) → List A → IO True =
|
||
λ A f xs ⇒ list.foldr A (IO True) io.pass (λ x act ⇒ io.seq' (f x) act) xs
|
||
|
||
def find-in-string : ω.(ω.Char → Bool) → ω.String → Maybe Char =
|
||
λ p str ⇒ list.find Char p (string.to-list str)
|
||
|
||
def number' : Char → Char → ℕ =
|
||
λ tens units ⇒ nat.plus (nat.times 10 (char.digit tens)) (char.digit units)
|
||
|
||
def number : String → ℕ =
|
||
λ line ⇒
|
||
case string.dup line return ℕ of {
|
||
[line] ⇒
|
||
maybe.fold (Char × Char) ℕ 0
|
||
(pair.uncurry' Char Char ℕ number')
|
||
(find-first-last Char char.is-digit (string.to-list line))
|
||
}
|
||
|
||
def part1 : List String → ℕ =
|
||
list.foldr String ℕ 0 (λ str n ⇒ nat.plus (number str) n)
|
||
|
||
namespace nat {
|
||
#[compile-scheme "(lambda (n) (builtin-io (display n) (newline)))"]
|
||
postulate println : ℕ → IO True
|
||
}
|
||
|
||
#[compile-scheme "(lambda (x) (builtin-io (display x) (newline)))"]
|
||
postulate dump : 0.(A : ★) → A → IO True
|
||
|
||
|
||
#[main]
|
||
def main : IO True =
|
||
io.bind (List String) True
|
||
(io.read-file-lines "in/day1")
|
||
(λ lines ⇒ dump ℕ (part1 lines))
|