Year 2015 Day 14
This day provides us an introduction to streams, infinite, lazily generated, collections of data.
import Data.String
import Data.List1
import Data.Vect
import Data.Stream
import Data.Zippable
import Decidable.Equality
import Util
Parsing And Datastructures
Collect the aspects defining a reindeer into a record
record Reindeer where
constructor MkReindeer
name : String
speed : Nat
duration, rest : Nat
This time around, since the lines describing a reindeer contain a lot of cruft,
we'll handle the parsing by converting the input, after splitting it on space
characters, to a Vect, and indexing into that Vect.
parseReindeer : Has (Except String) fs =>
(input : String) -> Eff fs Reindeer
parseReindeer input = do
parts <- note "Input has wrong size: \{input}" $
toVect 15 . forget . split (== ' ') . trim $ input
let name = index 0 parts
speed <- note "" $
parsePositive $ index 3 parts
duration <- note "" $
parsePositive $ index 6 parts
rest <- note "" $
parsePositive $ index 13 parts
pure $ MkReindeer name speed duration rest
Solver Functions
A stream is an infinite analog of a list, storing an infinite collection of (lazily generated) values.
Streams are defined like:
data Stream' : Type -> Type where
(::) : a -> Inf (Stream' a) -> Stream' a
Streams are a member of a family of concepts analogous to iterators in imperative languages, the different flavors of colist.
Colists are the codata duals of lists, we'll dig more into to this later, but to
provide a high level summary, where data is defined by how it is constructed,
codata is defined by how it is destructed. While a list is defined by how you
can cons an element x onto a list xs to produce a new list x :: xs, a
colist is defined by how you can break down a colist x :: xs into a head x
and a tail xs.
Streams are a particular type of colist that has no empty case, breaking down a
Stream will always produce an element and another stream, resulting in streams
always being infinite in length.
Destructing a Stream by pattern matching is semantically equivalent to calling
the next method on an iterator in a language like rust, it produces the
element at the head of a stream, and a new stream producing future elements.
We will model are reindeer's future history of locations as a stream, with each
element being the position at the time given by the index into the stream,
generating it with a pair of mutually recursive functions. The run function
adds the speed to current position to produce the next one, and the rest
function doesn't modify the position whill still consuming a time step.
distances : Reindeer -> Stream Nat
distances x = run x x.duration 0
where
run : (deer : Reindeer) -> (left : Nat) -> (position : Nat)
-> Stream Nat
rest : (deer : Reindeer) -> (left : Nat) -> (position : Nat)
-> Stream Nat
run deer 0 position = rest deer deer.rest position
run deer (S k) position = position :: run deer k (position + deer.speed)
rest deer 0 position = run deer deer.duration position
rest deer (S k) position = position :: rest deer k position
Carry an accumulator containing the scores for each reindeer down the stream, at each position, granting one point to each reindeer at the leader position after the end of the second.
leaderScoring : {n : _} -> Vect (S n) (Stream Nat) -> Stream (Vect (S n) Nat)
leaderScoring xs = leaderScoring' (replicate _ 0) xs
where
leaderScoring' : {n : _} -> (acc : Vect (S n) Nat) -> Vect (S n) (Stream Nat)
-> Stream (Vect (S n) Nat)
leaderScoring' acc xs =
let positions = map (head . tail) xs
leader_pos = maxBy compare 0 positions
points : Vect _ Nat =
map (\x => if x == leader_pos then 1 else 0) positions
in acc :: leaderScoring' (zipWith (+) acc points) (map tail xs)
Part Functions
Part 1
Parse the input, generate the position Streams for each reindeer, then index
the finish position in each stream.
part1 : Eff (PartEff String) (Nat, ())
part1 = do
lines <- map lines $ askAt "input"
reindeer <- traverse parseReindeer lines
debug $ show reindeer
let dists = map distances reindeer
let dists_end = map (index 2503) dists
let max = maxBy compare 0 dists_end
pure (max, ())
Parse the input into a vect, and make sure it is not empty, then generate the
stream with the leaderScoring function and index into it.
part2 : () -> Eff (PartEff String) Nat
part2 x = do
lines <- map lines $ askAt "input"
let (len ** lines) = listToVect lines
case len of
0 => throw "No reindeer :("
(S k) => do
reindeer <- traverse parseReindeer lines
let dists = leaderScoring $ map distances reindeer
let dists_end = index 2503 dists
pure $ maxBy compare 0 dists_end