Year 2015 Day 7 Part 2

README.md

@@ -7,6 +7,11 @@ The goal of this project is to get all 500 currently available stars in the form
 - [Runner](src/Runner.md)
 
   Provides data structures for structuring the division of the project into years, days, and parts.
+
+- [Main](src/Main.md)
+
+Provides the `Runner` based command line interface for running a selected day's solution.
+
 - [Util](src/Util.md)
 
   Provides extensions of the functionality of the standard library and external libraries. Extensions to the standard library are in the base of this module.
@@ -24,3 +29,4 @@ The goal of this project is to get all 500 currently available stars in the form
   - [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/Day1.md

@@ -1,4 +1,4 @@
-# Day 1
+# Year 2015 Day 1
 
 Pretty simple, basic warmup problem, nothing really novel is on display here except the effectful part computations.
 

src/Years/Y2015/Day2.md

@@ -1,4 +1,4 @@
-# Day 2
+# Year 2015 Day 2
 
 This day provides us our first little taste of effectful parsing
 

src/Years/Y2015/Day3.md

@@ -1,4 +1,4 @@
-# Day 3
+# Year 2015 Day 3
 
 This day provides a gentle introduction to `mutual` blocks and mutually recursive functions. 
 

src/Years/Y2015/Day4.md

@@ -1,4 +1,4 @@
-# Day 4
+# Year 2015 Day 4
 
 This day introduces us to a little bit of FFI, linking to openssl to use it's `MD5` functionality.
 

src/Years/Y2015/Day5.md

@@ -1,4 +1,4 @@
-# Day 5
+# Year 2015 Day 5
 
 This day provides a nice chance to introduce [views](https://idris2.readthedocs.io/en/latest/tutorial/views.html), specifically `String`'s [`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList) view, which lets us treat `String`s as if they were lazy lists or iterators.
 

src/Years/Y2015/Day6.md

@@ -1,4 +1,4 @@
-# Day 6
+# Year 2015 Day 6
 
 <!-- idris
 module Years.Y2015.Day6

src/Years/Y2015/Day7.md

@@ -0,0 +1,236 @@
+# 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 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
+public export covering
+day7 : Day
+day7 = Both 7 part1 part2
+-->