114 lines
3.3 KiB
Plaintext
114 lines
3.3 KiB
Plaintext
load "string.quox"
|
||
load "io.quox"
|
||
|
||
|
||
namespace real {
|
||
postulate0 ℝ : ★
|
||
|
||
#[compile-scheme "inexact"]
|
||
postulate to-ℝ : ℕ → ℝ
|
||
|
||
#[compile-scheme "sqrt"]
|
||
postulate sqrt : ℝ → ℝ
|
||
|
||
#[compile-scheme "(lambda (x) (exact (floor x)))"]
|
||
postulate floor : ℝ → ℕ
|
||
|
||
#[compile-scheme "(lambda (x) (exact (ceiling x)))"]
|
||
postulate ceiling : ℝ → ℕ
|
||
|
||
#[compile-scheme "(lambda% (x y) (+ x y))"]
|
||
postulate plus : ℝ → ℝ → ℝ
|
||
|
||
#[compile-scheme "(lambda% (x y) (- x y))"]
|
||
postulate minus : ℝ → ℝ → ℝ
|
||
|
||
#[compile-scheme "(lambda% (x y) (* x y))"]
|
||
postulate times : ℝ → ℝ → ℝ
|
||
|
||
#[compile-scheme "(lambda% (x y) (/ x y))"]
|
||
postulate divide : ℝ → ℝ → ℝ
|
||
|
||
#[compile-scheme "(lambda% (x y) (if (< x y) 'true 'false))"]
|
||
postulate lt : ω.ℝ → ω.ℝ → Bool
|
||
|
||
def negate : ℝ → ℝ = λ x ⇒ minus (to-ℝ 0) x
|
||
|
||
def quad : ω.ℝ → ω.ℝ → ω.ℝ → ℝ × ℝ =
|
||
λ a b c ⇒
|
||
letω res =
|
||
(λ op ⇒
|
||
let disc = minus (times b b) (times (to-ℝ 4) (times a c)) in
|
||
divide (op (negate b) (sqrt disc)) (times (to-ℝ 2) a))
|
||
∷ (ℝ → ℝ → ℝ) → ℝ in
|
||
letω ordered =
|
||
(λ x y ⇒ bool.if (ℝ × ℝ) (lt x y) (x, y) (y, x)) ∷ ω.ℝ → ω.ℝ → ℝ × ℝ in
|
||
ordered (res plus) (res minus)
|
||
}
|
||
|
||
def0 ℝ = real.ℝ
|
||
def to-ℝ = real.to-ℝ
|
||
|
||
|
||
def range : ω.ℕ → ω.ℕ → ℕ × ℕ =
|
||
λ t d ⇒
|
||
letω d = to-ℝ d; t = to-ℝ t;
|
||
res = real.quad (real.negate (to-ℝ 1)) t (real.negate d);
|
||
lo = fst res; hi = snd res
|
||
in (real.ceiling lo, real.floor hi)
|
||
|
||
def result : ω.(ℕ × ℕ) → ℕ =
|
||
λ td ⇒ letω r = range (fst td) (snd td) in succ (nat.minus (snd r) (fst r))
|
||
|
||
|
||
def0 Game : ★ = ℕ × ℕ
|
||
|
||
def to-ℕ' : String → ℕ =
|
||
λ s ⇒ maybe.fold ℕ ℕ 0 (λ n ⇒ n) (string.to-ℕ s)
|
||
|
||
def split-line : ω.String → List ℕ =
|
||
λ l ⇒
|
||
letω strings = string.split char.ws? l;
|
||
strings = list.filter String string.not-null strings;
|
||
strings = list.tail-or-nil String strings in
|
||
list.map String ℕ to-ℕ' strings
|
||
|
||
def split-file : ω.String → List Game =
|
||
λ str ⇒
|
||
letω both = string.break (λ c ⇒ char.eq c char.newline) str;
|
||
one = fst both; two = snd both;
|
||
times = split-line one; distances = split-line two in
|
||
list.zip-with-uneven ℕ ℕ Game (λ t d ⇒ (t, d)) times distances
|
||
|
||
|
||
def space? : ω.Char → Bool = λ c ⇒ char.eq c char.space
|
||
|
||
def squash : ω.String → String =
|
||
λ s ⇒
|
||
letω nonws? = (λ c ⇒ bool.not (char.ws? c)) ∷ ω.Char → Bool in
|
||
string.from-list (list.filter Char nonws? (string.to-list s))
|
||
|
||
def from-line : ω.String → ℕ =
|
||
λ s ⇒ letω s = snd (string.break space? s) in to-ℕ' (squash s)
|
||
|
||
def nonsplit-file : ω.String → Game =
|
||
λ str ⇒
|
||
letω both = string.break (λ c ⇒ char.eq c char.newline) str;
|
||
one = fst both; two = snd both in
|
||
(from-line one, from-line two)
|
||
|
||
|
||
def product : List ℕ → ℕ = list.foldl ℕ ℕ 1 nat.times
|
||
|
||
|
||
def part1 =
|
||
io.bindω String True
|
||
(io.read-fileω "in/day6")
|
||
(λ s ⇒ io.dump ℕ (product (list.mapω Game ℕ result (split-file s))))
|
||
|
||
#[main]
|
||
def part2 =
|
||
io.bindω String True
|
||
(io.read-fileω "in/day6")
|
||
(λ s ⇒ io.dump ℕ (result (nonsplit-file s)))
|