From 22eccd177cf430827652d6e98b77851d4147efd1 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Tue, 28 Jan 2025 11:38:11 -0500 Subject: [PATCH] Year 2015 Day 13 Part 1 --- README.md | 6 + src/SUMMARY.md | 1 + src/Years/Y2015.md | 7 ++ src/Years/Y2015/Day13.md | 241 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 255 insertions(+) create mode 100644 src/Years/Y2015/Day13.md diff --git a/README.md b/README.md index 731d675..763edcc 100644 --- a/README.md +++ b/README.md @@ -132,7 +132,13 @@ solution. New Parser Effect stack and DLists + - [Day 13](src/Years/Y2015/Day13.md) + + Naive ring buffer and `parameters` blocks[^2] + ## References [^1]: Idris 2 Manual: [Views and the "with" rule](https://idris2.readthedocs.io/en/latest/tutorial/views.html#views-and-the-with-rule) + +[^2]: diff --git a/src/SUMMARY.md b/src/SUMMARY.md index f0b09eb..9447a3a 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -34,3 +34,4 @@ - [Day 10 - Digits View](Years/Y2015/Day10.md) - [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) diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 8f94f4f..79ae4e8 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -19,6 +19,7 @@ import Years.Y2015.Day9 import Years.Y2015.Day10 import Years.Y2015.Day11 import Years.Y2015.Day12 +import Years.Y2015.Day13 ``` # Days @@ -101,6 +102,12 @@ y2015 = MkYear 2015 [ , day12 ``` +## [Day 13](Y2015/Day13.md) + +```idris + , day13 +``` + ```idris ] ``` diff --git a/src/Years/Y2015/Day13.md b/src/Years/Y2015/Day13.md new file mode 100644 index 0000000..a344473 --- /dev/null +++ b/src/Years/Y2015/Day13.md @@ -0,0 +1,241 @@ +# [Year 2015 Day 13](https://adventofcode.com/2015/day/13) + +This day exhibits a naive, `Vect` based implementation of a ring buffer, as well +as our first introduction to `parameters` blocks. + +```idris hide +module Years.Y2015.Day13 + +import Data.Primitives.Interpolation + +import Control.Eff + +import Runner +``` + +```idris +import Data.String +import Data.List1 +import Data.List.Lazy +import Data.Vect +import Data.Maybe +import Data.SortedMap.Dependent +import Decidable.Equality + +import Util + +%default total +``` + +## Parsing and Data Structures + +```idris +Name : Type +Name = String + +Happiness : Type +Happiness = Integer +``` + +Describe a change in happiness from a change in seating arrangement as data +structure, indexed by the name of the individual whose happiness it describes, +and provide some projections. + +```idris +data Change : (changee : Name) -> Type where + NextTo : (changee : Name) -> (other : Name) -> (amount : Happiness) + -> Change (changee) + +(.changee) : Change changee -> Name +(.changee) (NextTo changee _ _) = changee + +(.other) : Change changee -> Name +(.other) (NextTo _ other _) = other + +(.amount) : Change changee -> Happiness +(.amount) (NextTo _ _ amount) = amount +``` + +Collect the list of changes provided as input into a structure that encodes our +assumptions at the type level. + +The changes are stored in a in a dependent map, with the name of the individual +as the key, and lists of potential changes to their happiness as the values. + +This problem is a bit nicer to express in terms of a collection of known size, +and we don't want to be constantly converting the keys list to a `Vect`, so we +instead store it in `Changes` as a `Vect`. We don't want to accidentally store +the wrong thing here, so we store an auto-implicit proof of equality, +`keys_prf`, proving that the `names` list is exactly the list of keys in +`change_map` converted to a Vect with `fromList`. + +It will also make things a bit nicer if we can assume that our `names` list is +non-empty, after all it really doesn't make sense to talk about seating +arrangements at a table with 0 people at it, so we store an auto-implict +`nonempty` proof establishing that the length of `change_map`'s keys list, and +thus `names`, is at least 1. + +```idris +record Changes where + constructor MkChanges + change_map : SortedDMap Name (\n => List (Change n)) + names : Vect (length (keys change_map)) Name + {auto keys_prf : names = fromList (keys change_map)} + {auto nonempty : IsSucc (length (keys change_map))} +``` + +Our usual pattern-matching based parsing of one element of the input, returning +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 str = do + changee ::: [_, direction, amount, _, _, _, _, _, _, other] + <- pure $ split (== ' ') str + | _ => throw "Invalid input string \{str}" + amount <- note "Invalid amount \{amount} in \{str}" $ parseInteger amount + amount : Happiness <- + case direction of + "gain" => pure amount + "lose" => pure $ negate amount + x => throw "Invalid direction \{x} in \{str}" + let other = pack . filter (/= '.') . unpack $ other + pure (_ ** (changee `NextTo` other) amount) +``` + +Parse the entire list of changes in the input, collecting them into a dependent +map as we go along, and performing the checks needed for Idris to be satisfied +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 + changes <- traverse parseChange strs + let change_map = insertChanges changes empty + 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" + where + insertChanges : List (name ** Change name) + -> (acc : SortedDMap Name (\n => List (Change n))) + -> SortedDMap Name (\n => List (Change n)) + insertChanges [] acc = acc + insertChanges ((name ** change) :: xs) acc = + case lookupPrecise name acc of + Nothing => insertChanges xs (insert name [change] acc) + Just ys => insertChanges xs (insert name (change :: ys) acc) +``` + +## Solver functions + +All of these functions are about to take the same first argument, +`(cs : Changes)`. This is a really common occurrence, especially when dealing +with dependent proof types, so Idris has syntax sugar to avoid repeating your +self in theses situations, `parameters` blocks[^1]. + +A `parameters` block adds the provided arguments to the start of every top level +signature contained within it, in this case, making the first argument of all of +these functions have type `(cs : Changes)`. The arguments to the `parameters` +blocks are also added to the front of the arguments list, using the names +provided in the signature. + +`parameters` blocks also provide another fun bit of functionality that makes +code within them more concise, within a `parameters` block, the parameters are +implicitly passed as arguments to calls to functions in the same block. + +```idris +parameters (cs : Changes) +``` + +Calculate the happiness change for a given person in a seating arrangement, use +`finS` and `unfinS` to get the indexes of the parties seated to either side of +us, and look them up in our map, adding the amount of change described by them +together. + +Notice how `cs` appears neither in the arguments list, nor the type signature, +yet we can still refer to it as if it was included at the start of both. + +```idris + happinessFor : + (arrangement : Vect (length (keys cs.change_map)) Name) + -> (idx : Fin (length (keys cs.change_map))) + -> Happiness + happinessFor arrangement idx = + let name = idx `index` arrangement + in case name `lookupPrecise` cs.change_map of + Nothing => 0 + Just changes => + let name_right = (finS idx) `index` arrangement + change_right = + fromMaybe 0 . map (.amount) . find ((== name_right) . (.other)) $ + changes + name_left = (unfinS idx) `index` arrangement + change_left = + fromMaybe 0 . map (.amount) . find ((== name_left) . (.other)) $ + changes + in change_right + change_left +``` + +Calculate the overall happiness change for a given arrangement by mapping our +`happinessFor` function over a list of all possible indexes to the `arrangement` +vect, and summing the results. + +Notice how the `cs` parameter is implicitly passed to `happinessFor`, as we are +inside the same `parameters` block as it. + +```idris + happinessChange : + (arrangement : Vect (length (keys cs.change_map)) Name) + -> Happiness + happinessChange arrangement = + let idxes = List.allFins (length (keys cs.change_map)) + changes = map (happinessFor arrangement) idxes + in sum changes +``` + +Find the arrangement with the maximum total change in happiness by mapping +`happinessChange` over a list of all the possible permutations of our seed +arrangement described by `names`, and using `maxBy` to identify the largest +positive change in overall happiness. + +```idris + maxHappiness : Has (Except String) fs => + Eff fs (Happiness, Vect (length (keys cs.change_map)) Name) + maxHappiness = + let arrangements = permutations cs.names + changes = map happinessChange arrangements + pairs = zip changes arrangements + in case pairs of + [] => throw "No arrangements" + (x :: xs) => pure $ maxBy (compare `on` fst) x xs +``` + +## Part Functions + +### Part 1 + +Parse our input and feed it into our `maxHappiness` function. + +Notice how, since we are outside the `parameters` block, we have to provide the +`cs` argument to `maxHappiness` explicitly. + +```idris +part1 : Eff (PartEff String) (Happiness, ()) +part1 = do + input <- map lines $ askAt "input" + changes <- parseChanges input + (max, arrangement) <- maxHappiness changes + pure (max, ()) +``` + +```idris hide +public export +day13 : Day +day13 = First 13 part1 +``` + +## References + +[^1]: