Year 2015 Day 13
This day exhibits a naive, Vect based implementation of a ring buffer, as well
as our first introduction to parameters blocks.
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
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.
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.
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.
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.
parseChanges : Has (Except String) fs =>
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 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"
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 blocks1.
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.
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.
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.
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.
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.
part1 : Eff (PartEff String) (Happiness, ())
part1 = do
input <- map lines $ askAt "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.
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