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