From feb75002bde190054cc6264b17c0a180cf32cde9 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 10 Jan 2025 14:16:31 -0500 Subject: [PATCH 1/4] Readme fix --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index b289f91..bd60f8c 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. From 080b9f8c77b65fb9916e1118c621dd945d807df3 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 10 Jan 2025 15:31:24 -0500 Subject: [PATCH 2/4] Include year in markdown headers --- src/Years/Y2015/Day1.md | 2 +- src/Years/Y2015/Day2.md | 2 +- src/Years/Y2015/Day3.md | 2 +- src/Years/Y2015/Day4.md | 2 +- src/Years/Y2015/Day5.md | 2 +- src/Years/Y2015/Day6.md | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) 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 # Days @@ -58,6 +59,12 @@ y2015 = MkYear 2015 [ , day6 ``` +## [Day 7](Y2015/Day7.md) + +```idris + , day7 +``` + ```idris ] ``` diff --git a/src/Years/Y2015/Day7.md b/src/Years/Y2015/Day7.md new file mode 100644 index 0000000..f8abae3 --- /dev/null +++ b/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 +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 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) +``` + + From 5a313c952f10bdc1206048fd3f7364ef214dca1b Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 10 Jan 2025 22:47:58 -0500 Subject: [PATCH 4/4] Year 2015 Day 7 Part 2 --- src/Years/Y2015/Day7.md | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/src/Years/Y2015/Day7.md b/src/Years/Y2015/Day7.md index f8abae3..2a8df71 100644 --- a/src/Years/Y2015/Day7.md +++ b/src/Years/Y2015/Day7.md @@ -197,11 +197,11 @@ solveWire wire = do ### 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. +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) +part1 : Eff (PartEff String) (Bits16, (SortedDMap Wire Gate, Literal)) part1 = do circut <- askAt "input" >>= parseGates (value, _) <- @@ -209,11 +209,28 @@ part1 = do {fs = State (SortedMap Wire Literal) :: Reader (SortedDMap Wire Gate) :: PartEff String } - pure (value, circut) + 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 ```