Year 2015 Day 14 Part 2

README.md

@@ -136,6 +136,10 @@ solution.
 
     Naive ring buffer and `parameters` blocks[^2]
 
+  - [Day 14](src/Years/Y2015/Day14.md)
+
+    Introduction to streams, infinite collections of data
+
 ## References
 
 [^1]: Idris 2 Manual:

advent.ipkg

@@ -41,7 +41,7 @@ main = Main
 
 -- name of executable
 executable = "advent"
--- opts =
+opts = "--directive lazy=weakMemo"
 sourcedir = "src"
 -- builddir =
 -- outputdir =

src/SUMMARY.md

@@ -35,3 +35,4 @@
   - [Day 11 - Refinement Types](Years/Y2015/Day11.md)
   - [Day 12 - Custom Parser Effect and DLists](Years/Y2015/Day12.md)
   - [Day 13 - Naive Ring Buffer and parameters blocks](Years/Y2015/Day13.md)
+  - [Day 14 - Introduction to Streams](Years/Y2015/Day14.md)

src/Util.md

@@ -192,6 +192,14 @@ Lazily generate all the permutations of a Vect
   maxBy f (x :: xs) = Foldable.maxBy f x xs
 ```
 
+### Convert a list to a vect as a sigma type
+
+```idris
+  export
+  listToVect : List a -> (n : Nat ** Vect n a)
+  listToVect xs = (length xs ** fromList xs)
+```
+
 ## Fin
 
 ```idris hide

src/Years/Y2015.md

@@ -20,6 +20,7 @@ import Years.Y2015.Day10
 import Years.Y2015.Day11
 import Years.Y2015.Day12
 import Years.Y2015.Day13
+import Years.Y2015.Day14
 ```
 
 # Days
@@ -108,6 +109,12 @@ y2015 = MkYear 2015 [
   , day13
 ```
 
+## [Day 14](Y2015/Day14.md)
+
+```idris
+  , day14
+```
+
 ```idris
   ]
 ```

src/Years/Y2015/Day14.md

@@ -0,0 +1,173 @@
+# [Year 2015 Day 14](https://adventofcode.com/2015/day/14)
+
+This day provides us an introduction to streams, infinite, lazily generated,
+collections of data.
+
+```idris hide
+module Years.Y2015.Day14
+
+import Data.Primitives.Interpolation
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+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
+
+```idris
+record Reindeer where
+  constructor MkReindeer
+  name : String
+  speed : Nat
+  duration, rest : Nat
+```
+
+```idris hide
+Show Reindeer where
+  show (MkReindeer name speed duration rest) = 
+    "MkReindeer \{name} \{speed} \{duration} \{rest}"
+```
+
+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`.
+
+```idris
+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:
+
+```idris
+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.
+
+```idris
+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.
+
+```idris
+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 `Stream`s for each reindeer, then index
+the finish position in each stream.
+
+```idris
+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.
+
+```idris
+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
+```
+
+```idris hide
+public export
+day14 : Day 
+day14 = Both 14 part1 part2
+```