# 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
-->