Year 2015 Day 13 Part 2

This commit is contained in:
Nathan McCarty 2025-01-29 03:32:22 -05:00
parent 22eccd177c
commit f8d6e3cfcb

View file

@ -89,7 +89,8 @@ a dependent pair of the name of the individual this record describes, and the
change described by that record. change described by that record.
```idris ```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 parseChange str = do
changee ::: [_, direction, amount, _, _, _, _, _, _, other] changee ::: [_, direction, amount, _, _, _, _, _, _, other]
<- pure $ split (== ' ') str <- pure $ split (== ' ') str
@ -110,10 +111,11 @@ that the conditions encoded by the auto-implict proofs in `Changes` are met.
```idris ```idris
parseChanges : Has (Except String) fs => parseChanges : Has (Except String) fs =>
List String -> Eff fs Changes List String -> (seed : SortedDMap Name (\n => List (Change n)))
parseChanges strs = do -> Eff fs Changes
parseChanges strs seed = do
changes <- traverse parseChange strs changes <- traverse parseChange strs
let change_map = insertChanges changes empty let change_map = insertChanges changes seed
case isItSucc (length (keys change_map)) of case isItSucc (length (keys change_map)) of
Yes prf => pure $ MkChanges change_map (fromList (keys change_map)) Yes prf => pure $ MkChanges change_map (fromList (keys change_map))
No contra => throw "Empty table, not very interesting" 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 : Eff (PartEff String) (Happiness, ())
part1 = do part1 = do
input <- map lines $ askAt "input" input <- map lines $ askAt "input"
changes <- parseChanges input changes <- parseChanges input empty
(max, arrangement) <- maxHappiness changes (max, arrangement) <- maxHappiness changes
pure (max, ()) 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 ```idris hide
public export public export
day13 : Day day13 : Day
day13 = First 13 part1 day13 = Both 13 part1 part2
``` ```
## References ## References