Year 2015 Day 7 Part 1

README.md

@@ -29,3 +29,4 @@ Provides the `Runner` based command line interface for running a selected day's
   - [Day 4](src/Years/Y2015/Day4.md)
   - [Day 5](src/Years/Y2015/Day5.md)
   - [Day 6](src/Years/Y2015/Day6.md)
+  - [Day 7](src/Years/Y2015/Day7.md)

src/Years/Y2015.md

@@ -12,6 +12,7 @@ import Years.Y2015.Day3
 import Years.Y2015.Day4
 import Years.Y2015.Day5
 import Years.Y2015.Day6
+import Years.Y2015.Day7
 -->
 
 # Days
@@ -58,6 +59,12 @@ y2015 = MkYear 2015 [
   , day6
 ```
 
+## [Day 7](Y2015/Day7.md)
+
+```idris
+  , day7
+```
+
 ```idris
   ]
 ```

src/Years/Y2015/Day7.md

@@ -0,0 +1,219 @@
+# 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 `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
+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
+%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
+
+```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 the context for part 2.
+
+```idris
+covering
+part1 : Eff (PartEff String) (Bits16, SortedDMap Wire Gate)
+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)
+```
+
+<!-- idris
+public export covering
+day7 : Day
+day7 = First 7 part1
+-->