diff --git a/src/Years/Y2015/Day14.md b/src/Years/Y2015/Day14.md index 3de7430..5418617 100644 --- a/src/Years/Y2015/Day14.md +++ b/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 ```