From b0e7c1aa917c020192032132524c70119259a8d0 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Tue, 14 Jan 2025 15:15:09 -0500 Subject: [PATCH] Reformat markdown --- README.md | 22 +++++---- src/Grid.md | 50 ++++++++++++++----- src/Main.md | 104 ++++++++++++++++++++++++---------------- src/Runner.md | 96 ++++++++++++++++++++++++------------- src/Util.md | 11 +++-- src/Util/Eff.md | 23 ++++++--- src/Years/Y2015.md | 2 +- src/Years/Y2015/Day1.md | 19 +++++--- src/Years/Y2015/Day2.md | 27 +++++++---- src/Years/Y2015/Day3.md | 51 +++++++++++++++----- src/Years/Y2015/Day4.md | 82 +++++++++++++++++++++++-------- src/Years/Y2015/Day5.md | 72 +++++++++++++++++++++------- src/Years/Y2015/Day6.md | 52 ++++++++++++++------ src/Years/Y2015/Day7.md | 36 ++++++++++---- 14 files changed, 459 insertions(+), 188 deletions(-) diff --git a/README.md b/README.md index 5bfba46..27f2774 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 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. -### 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.