259 lines
7.5 KiB
Markdown
259 lines
7.5 KiB
Markdown
# [Year 2015 Day 7](https://adventofcode.com/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 `Gate`s. 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.
|
|
|
|
```idris hide
|
|
module Years.Y2015.Day7
|
|
|
|
import Control.Eff
|
|
|
|
import Runner
|
|
```
|
|
|
|
```idris
|
|
import Data.Bits
|
|
import Data.Fin
|
|
import Data.String
|
|
import Data.List1
|
|
import Data.SortedMap
|
|
import Data.SortedMap.Dependent
|
|
import Decidable.Equality
|
|
```
|
|
|
|
```idris hide
|
|
%default total
|
|
```
|
|
|
|
## 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.
|
|
|
|
```idris
|
|
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`.
|
|
|
|
```idris
|
|
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`
|
|
|
|
```idris
|
|
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
|
|
|
|
```idris
|
|
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
|
|
|
|
```idris
|
|
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
|
|
|
|
```idris
|
|
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.
|
|
|
|
```idris
|
|
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
|
|
|
|
```idris
|
|
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.
|
|
|
|
```idris
|
|
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.
|
|
|
|
```idris
|
|
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
|
|
```
|
|
|
|
```idris hide
|
|
public export covering
|
|
day7 : Day
|
|
day7 = Both 7 part1 part2
|
|
```
|