diff --git a/README.md b/README.md index b289f91..5bfba46 100644 --- a/README.md +++ b/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) diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index b3679ff..19be161 100644 --- a/src/Years/Y2015.md +++ b/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 ] ``` diff --git a/src/Years/Y2015/Day1.md b/src/Years/Y2015/Day1.md index 352f7cd..38c9e42 100644 --- a/src/Years/Y2015/Day1.md +++ b/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. diff --git a/src/Years/Y2015/Day2.md b/src/Years/Y2015/Day2.md index 733f351..51641d4 100644 --- a/src/Years/Y2015/Day2.md +++ b/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 diff --git a/src/Years/Y2015/Day3.md b/src/Years/Y2015/Day3.md index cb3edbc..af7f5e2 100644 --- a/src/Years/Y2015/Day3.md +++ b/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. diff --git a/src/Years/Y2015/Day4.md b/src/Years/Y2015/Day4.md index 29c4ca8..04d5f40 100644 --- a/src/Years/Y2015/Day4.md +++ b/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. diff --git a/src/Years/Y2015/Day5.md b/src/Years/Y2015/Day5.md index ba47358..40ed6f0 100644 --- a/src/Years/Y2015/Day5.md +++ b/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. diff --git a/src/Years/Y2015/Day6.md b/src/Years/Y2015/Day6.md index a41508a..cc95926 100644 --- a/src/Years/Y2015/Day6.md +++ b/src/Years/Y2015/Day6.md @@ -1,4 +1,4 @@ -# Day 6 +# Year 2015 Day 6 + +```idris +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. + +```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 +``` + +