diff --git a/README.md b/README.md index 5bfba46..f40d0a7 100644 --- a/README.md +++ b/README.md @@ -1,24 +1,30 @@ -# Advent +# Advent -The goal of this project is to get all 500 currently available stars in the form of one single idris application, and thoroughly document the results as literate idris files. +The goal of this project is to get all 500 currently available stars in the form +of one single idris application, and thoroughly document the results as literate +idris files. # Index of non-day modules - [Runner](src/Runner.md) - Provides data structures for structuring the division of the project into years, days, and parts. + 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. +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. - + Provides extensions of the functionality of the standard library and external + libraries. Extensions to the standard library are in the base of this module. + - [Util.Eff](src/Util/Eff.md) - - Extend the functionality of the effects included in the [eff](https://github.com/stefan-hoeck/idris2-eff/) library + + Extend the functionality of the effects included in the + [eff](https://github.com/stefan-hoeck/idris2-eff/) library # Index of years and days @@ -30,3 +36,4 @@ Provides the `Runner` based command line interface for running a selected day's - [Day 5](src/Years/Y2015/Day5.md) - [Day 6](src/Years/Y2015/Day6.md) - [Day 7](src/Years/Y2015/Day7.md) + - [Day 8](src/Years/Y2015/Day8.md) diff --git a/src/Grid.md b/src/Grid.md index 77fa988..ceb6a22 100644 --- a/src/Grid.md +++ b/src/Grid.md @@ -2,7 +2,9 @@ Types and utilities for dealing with a 2D grid of things -We base our `Grid` type on `Data.Seq.Sized` from `contrib`, a finger tree based collection that tracks its size in its type, since it provides somewhat efficient random access and updates. +We base our `Grid` type on `Data.Seq.Sized` from `contrib`, a finger tree based +collection that tracks its size in its type, since it provides somewhat +efficient random access and updates. ```idris module Grid @@ -23,7 +25,8 @@ import Decidable.Equality A coordinate is a pair of numbers both less than their respective bounds. -Since `Grid`s will always be non-empty in the contexts we will be using them in, this type alias adds one to each of the bounds to ensure non-emptyness +Since `Grid`s will always be non-empty in the contexts we will be using them in, +this type alias adds one to each of the bounds to ensure non-emptyness ```idris public export @@ -35,11 +38,20 @@ Coord rows cols = (Fin (S rows), Fin (S cols)) Lazily generate all the coordinates for a given pair of bounds -Uses an internal helper function to generate a lazy list of all the fins of a given bound in ascending order (`all`), and another to convert a lazy list of `Fin` into a lazy list of pairs of `Fin`s. +Uses an internal helper function to generate a lazy list of all the fins of a +given bound in ascending order (`all`), and another to convert a lazy list of +`Fin` into a lazy list of pairs of `Fin`s. -The totality checker likes to go in the descending direction, since then it can reason about values getting structurally "smaller", so it has issues with `all'` moving in the ascending direction. We know this function is total because the `acc < last` check will always eventually be triggered, since `Fin`s only have a finite number of values. +The totality checker likes to go in the descending direction, since then it can +reason about values getting structurally "smaller", so it has issues with `all'` +moving in the ascending direction. We know this function is total because the +`acc < last` check will always eventually be triggered, since `Fin`s only have a +finite number of values. -We pull out an `assert_smaller` to tell Idris that the argument to the recursive call is getting structurally smaller, which while not strictly correct, does convey to the compiler that we are getting closer to our recursive base case and that the function is thus total. +We pull out an `assert_smaller` to tell Idris that the argument to the recursive +call is getting structurally smaller, which while not strictly correct, does +convey to the compiler that we are getting closer to our recursive base case and +that the function is thus total. ```idris export @@ -58,9 +70,12 @@ allCords = concat . map row $ all row r = map (\c => (r, c)) all ``` -Add a given vector to a coordinate, returning `Nothing` if we go off the ends of the bounds in the process. +Add a given vector to a coordinate, returning `Nothing` if we go off the ends of +the bounds in the process. -To keep this function simple and reasonably efficient, we perform the arithmetic in integer space, using `integerToFin` to fallably convert back to `Fin` space, making use of the `Maybe` monad to keep the code clean. +To keep this function simple and reasonably efficient, we perform the arithmetic +in integer space, using `integerToFin` to fallably convert back to `Fin` space, +making use of the `Maybe` monad to keep the code clean. ```idris export @@ -89,7 +104,8 @@ record Grid (rows, cols : Nat) (e : Type) where ### Constructors -Construct a `Grid` by filling every slot with identical copies of the provided element +Construct a `Grid` by filling every slot with identical copies of the provided +element ```idris export @@ -100,7 +116,9 @@ replicate seed = in MkGrid grid ``` -Attempt to construct a `Grid` from a Foldable of Foldables. Will return `Nothing` if either the rows are of heterogeneous size, or if either the rows or columns are empty. Requires that the outer Foldable also be Traversable. +Attempt to construct a `Grid` from a Foldable of Foldables. Will return +`Nothing` if either the rows are of heterogeneous size, or if either the rows or +columns are empty. Requires that the outer Foldable also be Traversable. We make heavy use of the `Maybe` monad to keep the code clean here. @@ -133,7 +151,9 @@ fromFoldable xs = do No _ => Nothing ``` -Construct a `Grid` from a non-empty `Vect` of non-empty `Vect`s. To keep the function simple, we require that both the row and column dimension are known to be non-zero before calling this constructor. +Construct a `Grid` from a non-empty `Vect` of non-empty `Vect`s. To keep the +function simple, we require that both the row and column dimension are known to +be non-zero before calling this constructor. ```idris export @@ -141,7 +161,7 @@ fromVect : Vect (S rows) (Vect (S cols) e) -> Grid rows cols e fromVect xs = MkGrid . fromVect . map fromVect $ xs ``` -Construct `Grid` containing the coordinate of the location in each location +Construct `Grid` containing the coordinate of the location in each location ```idris export @@ -296,7 +316,8 @@ Extensions of the above functionality #### Indexing -Convert this grid to one with both the index of the location and the element in each location +Convert this grid to one with both the index of the location and the element in +each location ```idris export @@ -305,6 +326,7 @@ indexed grid = zip coordinateGrid grid ``` Same as `flat` above, but indexed + ```idris export flatIndexed : {rows, cols : Nat} -> Grid rows cols e -> LazyList (Coord rows cols, e) @@ -313,7 +335,8 @@ flatIndexed = flat . indexed #### String functionality -Attempts to convert a string, with newline delimited rows, to a grid of characters +Attempts to convert a string, with newline delimited rows, to a grid of +characters ```idris export @@ -340,6 +363,7 @@ toVects (MkGrid grid) = toVect . map toVect $ grid ``` Convert a grid to a list of lists + ```idris export toLists : Grid rows cols e -> List (List e) diff --git a/src/Main.md b/src/Main.md index b859238..a913135 100644 --- a/src/Main.md +++ b/src/Main.md @@ -1,25 +1,11 @@ -**Table of Contents** - -- [Advent of Code](#advent-of-code) -- [Command Line Interface](#command-line-interface) - - [Error Type](#error-type) - - [Extract the year and day](#extract-the-year-and-day) -- [The Advent ](#the-advent) -- [The Hard Part](#the-hard-part) - - [Parsing the arguments](#parsing-the-arguments) - - [Handling the arguments and finding the input](#handling-the-arguments-and-finding-the-input) - - [Executing the parts](#executing-the-parts) - - [Helper functions](#helper-functions) - - [Print strings to stderr](#print-strings-to-stderr) - - [Decompose a Writer](#decompose-a-writer) - - [Lower logging into the IO component of the effect](#lower-logging-into-the-io-component-of-the-effect) -- [Handle the effectful action as an IO action ](#handle-the-effectful-action-as-an-io-action) - # Advent of Code -This module provides a command line interface for running the solution to a specific day for a specific year, run as `advent $YEAR $DAY`. +This module provides a command line interface for running the solution to a +specific day for a specific year, run as `advent $YEAR $DAY`. -This runner will automatically locate the appropriate input file and then run the selected day's solution against it. See [Runner](Runner.md) for the definitions of the `Day`, `Year`, and `Advent` data types. +This runner will automatically locate the appropriate input file and then run +the selected day's solution against it. See [Runner](Runner.md) for the +definitions of the `Day`, `Year`, and `Advent` data types. ```idris module Main @@ -49,7 +35,9 @@ import Years.Y2015; # Command Line Interface -Since this is a simple application, I am using `GetOpt` from `contrib` for argument parsing. Here we define our options list, a data type to describe our flags, and the usage message header. +Since this is a simple application, I am using `GetOpt` from `contrib` for +argument parsing. Here we define our options list, a data type to describe our +flags, and the usage message header. ```idris data Flag = UseExample | Verbose @@ -68,7 +56,9 @@ header = "Usage: advent YEAR DAY [OPTION...]" ## Error Type -We will be using one unified error type for the entire `Main` module, but we must go ahead and define it before we go any further with command line arguments parsing, as we are about to do some things that might fail. +We will be using one unified error type for the entire `Main` module, but we +must go ahead and define it before we go any further with command line arguments +parsing, as we are about to do some things that might fail. ```idris data Error : Type where @@ -83,8 +73,8 @@ data Error : Type where %name Error err ``` -A `Show` implementation for `Error` is provided, hidden in this document for brevity. - +A `Show` implementation for `Error` is provided, hidden in this document for +brevity. # Days @@ -65,7 +67,12 @@ y2015 = MkYear 2015 [ , day7 ``` +## [Day 8](Y2015/Day8.md) + +```idris + , day8 +``` + ```idris ] ``` - diff --git a/src/Years/Y2015/Day1.md b/src/Years/Y2015/Day1.md index 38c9e42..cfc4950 100644 --- a/src/Years/Y2015/Day1.md +++ b/src/Years/Y2015/Day1.md @@ -1,6 +1,7 @@ # Year 2015 Day 1 -Pretty simple, basic warmup problem, nothing really novel is on display here except the effectful part computations. +Pretty simple, basic warmup problem, nothing really novel is on display here +except the effectful part computations. -### Parsing +### Parsing Pattern match on the action string, throwing an error if the action was invalid @@ -131,7 +136,8 @@ parseAction "toggle" = pure Toggle parseAction str = throw "Invalid action: \{str}" ``` -Attempt to split the string into two parts on the comma, and then attempt to parse the parts as `Fin`s, throwing an appropriate error if anything goes wrong +Attempt to split the string into two parts on the comma, and then attempt to +parse the parts as `Fin`s, throwing an appropriate error if anything goes wrong ```idris parseCoord : Has (Except String) fs => @@ -157,7 +163,8 @@ parseRange pair1 pair2 = do pure $ MkRange top_left bottom_right ``` -Split a string into a list of parts, pattern matching those parts to attempt to extract a `Command`. +Split a string into a list of parts, pattern matching those parts to attempt to +extract a `Command`. ```idris parseCommand : Has (Except String) fs => Has Logger fs => @@ -181,7 +188,10 @@ parseCommand input = do ## Problem structure -Since we are dealing with a million slots here, we'll want some level of true mutability. The actual structure containing the slots doesn't need to be modified once its setup, so we'll make the mutability interior to the slots and keep a `Grid` of `IORef`s. +Since we are dealing with a million slots here, we'll want some level of true +mutability. The actual structure containing the slots doesn't need to be +modified once its setup, so we'll make the mutability interior to the slots and +keep a `Grid` of `IORef`s. We'll setup a helper function to initialize our grid based on a seed value. @@ -193,7 +203,8 @@ ioGrid rows cols seed = in traverse (traverse id) grid ``` -Convert a `Grid` of `IORef`s into a `Grid` of pure values by traversing the `readIORef` operation over our `Grid`. +Convert a `Grid` of `IORef`s into a `Grid` of pure values by traversing the +`readIORef` operation over our `Grid`. ```idris purify : Has IO fs => @@ -208,9 +219,12 @@ purify grid = traverse (traverse readIORef) grid ```idris namespace Part1 ``` -Apply a given command to our `Grid` of `IORef`s. -Use our `extractRange` function to extract all the `IORef`s in the grid cells touched by our `Range` and then traverse an appropriate mutating action over them. +Apply a given command to our `Grid` of `IORef`s. + +Use our `extractRange` function to extract all the `IORef`s in the grid cells +touched by our `Range` and then traverse an appropriate mutating action over +them. ```idris applyCommand : Has IO fs => @@ -223,7 +237,8 @@ Use our `extractRange` function to extract all the `IORef`s in the grid cells to Toggle => Lazy.traverse_ (`modifyIORef` not) cells ``` -Apply a list of commands to our `Grid` of `IORef`s, doing some debug logging along the way. +Apply a list of commands to our `Grid` of `IORef`s, doing some debug logging +along the way. ```idris export @@ -246,7 +261,8 @@ Apply a list of commands to our `Grid` of `IORef`s, doing some debug logging alo namespace Part2 ``` -Much the same as above, but instead we apply the part 2 rules to a `Grid` of `Nat`. +Much the same as above, but instead we apply the part 2 rules to a `Grid` of +`Nat`. ```idris applyCommand : Has IO fs => @@ -259,7 +275,9 @@ Much the same as above, but instead we apply the part 2 rules to a `Grid` of `Na Toggle => Lazy.traverse_ (`modifyIORef` (+ 2)) cells ``` -Identical to above, except for using our part 2 `applyCommand`. We can use the same name here because we have the two variants behind namespaces and Idris can disambiguate via the types. +Identical to above, except for using our part 2 `applyCommand`. We can use the +same name here because we have the two variants behind namespaces and Idris can +disambiguate via the types. ```idris export @@ -280,7 +298,9 @@ Identical to above, except for using our part 2 `applyCommand`. We can use the s ### Part 1 -Parse our commands, generate our initial `Grid` with all the lights turned off (represented by `False`), apply our commands to it, purify it, and count the lights that are turned on. +Parse our commands, generate our initial `Grid` with all the lights turned off +(represented by `False`), apply our commands to it, purify it, and count the +lights that are turned on. Pass out our list of parsed commands as the context for reuse in part 2. @@ -298,7 +318,9 @@ part1 = do ### Part 2 -This time, use an initial `Grid` with all brightness values at 0, apply our list of preparsed commands using our part 2 `applyCommands` function (selected via the type signature), and then add up the brightnesses. +This time, use an initial `Grid` with all brightness values at 0, apply our list +of preparsed commands using our part 2 `applyCommands` function (selected via +the type signature), and then add up the brightnesses. ```idris part2 : List (Command 999 999) -> Eff (PartEff String) Nat diff --git a/src/Years/Y2015/Day7.md b/src/Years/Y2015/Day7.md index 2a8df71..5919288 100644 --- a/src/Years/Y2015/Day7.md +++ b/src/Years/Y2015/Day7.md @@ -2,9 +2,16 @@ 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. +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. +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.String +import Data.Vect +import Data.List.Lazy +import Data.Either +``` + +## Parsing + +A "Parser" is an effectful computation that has access to a list of chars as +state, can throw exceptions of type `String`, and has non-determinism through +the `Choose` effect, which consumes some of the state to potentially return a +value. + +### Basic operation + +Get the next character out of the parser state, updating the state to consume +that character. + +```idris +nextChar : Has (State (List Char)) fs => Has (Except String) fs => Eff fs Char +nextChar = do + c :: rest <- get + | [] => throw "End of input" + put rest + pure c +``` + +Attempt to parse a single character based on the supplied predicate, consuming +the character from the state and throwing the provided error if the predicate +does not hold over the consumed character. + +```idris +char : Has (State (List Char)) fs => Has (Except String) fs => + (pred : Char -> Bool) -> (err : Char -> String) -> Eff fs Char +char pred err = do + c <- nextChar + unless (pred c) (throw $ err c) + pure c +``` + +Type alias for a parser + +```idris +Parser : (res : Type) -> Type +Parser res = Eff [State (List Char), Except String, Choose, Logger] res +``` + +Parse 0+ of a thing, speculatively attempting to apply the given parser. In the +event the supplied parser fails, catch the error, unwind changes to the state, +and return an empty list, otherwise append the parsed element to the head of the +returned list and recurse. + +The rewinding of the state on failure _could_ be handled by the effect stack if +`Except` was structured a bit differently, but that's a topic for another day. + +```idris +many : (f : Parser t) -> Parser (List t) +many f = do + state <- get + Just x <- lift $ catch (\ _ => pure Nothing) (map Just f) + | Nothing => do + put state + pure [] + map (x ::) $ many f +``` + +"Parse" the end of the input, returning a unit if we are at the end of input, +throwing an error otherwise. + +```idris +endOfInput : Parser () +endOfInput = do + [] <- get + | xs => throw "Expected end of input, state non empty: `\{pack xs}`" + pure () +``` + +### Character Classes + +Parse a single `"`, throwing an error if the current character is anything else. +Returns a unit since there is only one possible character this parses, and this +avoids us having to discard the character later in our `string` parser. + +```idris +quote : Parser () +quote = do + _ <- char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`") + pure () +``` + +Parse any character except `\` or `"` + +```idris +normal : Parser Char +normal = + char + (\x => not $ any (== x) (the (List _) ['\\', '"'])) + (\x => "Expected normal, got `\{String.singleton x}`") +``` + +#### Escaped Characters + +Parse the character sequence `\"`, returning just the `"`. Despite the fact that +can only return one possible character, like `quote` above, we return the parsed +character, as we intend to provide all the escaped character parsers to the +`oneOfM` combinator later. + +```idris +eQuote : Parser Char +eQuote = do + _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") + char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`") +``` + +Parse the character sequence `\\`, returning just the second `\`. + +```idris +eSlash : Parser Char +eSlash = do + _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") + char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") +``` + +Convert a lowercase hexadecimal digit to its numerical value. + +```idris +fromHex : Char -> Int +fromHex c = + if ord c >= 97 + then ord c - 87 + else ord c - 48 +``` + +Parse a character sequence `\xAB`, where `AB` are hexadecimal digits, and decode +the numerical value of `AB`, as a hexadecimal number, into its corresponding +character. + +```idris +eHex : Parser Char +eHex = do + _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") + _ <- char (== 'x') (\x => "Expected `x`, got `\{String.singleton x}`") + [x, y] <- map (map $ fromHex . toLower) . + sequence . + Vect.replicate 2 $ + (char + isHexDigit + (\x => "Expected hex digit, got `\{String.singleton x}`")) + pure . chr $ x * 0x10 + y +``` + +Use the `oneOfM` combinator to combine our escaped character parsers into a +single character class. `oneOfM` uses the `Choice` effect to try all of the +provided parsers, conceptually in parallel, returning all of the results. + +```idris +escaped : Parser Char +escaped = oneOfM $ the (List _) [eQuote, eSlash, eHex] +``` + +### Top Level Class + +Combine our `normal` and `escaped` parsers into a single parser for non-quote +characters. + +```idris +character : Parser Char +character = oneOfM $ the (List _) [normal, escaped] +``` + +Parse a string literal by describing its layout as a quote (`"`), followed by +any number of characters, then another quote, followed by the end of input. +Return the characters between the outer quotes. + +```idris +string : Parser (List Char) +string = do + quote + xs <- many character + quote + endOfInput + pure xs +``` + +## Running a parser + +Run a parser, with some debug logging, by peeling the parsing effects of of the +type. The order is important here, remember that function composition "runs" +right to left. + +We peel the state off the type first, so that we can get implicit "rewinding" of +the state inside of our combinators, like `oneOfM`. + +For a full understanding of what's going on here, we need to see how the type +signature changes as we peel effects off the type, you can uncomment the +commented lines, and comment out the rest of the function, modifying the +`let output =` line to follow along yourself, though the types you get may look +a little different due to idris evaluating type alaises like `Eff` for you, I am +keeping them in aliased forms, and excluding `Logger`, which doesn't impact the +semantic of parsing, to keep the examples concise: + +- `runstate (unpack str) $ x` + + This produces a value with type + `Eff [Except String, Choose] (List Char, List Char)`. In this tuple of values, + the first element is the actual output of the parser, and the second element + is the state after the parser has run. + +- `runExcept . runState (unpack str) $ x` + + This produces a value with type + `Eff [Choose] (Either String (List Char, List Char))`. This corresponds to a + computation that either returns our tuple of output and state from before, or + an error. Important to note here is that, in the error case, we only return a + `String` (our error type), our state is discarded. + +- `runChoose {f = LazyList} . runExcept . runState (unpack str) $ x` + + The `Choose` effect, works with any type that implements the `Alternative` + interface, and the choice of type impacts the semantics. A full discussion of + this is beyond the scope for today, but we chose to "run" `Choose` with + `LazyList`, which effectively gives us an iterator over all the possible + parsings of our input text. + + This produces a value with type + `Eff [] (LazyList (Either String (List Char, List Char)))`. When we hit an + application of `Choose`, like `oneOfM`, all possibilities will be tried and + each one will be added to our output `LazyList`. Because this is a `LazyList`, + and not a `List`, only values we actually inspect are generated, allowing + parsing to terminate after the first successful parse without having to + generate the rest of the list. + + Note that we have an independent possible state value for each slot in the + list, this speaks to this effect stack, when run in this order, providing a + sort of branching behavior for states, allowing different branches in the + `Choose` effect to modify their state without impacting the state of other + branches. + +From there, we run our `lazyRights` helper function over the outputs `LazyList` +to discard parsing paths that result in an error, extract the first element of +each tuple, get the head of the list, if one still exists, and use `pack` to +convert the contents of the resulting `Maybe (List Char)` to a string. Then a +little bit of debug logging, and return the output. + +```idris +runParser : Has Logger fs => Parser (List Char) -> String + -> Eff fs $ Maybe String +runParser x str = do + info "Parsing: \{str}" + -- let outputs = + -- runChoose {f = LazyList} . runExcept . runState (unpack str) $ x + -- ?parser_types + outputs <- + lift . runChoose {f = LazyList} . runExcept . runState (unpack str) $ x + let output = map pack . head' . map fst . lazyRights $ outputs + case output of + Nothing => + debug "Failed: \{show outputs}" + Just y => do + debug "Got: \{y}" + trace "\{show outputs}" + pure output + where + lazyRights : LazyList (Either a b) -> LazyList b + lazyRights [] = [] + lazyRights (Left _ :: xs) = lazyRights xs + lazyRights (Right x :: xs) = x :: lazyRights xs +``` + +## Part Functions + +### Part 1 + +Convert the inputs into a list of lines, traverse our parser over it, deal with +possible failures by sequencing the `List (Maybe String)` into a +`Maybe (List String)`, and the compute the difference in character counts. + +```idris +part1 : Eff (PartEff String) (Int, ()) +part1 = do + inputs <- map lines $ askAt "input" + outputs <- traverse (runParser string) inputs + Just outputs <- pure $ sequence outputs + | _ => throw "Some strings failed to parse" + let difference = + sum $ zipWith (\x, y => strLength x - strLength y) inputs outputs + pure (difference, ()) +``` + +