Year 2015 Day 14 Part 2

src/Years/Y2015/Day14.md

@@ -18,6 +18,7 @@ import Data.String
 import Data.List1
 import Data.Vect
 import Data.Stream
+import Data.Zippable
 import Decidable.Equality
 
 import Util
@@ -111,6 +112,24 @@ distances x = run x x.duration 0
     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
@@ -121,7 +140,7 @@ the finish position in each stream.
 ```idris
 part1 : Eff (PartEff String) (Nat, ())
 part1 = do
-  lines <- map (lines) $ askAt "input"
+  lines <- map lines $ askAt "input"
   reindeer <- traverse parseReindeer lines
   debug $ show reindeer
   let dists = map distances reindeer
@@ -130,8 +149,25 @@ part1 = do
   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 = First 14 part1
+day14 = Both 14 part1 part2
 ```