From f8d6e3cfcbe6904496ff1034d63efab3accd9317 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Wed, 29 Jan 2025 03:32:22 -0500 Subject: [PATCH] Year 2015 Day 13 Part 2 --- src/Years/Y2015/Day13.md | 34 ++++++++++++++++++++++++++++------ 1 file changed, 28 insertions(+), 6 deletions(-) diff --git a/src/Years/Y2015/Day13.md b/src/Years/Y2015/Day13.md index a344473..e0f7f89 100644 --- a/src/Years/Y2015/Day13.md +++ b/src/Years/Y2015/Day13.md @@ -89,7 +89,8 @@ a dependent pair of the name of the individual this record describes, and the change described by that record. ```idris -parseChange : Has (Except String) fs => String -> Eff fs (name ** Change name) +parseChange : Has (Except String) fs => + String -> Eff fs (name ** Change name) parseChange str = do changee ::: [_, direction, amount, _, _, _, _, _, _, other] <- pure $ split (== ' ') str @@ -110,10 +111,11 @@ that the conditions encoded by the auto-implict proofs in `Changes` are met. ```idris parseChanges : Has (Except String) fs => - List String -> Eff fs Changes -parseChanges strs = do + List String -> (seed : SortedDMap Name (\n => List (Change n))) + -> Eff fs Changes +parseChanges strs seed = do changes <- traverse parseChange strs - let change_map = insertChanges changes empty + let change_map = insertChanges changes seed case isItSucc (length (keys change_map)) of Yes prf => pure $ MkChanges change_map (fromList (keys change_map)) No contra => throw "Empty table, not very interesting" @@ -225,15 +227,35 @@ Notice how, since we are outside the `parameters` block, we have to provide the part1 : Eff (PartEff String) (Happiness, ()) part1 = do input <- map lines $ askAt "input" - changes <- parseChanges input + changes <- parseChanges input empty (max, arrangement) <- maxHappiness changes pure (max, ()) ``` +### Part 2 + +Our implementation already replaces missing relationships with 0, so we can +cheese this by injecting ourself with an empty relationship list into the +`change_map : SortedDMap Name (\n => (List n))`. + +The overall `Changes` data structure isn't easy to modify, and since our data +set is quite small here, we'll just inject this into parsing and reparse our +data. + +```idris +part2 : () -> Eff (PartEff String) Happiness +part2 x = do + input <- map lines $ askAt "input" + let seed = insert "ME!!!!" [] empty + changes <- parseChanges input seed + (max, arrangement) <- maxHappiness changes + pure max +``` + ```idris hide public export day13 : Day -day13 = First 13 part1 +day13 = Both 13 part1 part2 ``` ## References