Year 2015 Day 7
This day provides us a gentle introduction to dependent maps.
Per the problem specification, each wire can only be output to by one gate. To
encode this property in the type, we'll tag Gate with the output wire in the
type, and then store our ciruct as a dependent map from wires to Gates. This
ensures that the circut only contains one gate outputting to each wire, and that
looking up a wire in the ciruct produces exactly the gate that outputs to it
through type checking.
Ensuring that the input contains only one gate outputting for each wire is done through throwing a runtime error in the parsing function if a second gate outputting to a given wire is found in the input.
import Data.Bits
import Data.Fin
import Data.String
import Data.List1
import Data.SortedMap
import Data.SortedMap.Dependent
import Decidable.Equality
Parsing and data structures
Problem structure
Define type aliases for wires and literals, and specify that an input can be either a literal or a wire.
Wire : Type
Wire = String
Literal : Type
Literal = Bits16
Input : Type
Input = Either Literal Wire
Description of a Gate, tagged in the type with the name of the output wire.
This creates what is referred to as an "indexed type family", in this case a
family of Gate types indexed by values of type Wire.
data Gate : Wire -> Type where
Constant : (x : Input) -> {output : Wire} -> Gate output
And : (x, y : Input) -> {output : Wire} -> Gate output
Or : (x, y : Input) -> {output : Wire} -> Gate output
Not : (x : Input) -> {output : Wire} -> Gate output
LShift : (x : Input) -> (y : Index {a = Literal}) -> {output : Wire}
-> Gate output
RShift : (x : Input) -> (y : Index {a = Literal}) -> {output : Wire}
-> Gate output
Parsing functions
Parse a shift value, making sure its bounded properly to index a Bits16
parseShift : Has (Except String) fs => String -> Eff fs (Index {a = Literal})
parseShift str =
note "Invalid shift: \{str}" $ parsePositive str
Make sure that this string consists only of lowercase letters
parseWire : Has (Except String) fs => String -> Eff fs Wire
parseWire str =
if all isLower (unpack str)
then pure str
else throw "Invalid wire \{str}"
Parse either a wire or a literal
parseInput : Has (Except String) fs => String -> Eff fs Input
parseInput str =
case parsePositive str of
Nothing => map Right . parseWire $ str
Just x => pure $ Left x
Split the string into components and pattern match on them to extract a gate
parseGate : Has (Except String) fs => Has Logger fs =>
String -> Eff fs (wire : Wire ** Gate wire)
parseGate str = do
debug "Parsing gate: \{str}"
case split (== ' ') str of
x ::: ["->", output ] => do
x <- parseInput x
output <- parseWire output
pure (output ** Constant x)
"NOT" ::: [x, "->", output] => do
x <- parseInput x
output <- parseWire output
pure (output ** Not x)
x ::: ["AND", y, "->", output] => do
x <- parseInput x
y <- parseInput y
output <- parseWire output
pure (output ** And x y)
x ::: ["OR", y, "->", output] => do
x <- parseInput x
y <- parseInput y
output <- parseWire output
pure (output ** Or x y)
x ::: ["RSHIFT", y, "->", output] => do
x <- parseInput x
y <- parseShift y
output <- parseWire output
pure (output ** RShift x y)
x ::: ["LSHIFT", y, "->", output] => do
x <- parseInput x
y <- parseShift y
output <- parseWire output
pure (output ** LShift x y)
_ => throw "Invalid Gate: \{str}"
Break the input into lines, traverse parseGate over the lines, and collect the
results into our circut DMap.
The type of a value in a SortedDMap depends on the value of the key that
refers to it, in the type constructor SortedDMap k v, v is of type
k -> Type, this is the function the map calls to calculate the type of the
value from the value of the key. This, not so coincidentally, is the type
signature of our Gate type constructor, which we can slot in here to get a map
from a wire to the gate outputting to that wire, preventing us from accidentally
associating a wire to the wrong gate.
parseGates : Has (Except String) fs => Has Logger fs =>
String -> Eff fs (SortedDMap Wire Gate)
parseGates input = do
gates : List (wire : Wire ** Gate wire) <-
traverse parseGate . lines . trim $ input
foldlM insertGate empty gates
where
insertGate : SortedDMap Wire Gate -> (wire : Wire ** Gate wire)
-> Eff fs $ SortedDMap Wire Gate
insertGate map (wire ** gate) =
if isJust $ lookup wire map
then throw "Duplicate gate for \{wire}"
else pure $ insert wire gate map
Solver Functions
Recursively solve for the value on a wire, keeping a cache of already solved wires
covering
solveWire : Has (Except String) fs => Has (State (SortedMap Wire Literal)) fs =>
Has (Reader (SortedDMap Wire Gate)) fs =>
(wire : Wire) -> Eff fs Literal
solveWire wire = do
-- Short circut if we are already in the cache
Nothing <- map (lookup wire) get
| Just cached => pure cached
-- Find the gate that outputs to this wire in our circut
Just gate <- map (lookupPrecise wire) ask
| _ => throw "No output for wire \{wire}"
-- Recursively solve for the inputs and apply this gate's operation
res : Literal <- case gate of
Constant x => fromInput x
And x y => do
x <- fromInput x
y <- fromInput y
pure $ x .&. y
Or x y => do
x <- fromInput x
y <- fromInput y
pure $ x .|. y
Not x => do
x <- fromInput x
pure $ complement x
LShift x y => do
x <- fromInput x
pure $ x `shiftL` y
RShift x y => do
x <- fromInput x
pure $ x `shiftR` y
-- Add this gate's output to the cache
modify $ insert wire res
pure res
where
fromInput : (i : Input) -> Eff fs Literal
fromInput (Left x) = pure x
fromInput (Right x) = solveWire x
Part Functions
Part 1
Parse the input, then feed it and an initial empty cache into our solveWire
function, passing the produced value as the output and the circut, represented
as a dependent map from wires to gates, as well as the output signal from wire
'a' as the context for part 2.
covering
part1 : Eff (PartEff String) (Bits16, (SortedDMap Wire Gate, Literal))
part1 = do
circut <- askAt "input" >>= parseGates
(value, _) <-
runState empty . runReader circut $ solveWire "a"
{fs = State (SortedMap Wire Literal)
:: Reader (SortedDMap Wire Gate)
:: PartEff String }
pure (value, (circut, value))
Part 2
Override the value for the 'b' wire to the output from the 'a' wire in part 1, then rerun our calcuation to find the new output for the 'a' wire.
covering
part2 : (SortedDMap Wire Gate, Literal) -> Eff (PartEff String) Bits16
part2 (circut, value) = do
let circut = insert "b" (Constant (Left value)) circut
(value, _) <-
runState empty . runReader circut $ solveWire "a"
{fs = State (SortedMap Wire Literal)
:: Reader (SortedDMap Wire Gate)
:: PartEff String }
pure value