Idris/advent
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

Reformat markdown

Browse source
This commit is contained in:
Nathan McCarty 2025-01-14 15:15:09 -05:00
parent 5a313c952f
commit b0e7c1aa91
14 changed files with 459 additions and 188 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
README.md
View file

@ -1,24 +1,30 @@
# 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

48
src/Grid.md
View file

@ -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
@ -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)

100
src/Main.md
View file

@ -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.
<!-- idris
Show Error where
@ -112,7 +102,11 @@ Show Error where
## Extract the year and day
After peeling off our options from the arguments using `GetOpt`, we will be left with a list of non-option arguments, which we must then parse into our year number/day number pair. We perform some pattern matching to make sure the list is the correct length, and then parse the individual integers, throwing an error if anything goes wrong
After peeling off our options from the arguments using `GetOpt`, we will be left
with a list of non-option arguments, which we must then parse into our year
number/day number pair. We perform some pattern matching to make sure the list
is the correct length, and then parse the individual integers, throwing an error
if anything goes wrong
```idris
||| Convert the non-option arguments into a Year/Day pair
@ -129,7 +123,10 @@ argumentsToPair xs = throw $ ArgumentsError (length xs)
# The Advent
Construct our top-level `Advent` record from the imported `Year` modules. The argument to the `MkAdvent` constructor is a `FreshList`, with a freshness criteria ensuring that the list is in ascending order and does not include any duplicate `Year`s.
Construct our top-level `Advent` record from the imported `Year` modules. The
argument to the `MkAdvent` constructor is a `FreshList`, with a freshness
criteria ensuring that the list is in ascending order and does not include any
duplicate `Year`s.
```idris
advent : Advent
@ -140,11 +137,17 @@ advent = MkAdvent [
# The Hard Part
Now we must glue everything together, parse our arguments, handle any supplied options, locate the relevant year and day, locate the corresponding input file, read it, and then run the selected `Day` against it.
Now we must glue everything together, parse our arguments, handle any supplied
options, locate the relevant year and day, locate the corresponding input file,
read it, and then run the selected `Day` against it.
Because we are building our application around effects, the actual core of the application is the effectful `start` computation, that the `main` function will then apply `IO` based handlers to.
Because we are building our application around effects, the actual core of the
application is the effectful `start` computation, that the `main` function will
then apply `IO` based handlers to.
Our reader and writer aren't ready yet, we need to do some setup first, so the top level type signature doesn't include them, so we'll add them to the effects list as they become available.
Our reader and writer aren't ready yet, we need to do some setup first, so the
top level type signature doesn't include them, so we'll add them to the effects
list as they become available.
```idris
covering
@ -155,7 +158,9 @@ start = do
## Parsing the arguments
Feed the augments from `System.getArgs` into `getOpt`, making sure to drop the name the binary was invoked with, then check for any errors in the result, throwing our own error if any are encountered.
Feed the augments from `System.getArgs` into `getOpt`, making sure to drop the
name the binary was invoked with, then check for any errors in the result,
throwing our own error if any are encountered.
```idris
-- Read and parse arguments/options
@ -165,7 +170,9 @@ Feed the augments from `System.getArgs` into `getOpt`, making sure to drop the n
throw (OptionsError opts.errors)
```
Use our `argumentsToPair` function to extract the selected year and day numbers from the positional arguments, implicitly throwing an error if there are any failures doing so.
Use our `argumentsToPair` function to extract the selected year and day numbers
from the positional arguments, implicitly throwing an error if there are any
failures doing so.
```idris
(year, day_n) <- argumentsToPair opts.nonOptions
@ -173,7 +180,9 @@ Use our `argumentsToPair` function to extract the selected year and day numbers
## Handling the arguments and finding the input
Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise blackhole the logs. Afterwards, use `logHandler` to introduce the logging `Writer` into the effects list.
Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise
blackhole the logs. Afterwards, use `logHandler` to introduce the logging
`Writer` into the effects list.
```idris
-- If the verbose flag is set, hook up the logging writer to stderr
@ -184,9 +193,13 @@ Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise
logHandler $ do
```
Find the current directory and append to it to find the input file. If the `--use-example/-u` flag is set, look for the input file at `inputs/examples/$year/$day`, otherwise look for it at `inputs/real/$year/$day`.
Find the current directory and append to it to find the input file. If the
`--use-example/-u` flag is set, look for the input file at
`inputs/examples/$year/$day`, otherwise look for it at `inputs/real/$year/$day`.
After we've located it, attempt to read from it, throwing an `InputRead` error if any errors occur, then insert the contents into our `Reader` and inject it into the effects list.
After we've located it, attempt to read from it, throwing an `InputRead` error
if any errors occur, then insert the contents into our `Reader` and inject it
into the effects list.
```idris
-- Locate and read in the input file
@ -201,7 +214,8 @@ After we've located it, attempt to read from it, throwing an `InputRead` error i
runReaderAt "input" contents {fs = PartEff Error} $ do
```
Try and locate the `Day` in our `Advent` record, throwing an error if we are unable to locate it
Try and locate the `Day` in our `Advent` record, throwing an error if we are
unable to locate it
```idris
-- Attempt to locate the provided day
@ -210,7 +224,9 @@ Try and locate the `Day` in our `Advent` record, throwing an error if we are una
## Executing the parts
Run the selected `Day`'s part 1, wrapping any errors that it returns in a `SolveError`. Collect both the result and the opaque context value, then print out the result.
Run the selected `Day`'s part 1, wrapping any errors that it returns in a
`SolveError`. Collect both the result and the opaque context value, then print
out the result.
```idris
-- Run part 1
@ -220,7 +236,9 @@ Run the selected `Day`'s part 1, wrapping any errors that it returns in a `Solve
putStrLn $ unlines . map (" " ++) . lines . show @{day.showOut1} $ part_1
```
Check and see if the selected `Day` has a part 2, if it does, feed the opaque context value collected from part 1 into it, wrap any errors that it returns in a `SolveError`, then print out the result, then return, closing out the program.
Check and see if the selected `Day` has a part 2, if it does, feed the opaque
context value collected from part 1 into it, wrap any errors that it returns in
a `SolveError`, then print out the result, then return, closing out the program.
```idris
-- Run part 2 if we have it
@ -241,7 +259,8 @@ Check and see if the selected `Day` has a part 2, if it does, feed the opaque co
### Lower logging into the IO component of the effect
This function uses the provided `String -> IO ()` to remove the `Writer` from the effects list by translating `tell` calls to IO actions within the effect.
This function uses the provided `String -> IO ()` to remove the `Writer` from
the effects list by translating `tell` calls to IO actions within the effect.
```idris
-- Lowers logging into IO within the effect using the given IO function
@ -257,9 +276,12 @@ This function uses the provided `String -> IO ()` to remove the `Writer` from th
# Handle the effectful action as an IO action
Use `runEff` to translate the effects in `start`'s effects list into IO actions, and return the resulting `IO ()`.
Use `runEff` to translate the effects in `start`'s effects list into IO actions,
and return the resulting `IO ()`.
The `IO` component of the effects list is handled via `id`, translating `IO` actions into themselves, and we construct a helper function to handle errors as IO actions by printing the error and crashing the program.
The `IO` component of the effects list is handled via `id`, translating `IO`
actions into themselves, and we construct a helper function to handle errors as
IO actions by printing the error and crashing the program.
```idris
covering

96
src/Runner.md
View file

@ -1,23 +1,12 @@
**Table of Contents**
- [Unified interface for any day from any year](#unified-interface-for-any-day-from-any-year)
- [Effectful Parts](#effectful-parts)
- [The `Day` Record](#the-day-record)
- [Smarter Constructors](#smarter-constructors)
- [First](#first)
- [Both](#both)
- [Freshness](#freshness)
- [The `Year` Record](#the-year-record)
- [Freshness](#freshness-1)
- [The `Advent` Record](#the-advent-record)
- [Methods](#methods)
- [locate](#locate)
# Unified interface for any day from any year
This module provides some basic data types for building an application containing all my solutions to all of the parts of all the days across all of the years.
This module provides some basic data types for building an application
containing all my solutions to all of the parts of all the days across all of
the years.
This provides a defensively built API for constructing the overall `Advent` data structure that prevents registering a day/year twice or registering days/years out of order.
This provides a defensively built API for constructing the overall `Advent` data
structure that prevents registering a day/year twice or registering days/years
out of order.
```idris
module Runner
@ -32,9 +21,18 @@ import public Util.Eff
# Effectful Parts
The solution to each part of a day is run as an effectful computation, and as the available effects are meant to be the same across both parts, only varying in the type of the error value in the `Except` effect, I construct a type level function to have a single source of truth for this. The `err` type can be any type with a `Show` implementation, but that constraint will be tacked on in the next step.
The solution to each part of a day is run as an effectful computation, and as
the available effects are meant to be the same across both parts, only varying
in the type of the error value in the `Except` effect, I construct a type level
function to have a single source of truth for this. The `err` type can be any
type with a `Show` implementation, but that constraint will be tacked on in the
next step.
A `Writer` effect is provided for logging, and a `Reader` effect is provided to pass in the input, just to make the top level API a little bit cleaner. `IO` is also provided, even though the part solutions themselves shouldn't really be doing any IO, this may come in handy if a part needs `IO` for performance reasons.
A `Writer` effect is provided for logging, and a `Reader` effect is provided to
pass in the input, just to make the top level API a little bit cleaner. `IO` is
also provided, even though the part solutions themselves shouldn't really be
doing any IO, this may come in handy if a part needs `IO` for performance
reasons.
```idris
||| The effect type is the same in boths parts one and two, modulo potentially
@ -47,11 +45,20 @@ PartEff err =
# The `Day` Record
The `Day` type groups together an effectful `part1` computation, an optional effectful `part2` computation, the day number, and does some type wrangling to get the type system out of our way on this one.
The `Day` type groups together an effectful `part1` computation, an optional
effectful `part2` computation, the day number, and does some type wrangling to
get the type system out of our way on this one.
`part1` and `part2` are allowed independent output and error types, and this record captures `Show` implementations for those output and error types so that we can display them in `Main` where the `Day` is consumed without having to actually know what the types are.
`part1` and `part2` are allowed independent output and error types, and this
record captures `Show` implementations for those output and error types so that
we can display them in `Main` where the `Day` is consumed without having to
actually know what the types are.
It is often useful to pass a bit of context, such as the data structures resulting from parsing, between `part1` and `part2`, and this is achieved by the erased `ctx` type, which is totally opaque here. The runner code in `Main` will provide the value of the `ctx` type produced as part of the output of `part1` as the input of `part2`.
It is often useful to pass a bit of context, such as the data structures
resulting from parsing, between `part1` and `part2`, and this is achieved by the
erased `ctx` type, which is totally opaque here. The runner code in `Main` will
provide the value of the `ctx` type produced as part of the output of `part1` as
the input of `part2`.
```idris
||| Model solving a single day
@ -71,7 +78,11 @@ record Day where
## Smarter Constructors
The default `MkDay` constructor is slightly cumbersome to use, always requiring _something_ for the `part2` slot, even if there isn't a part 2 yet, and requiring that `part2` be wrapped in a `Just` when there is one, so we provide a pair of constructors for the case where there is only a `part1` and for where there is a `part1` and a `part2` that handle that for us.
The default `MkDay` constructor is slightly cumbersome to use, always requiring
_something_ for the `part2` slot, even if there isn't a part 2 yet, and
requiring that `part2` be wrapped in a `Just` when there is one, so we provide a
pair of constructors for the case where there is only a `part1` and for where
there is a `part1` and a `part2` that handle that for us.
```idris
namespace Day
@ -79,7 +90,9 @@ namespace Day
### First
The `First` constructor only accepts a `part1`, it does the work of filling in `part2` with `Nothing` and setting all of `part2`'s type arguments to `()` for us.'
The `First` constructor only accepts a `part1`, it does the work of filling in
`part2` with `Nothing` and setting all of `part2`'s type arguments to `()` for
us.'
```idris
||| Constructor for a day with only part one ready to run
@ -93,7 +106,8 @@ The `First` constructor only accepts a `part1`, it does the work of filling in `
### Both
The `Both` constructor does a little bit less heavy lifting, the only thing it needs to do for us is wrap `part2` in a `Just`.
The `Both` constructor does a little bit less heavy lifting, the only thing it
needs to do for us is wrap `part2` in a `Just`.
```idris
||| Constructor for a day with both parts ready to run
@ -108,9 +122,17 @@ The `Both` constructor does a little bit less heavy lifting, the only thing it n
## Freshness
We will be using a _Fresh List_ from the [structures](https://git.sr.ht/~thatonelutenist/Structures) package to build defensiveness into the API. A Fresh List structurally only allows you to prepend an element onto it when it satisfies some _freshness_ criteria relative to the elements already in the list.
We will be using a _Fresh List_ from the
[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build
defensiveness into the API. A Fresh List structurally only allows you to prepend
an element onto it when it satisfies some _freshness_ criteria relative to the
elements already in the list.
Here, we compare the day numbers of the two `Day`s using the less-than relationship. Since we are operating on the start of the list when this comparison takes place, this enforces, through type checking, that the resulting Fresh List is sorted in ascending order and that no two `Day`s have the same day number.
Here, we compare the day numbers of the two `Day`s using the less-than
relationship. Since we are operating on the start of the list when this
comparison takes place, this enforces, through type checking, that the resulting
Fresh List is sorted in ascending order and that no two `Day`s have the same day
number.
```idris
||| Freshness criteria for days
@ -127,7 +149,8 @@ FreshDay x y = x.day < y.day
# The `Year` Record
The `Year` record collects a number of `Day`s into a single Fresh List for the year, and is mostly just a simple container.
The `Year` record collects a number of `Day`s into a single Fresh List for the
year, and is mostly just a simple container.
```idris
||| Collect all the days in a given year
@ -141,7 +164,11 @@ record Year where
## Freshness
Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored in a `FreshList` in `Advent`, so we need to provide a freshness criteria for `Year` as well. We do so by applying the less-than relationship against the year number of the two `Years`, for the same reasons and with the same results as with `FreshDay`.
Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored
in a `FreshList` in `Advent`, so we need to provide a freshness criteria for
`Year` as well. We do so by applying the less-than relationship against the year
number of the two `Years`, for the same reasons and with the same results as
with `FreshDay`.
```idris
||| Freshness criteria for years
@ -158,7 +185,9 @@ FreshYear x y = x.year < y.year
# The `Advent` Record
The `Advent` record collects a number of `Year`s in much the same way that `Year` collects a number of days, sorting the `Year`s in a `FreshList` to provide API defensiveness.
The `Advent` record collects a number of `Year`s in much the same way that
`Year` collects a number of days, sorting the `Year`s in a `FreshList` to
provide API defensiveness.
```idris
||| Collect all years
@ -177,9 +206,12 @@ namespace Advent
### locate
This is a utility function that searches the `FreshList` of `Year`s for the provided year number, then searches the resulting `Year`, if one exists, for the provided day number.
This is a utility function that searches the `FreshList` of `Year`s for the
provided year number, then searches the resulting `Year`, if one exists, for the
provided day number.
We don't have to worry about potentially encountering duplicates here because of the freshness restriction.
We don't have to worry about potentially encountering duplicates here because of
the freshness restriction.
```idris
||| Attempt to locate `Day` entry corresponding to the provided day and year numbers

11
src/Util.md
View file

@ -1,6 +1,7 @@
# Utility functions
This module contains functions that extend the functionality of standard data types, other types of utility functionality get their own module
This module contains functions that extend the functionality of standard data
types, other types of utility functionality get their own module
```idris
module Util
@ -20,7 +21,8 @@ namespace Either
### mapLeft
Applies a function to the contents of a `Left` if the value of the given `Either` is actually a `Left`, otherwise, leaves `Right`s untouched.
Applies a function to the contents of a `Left` if the value of the given
`Either` is actually a `Left`, otherwise, leaves `Right`s untouched.
```idris
export
@ -28,6 +30,7 @@ Applies a function to the contents of a `Left` if the value of the given `Either
mapLeft f (Left x) = Left (f x)
mapLeft f (Right x) = Right x
```
## Vectors
Define some operations for pairs of numbers, treating them roughly like vectors
@ -81,7 +84,9 @@ namespace String
Returns `True` if `needle` is a substring of `haystack`
We first check to see if the needle is a prefix of the top level haystack, before calling into a tail recursive helper function that peels one character off of the string at a time, checking if the needle is a prefix at each step.
We first check to see if the needle is a prefix of the top level haystack,
before calling into a tail recursive helper function that peels one character
off of the string at a time, checking if the needle is a prefix at each step.
```idris
export

23
src/Util/Eff.md
View file

@ -18,7 +18,8 @@ import System.File
### Log Levels
Basic enumeration describing log levels, we define some (hidden) utility functions for working with these.
Basic enumeration describing log levels, we define some (hidden) utility
functions for working with these.
```idris
public export
@ -79,7 +80,9 @@ levelToTag (Other k) =
### Logger effect
This is a basic data structure that captures a lazy log message (so we don't have to pay any of the costs associated with generating the log message when it is filtered)
This is a basic data structure that captures a lazy log message (so we don't
have to pay any of the costs associated with generating the log message when it
is filtered)
```idris
public export
@ -87,7 +90,8 @@ data Logger : Type -> Type where
Log : (level : Level) -> (msg : Lazy String) -> Logger ()
```
We'll also provide some basic accessors, and an `ignore` function useful for writing handlers.
We'll also provide some basic accessors, and an `ignore` function useful for
writing handlers.
```idris
export
@ -105,9 +109,13 @@ ignore (Log level msg) = ()
#### Handler
Because we know that we will only be using `logger` in an `IO` context, we aren't currently going to provide a `runLogger` or the like, instead we'll define a function, suitable for use as a `runEff` handler, that filters log messages and prints them to `stderr` over `IO`.
Because we know that we will only be using `logger` in an `IO` context, we
aren't currently going to provide a `runLogger` or the like, instead we'll
define a function, suitable for use as a `runEff` handler, that filters log
messages and prints them to `stderr` over `IO`.
In the event a log message is filtered out, it's inner message is never inspected, avoiding evaluation.
In the event a log message is filtered out, it's inner message is never
inspected, avoiding evaluation.
```idris
export
@ -121,7 +129,10 @@ handleLoggerIO max_level x =
else pure . ignore $ x
```
Use the `WriterL "log" String` effect like a logging library. We'll provide a few "log levels" as verbs for the effect, but no filtering is done, when logging is enabled, all logs are always displayed, however the log level is indicated with a colored tag.
Use the `WriterL "log" String` effect like a logging library. We'll provide a
few "log levels" as verbs for the effect, but no filtering is done, when logging
is enabled, all logs are always displayed, however the log level is indicated
with a colored tag.
```idris
export

2
src/Years/Y2015.md
View file

@ -5,6 +5,7 @@ import Structures.Dependent.FreshList
import Runner
```
<!-- idris
import Years.Y2015.Day1
import Years.Y2015.Day2
@ -68,4 +69,3 @@ y2015 = MkYear 2015 [
```idris
]
```

19
src/Years/Y2015/Day1.md
View file

@ -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.
<!-- idris
module Years.Y2015.Day1
@ -14,9 +15,11 @@ import Runner
## Solver Functions
This one implements the entirety of the logic for part 1, in a simple tail recursive manner, pattern matching on each character in the input string.
This one implements the entirety of the logic for part 1, in a simple tail
recursive manner, pattern matching on each character in the input string.
We include a case for a non-paren character for totality's sake, but since we kinda trust the input here we just don't do anything in that branch.
We include a case for a non-paren character for totality's sake, but since we
kinda trust the input here we just don't do anything in that branch.
```idris
trackFloor : (start : Integer) -> (xs : List Char) -> Integer
@ -26,7 +29,9 @@ trackFloor start (')' :: xs) = trackFloor (start - 1) xs
trackFloor start (x :: xs) = trackFloor start xs
```
This one is slightly more complicated, ultimately very similar to the above, but with two accumulators, one for the position in the input string in addition to the one for the current floor.
This one is slightly more complicated, ultimately very similar to the above, but
with two accumulators, one for the position in the input string in addition to
the one for the current floor.
```idris
findBasement : (position : Nat) -> (currentFloor : Integer) -> (xs : List Char)
@ -48,7 +53,8 @@ Both this parts are simple application of one of our solver functions
### Part 1
Very uneventful, the only thing novel here is pulling the input out of the `ReaderL "input" String`, which will become very boring very quickly.
Very uneventful, the only thing novel here is pulling the input out of the
`ReaderL "input" String`, which will become very boring very quickly.
```idris
part1 : Eff (PartEff String) (Integer, ())
@ -60,7 +66,8 @@ part1 = do
### Part 2
We have to be careful to start the position accumulator at 1, since the problem specifies that the input string is 1-index.
We have to be careful to start the position accumulator at 1, since the problem
specifies that the input string is 1-index.
```idris
part2 : () -> Eff (PartEff String) Nat

27
src/Years/Y2015/Day2.md
View file

@ -32,7 +32,9 @@ record Box where
### Box methods
`.area` provides the surface area of the box, `.slack` provides the surface area of the smallest face, `.ribbon` provides the smallest perimeter of a face, and `.bow` provides the volume of the box.
`.area` provides the surface area of the box, `.slack` provides the surface area
of the smallest face, `.ribbon` provides the smallest perimeter of a face, and
`.bow` provides the volume of the box.
Names are as described in the problem
@ -53,14 +55,16 @@ Names are as described in the problem
(.bow) (MkBox length width height) = length * width * height
```
Provide the total amount of ribbon needed, by adding the ribbon (smallest perimeter) and the bow (volume) values together.
Provide the total amount of ribbon needed, by adding the ribbon (smallest
perimeter) and the bow (volume) values together.
```idris
totalRibbon : Box -> Integer
totalRibbon x = x.ribbon + x.bow
```
Provide the total amount of paper needed by adding the surface area and the slack (smallest side surface area) together.
Provide the total amount of paper needed by adding the surface area and the
slack (smallest side surface area) together.
```idris
paperNeeded : Box -> Integer
@ -77,14 +81,17 @@ parseBox : Has (Except String) fs =>
parseBox str = do
```
First, we split the string into 3 parts by pattern matching on the result of `split`, using `pure` to lift the computation into the effect, and throwing an error if the pattern match fails.
First, we split the string into 3 parts by pattern matching on the result of
`split`, using `pure` to lift the computation into the effect, and throwing an
error if the pattern match fails.
```idris
l ::: [w, h] <- pure $ split (== 'x') str
| xs => throw "Box did not have exactly 3 components: \{show xs}"
```
Then try to parse each of the three integers, throwing an error if parsing fails, then construct and return our box.
Then try to parse each of the three integers, throwing an error if parsing
fails, then construct and return our box.
```idris
length <- note "Failed parsing length: \{show l}" $ parsePositive l
@ -97,9 +104,11 @@ Then try to parse each of the three integers, throwing an error if parsing fails
### Part 1
Split the input into lines, effectfully traverse our box parser over the resulting list of lines, then sum the amounts of paper needed for each box.
Split the input into lines, effectfully traverse our box parser over the
resulting list of lines, then sum the amounts of paper needed for each box.
We return the list of parsed boxes as the context here to avoid needing to parse again in part 2
We return the list of parsed boxes as the context here to avoid needing to parse
again in part 2
```idris
part1 : Eff (PartEff String) (Integer, List Box)
@ -112,7 +121,9 @@ part1 = do
### Part 2
Much the same as part 1, except with the amount of ribbon needed instead of the amount of paper, and without the parsing, since we received the already parsed list of boxes from part 1 as our context value.
Much the same as part 1, except with the amount of ribbon needed instead of the
amount of paper, and without the parsing, since we received the already parsed
list of boxes from part 1 as our context value.
```idris
part2 : (boxes : List Box) -> Eff (PartEff String) Integer

51
src/Years/Y2015/Day3.md
View file

@ -1,6 +1,7 @@
# Year 2015 Day 3
This day provides a gentle introduction to `mutual` blocks and mutually recursive functions.
This day provides a gentle introduction to `mutual` blocks and mutually
recursive functions.
<!-- idris
module Years.Y2015.Day3
@ -23,13 +24,16 @@ import Util
## Parsing and data structures
We'll do parsing a little more properly this time, turning the input into a list of movement commands
We'll do parsing a little more properly this time, turning the input into a list
of movement commands
```idris
data Movement = North | East | South | West
```
We need an effectful operation to parse a single char into a movement. We'll pattern match on the char, and include a catch-all case that throws an error in the event of an invalid char
We need an effectful operation to parse a single char into a movement. We'll
pattern match on the char, and include a catch-all case that throws an error in
the event of an invalid char
```idris
parseMovement : Has (Except String) fs => (x : Char) -> Eff fs Movement
@ -40,7 +44,9 @@ parseMovement '<' = pure West
parseMovement x = throw "Invalid Movement: \{show x}"
```
We also need to be able to translate a `Movement` into a vector of length one pointing in the given direction in coordinate space. Somewhat arbitrarily, we chose 'North' to be positive x and 'East' to be positive y.
We also need to be able to translate a `Movement` into a vector of length one
pointing in the given direction in coordinate space. Somewhat arbitrarily, we
chose 'North' to be positive x and 'East' to be positive y.
```idris
vector : Movement -> (Integer, Integer)
@ -54,11 +60,17 @@ vector West = (0, -1)
### Visited houses
This is a pretty simple task, we are just applying the movements to our current position, and adding our current position to the set of visited locations, so we'll handle this with a normal tail recursive function.
This is a pretty simple task, we are just applying the movements to our current
position, and adding our current position to the set of visited locations, so
we'll handle this with a normal tail recursive function.
To keep the api nice, we wont ask for the set or the starting location in the top-level function, and instead have the top level function initialize the set and location before passing control to the inner tail-recursive variant.
To keep the api nice, we wont ask for the set or the starting location in the
top-level function, and instead have the top level function initialize the set
and location before passing control to the inner tail-recursive variant.
Because the starting location gets a present, we'll add our location to the set before performing the movement, so we will need to add our final location to the set in the recursive base case.
Because the starting location gets a present, we'll add our location to the set
before performing the movement, so we will need to add our final location to the
set in the recursive base case.
```idris
visitedLocations : List Movement -> SortedSet (Integer, Integer)
@ -73,13 +85,26 @@ visitedLocations xs = visitor xs empty (0, 0)
### Robo Santa
This one gets a bit more interesting, we'll adopt the same tail recursive approach, but instead use a `mutual` block and two mutually recursive functions to handle the alternation between santa and robo santa. The `visitSanta` function will pass control to `visitRobo` after executing its movement, and vise versa.
This one gets a bit more interesting, we'll adopt the same tail recursive
approach, but instead use a `mutual` block and two mutually recursive functions
to handle the alternation between santa and robo santa. The `visitSanta`
function will pass control to `visitRobo` after executing its movement, and vise
versa.
We'll want to insert both present deliverer's locations in the recursive base case, this may result in a duplicate location, but that's okay because `SortedSet` will only hold at most one of each item inserted into it.
We'll want to insert both present deliverer's locations in the recursive base
case, this may result in a duplicate location, but that's okay because
`SortedSet` will only hold at most one of each item inserted into it.
In idris, there is a general requirement that values be defined before their use, a common feature of dependently typed languages, resulting from the fact that just having the type signature of a function/value alone is not always enough to perform type checking, as functions can appear as part of types, requiring evaluation of the function and making automatic dependency analysis effectively impossible.
In idris, there is a general requirement that values be defined before their
use, a common feature of dependently typed languages, resulting from the fact
that just having the type signature of a function/value alone is not always
enough to perform type checking, as functions can appear as part of types,
requiring evaluation of the function and making automatic dependency analysis
effectively impossible.
Inside a `mutual` block, elaboration behaves differently, elaborating types first and then values in separate passes. This restricts what you can do a little, but enables mutually recursive functions.
Inside a `mutual` block, elaboration behaves differently, elaborating types
first and then values in separate passes. This restricts what you can do a
little, but enables mutually recursive functions.
```idris
visitedLocations' : List Movement -> SortedSet (Integer, Integer)
@ -103,7 +128,9 @@ visitedLocations' xs = visitSanta xs empty (0, 0) (0, 0)
### Part 1
Similar to the previous day, we get our input, unpack it, and traverse our effectful movement parsing function over it, before feeding that into our solving function.
Similar to the previous day, we get our input, unpack it, and traverse our
effectful movement parsing function over it, before feeding that into our
solving function.
```idris
part1 : Eff (PartEff String) (Nat, List Movement)

80
src/Years/Y2015/Day4.md
View file

@ -1,6 +1,7 @@
# Year 2015 Day 4
This day introduces us to a little bit of FFI, linking to openssl to use it's `MD5` functionality.
This day introduces us to a little bit of FFI, linking to openssl to use it's
`MD5` functionality.
<!-- idris
module Years.Y2015.Day4
@ -19,15 +20,22 @@ import Prim.Array
## FFI
We will be using openssl's `MD5` function to do the hashing, so we will need to provide a couple of foreign function definitions.
We will be using openssl's `MD5` function to do the hashing, so we will need to
provide a couple of foreign function definitions.
First, we'll provide one for the C standard library's `strlen`. We could get this value from within idris, but we'll do it through FFI to flesh out the example a bit more.
First, we'll provide one for the C standard library's `strlen`. We could get
this value from within idris, but we'll do it through FFI to flesh out the
example a bit more.
The format of the specifier after `%foreign` is "language:function name,library name". Since `strlen` is the c standard library, we use `libc` as the library name.
The format of the specifier after `%foreign` is "language:function name,library
name". Since `strlen` is the c standard library, we use `libc` as the library
name.
Idris will automatically convert primitive types like `String`s and `Int`s to their C equivalents at the FFI boundary.
Idris will automatically convert primitive types like `String`s and `Int`s to
their C equivalents at the FFI boundary.
`PrimIO` is a special, basic type of IO action based on linear types, we won't be getting into the specifics right now.
`PrimIO` is a special, basic type of IO action based on linear types, we won't
be getting into the specifics right now.
By convention, primitive FFI function names start with `prim__` in idris.
@ -36,9 +44,12 @@ By convention, primitive FFI function names start with `prim__` in idris.
prim__strlen : String -> PrimIO Int
```
Now we need one for the `MD5` function from openssl, the openssl objectfile calls itself `libcrypto`, so we'll use that as the library name.
Now we need one for the `MD5` function from openssl, the openssl objectfile
calls itself `libcrypto`, so we'll use that as the library name.
The `MD5` function actually returns a pointer to the hash value, but since the 3rd argument is the pointer it expects to write the hash to, we already have that value and we'll ignore it by having our `prim__md5` return unit.
The `MD5` function actually returns a pointer to the hash value, but since the
3rd argument is the pointer it expects to write the hash to, we already have
that value and we'll ignore it by having our `prim__md5` return unit.
The second argument is the length of the input string in bytes.
@ -49,13 +60,23 @@ prim__md5 : String -> Int -> Ptr Bits8 -> PrimIO ()
Now we glue these parts together in our higher level `md5'` function.
We use `malloc` from `System.FFI` to allocate a buffer for `prim__md5` to write to. This returns an `AnyPtr`, when we need a `Ptr Bits8`, so we'll need to cast it, using `prim__castPtr` from the prelude.
We use `malloc` from `System.FFI` to allocate a buffer for `prim__md5` to write
to. This returns an `AnyPtr`, when we need a `Ptr Bits8`, so we'll need to cast
it, using `prim__castPtr` from the prelude.
We then use our `prim__strlen` function to get the length of our input string from within C, using `primIO` from the prelude to "lift" the resulting `PrimIO Int` into our `io` context.
We then use our `prim__strlen` function to get the length of our input string
from within C, using `primIO` from the prelude to "lift" the resulting
`PrimIO Int` into our `io` context.
We then feed the string, the calculated length, and our casted buffer into our `prim__md5` function, then use `prim__getArrayBits8` from the [c-ffi](https://github.com/joelberkeley/c-ffi/) library to extract each of the bytes, passing them into a pure idris helper function to convert into hex representation.
We then feed the string, the calculated length, and our casted buffer into our
`prim__md5` function, then use `prim__getArrayBits8` from the
[c-ffi](https://github.com/joelberkeley/c-ffi/) library to extract each of the
bytes, passing them into a pure idris helper function to convert into hex
representation.
Since we are working with C FFI and performing a little bit of manual memory management here, we must remember to `free` our pointer, and then we can splice together our output string and return.
Since we are working with C FFI and performing a little bit of manual memory
management here, we must remember to `free` our pointer, and then we can splice
together our output string and return.
```idris
md5' : HasIO io => String -> io String
@ -77,21 +98,38 @@ md5' str = do
pack [hexDigit (n `shiftR` 4), hexDigit (n .&. 0xF)]
```
Now, because foreign functions return a `PrimIO` by default, our `md'` still requires some sort of `HasIO` (like IO). This is undesirable here, after all, MD5 is a hash function, so it really _ought_ to behave like a pure function. We know from taking a careful look at what FFI functions we are invoking that we aren't altering any global state.
Now, because foreign functions return a `PrimIO` by default, our `md'` still
requires some sort of `HasIO` (like IO). This is undesirable here, after all,
MD5 is a hash function, so it really _ought_ to behave like a pure function. We
know from taking a careful look at what FFI functions we are invoking that we
aren't altering any global state.
Idris has an escape hatch for these types of situations, `unsafePerformIO`. This function is, as the name suggests, _quite_ unsafe, so it shouldn't be used if you don't fully understand the implications, and only sparingly at that, but doing FFI to C is an intrinsically unsafe operation, so it's morally okay to use here, as long as we are careful to not violate referential transparency or type safety. Haskell programmers should note that `unsafePerformIO` is _much_ easier to use correctly in Idris, largely as a result of Idris being strict by default.
Idris has an escape hatch for these types of situations, `unsafePerformIO`. This
function is, as the name suggests, _quite_ unsafe, so it shouldn't be used if
you don't fully understand the implications, and only sparingly at that, but
doing FFI to C is an intrinsically unsafe operation, so it's morally okay to use
here, as long as we are careful to not violate referential transparency or type
safety. Haskell programmers should note that `unsafePerformIO` is _much_ easier
to use correctly in Idris, largely as a result of Idris being strict by default.
Finally, we'll construct our top level `md5` function, wrapping `md5'` in `unsafePerformIO`
Finally, we'll construct our top level `md5` function, wrapping `md5'` in
`unsafePerformIO`
```idris
md5 : String -> String
md5 str = unsafePerformIO $ md5' str
```
## Solver functions
### Count the leading zeros in a string
There is a more clever way to do this making use of a "view" strings have for interacting with them as if they were lazy lists, but we've already covered so much here that we'll save that one for another time and just do it the straight forward way, having a top level function that accepts a string, turns it into a list of chars, and then pass it into a tail recursive helper function to actually count the zeros.
There is a more clever way to do this making use of a "view" strings have for
interacting with them as if they were lazy lists, but we've already covered so
much here that we'll save that one for another time and just do it the straight
forward way, having a top level function that accepts a string, turns it into a
list of chars, and then pass it into a tail recursive helper function to
actually count the zeros.
```idris
countZeros : String -> Nat
@ -116,7 +154,10 @@ checkZeros key number =
### Find the first input with a specific number of zeros
Search numbers starting at the provided seed and counting up in a tail recursive helper function. This function is going to be effectively impossible to prove totality for, so we have removed our normal `%default total` annotation for this file
Search numbers starting at the provided seed and counting up in a tail recursive
helper function. This function is going to be effectively impossible to prove
totality for, so we have removed our normal `%default total` annotation for this
file
```idris
findFirst : (zeros : Nat) -> (key : String) -> (seed : Nat) -> Nat
@ -130,7 +171,10 @@ findFirst zeros key current =
### Part 1
Pass the input into our `findFirst` function and use the result as both our output and context value. Since part2 is searching for a longer run of 0s than part 1, numbers already checked by part 1 can not possibly be valid solutions for part 2, so we can skip them in part 2.
Pass the input into our `findFirst` function and use the result as both our
output and context value. Since part2 is searching for a longer run of 0s than
part 1, numbers already checked by part 1 can not possibly be valid solutions
for part 2, so we can skip them in part 2.
```idris
part1 : Eff (PartEff String) (Nat, Nat)

72
src/Years/Y2015/Day5.md
View file

@ -1,6 +1,10 @@
# 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.
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.
<!-- idris
module Years.Y2015.Day5
@ -31,19 +35,39 @@ vowels : List Char
vowels = ['a', 'e', 'i', 'o', 'u']
```
Now define a function to check if a string contains a minimum number of vowels. Here we make use of the `with` rule and the `AsList` view over strings.
Now define a function to check if a string contains a minimum number of vowels.
Here we make use of the `with` rule and the `AsList` view over strings.
The `with` rule provides dependently typed pattern matching, allowing us to make use of the fact that the form of some of the arguments can be determined by the values of the others.
The `with` rule provides dependently typed pattern matching, allowing us to make
use of the fact that the form of some of the arguments can be determined by the
values of the others.
The `AsList` view associates a `String` with a lazy list of the characters in the string by providing incremental proofs that the `String` decomposes into the lazy list. An `AsList` of value `Nil`/`[]` proves that the associated string is empty, and an `AsList` of value `c :: xs` proves that the associated string can be generated by `strCons`ing the character `c` onto the rest of the string as captured by the `AsList` in `xs`.
The `AsList` view associates a `String` with a lazy list of the characters in
the string by providing incremental proofs that the `String` decomposes into the
lazy list. An `AsList` of value `Nil`/`[]` proves that the associated string is
empty, and an `AsList` of value `c :: xs` proves that the associated string can
be generated by `strCons`ing the character `c` onto the rest of the string as
captured by the `AsList` in `xs`.
We use the `asList` function, which generates the `AsList` view for the provided string, as the argument to the `with` block. Functions like this that produce views for a value are refereed to as "covering functions". In general, views are dependently typed constructs whose value provides insight into the structure of another value.
We use the `asList` function, which generates the `AsList` view for the provided
string, as the argument to the `with` block. Functions like this that produce
views for a value are refereed to as "covering functions". In general, views are
dependently typed constructs whose value provides insight into the structure of
another value.
We implement this function by keeping a counter of the number of vowels we still need to see to accept the string, returning true when that counter equals zero, or false if we hit the end of the string (when the string argument is empty and the associated `AsList` is `Nil`) while the counter is still non-zero.
We implement this function by keeping a counter of the number of vowels we still
need to see to accept the string, returning true when that counter equals zero,
or false if we hit the end of the string (when the string argument is empty and
the associated `AsList` is `Nil`) while the counter is still non-zero.
If the counter is non-zero and the string is non-empty, we check the current `c` character to see if it is a vowel, by checking to see if our `vowels` list contains it, then recurse, decrementing the counter if it was a vowel, and leaving the counter unchanged if it wasn't.
If the counter is non-zero and the string is non-empty, we check the current `c`
character to see if it is a vowel, by checking to see if our `vowels` list
contains it, then recurse, decrementing the counter if it was a vowel, and
leaving the counter unchanged if it wasn't.
The use of `| xs` after the recursive call to `containsVowels` tells Idris to recurse directly to the `with` block, allowing it to reuse the `AsList` value in `xs` without having to generate the `AsList` view again.
The use of `| xs` after the recursive call to `containsVowels` tells Idris to
recurse directly to the `with` block, allowing it to reuse the `AsList` value in
`xs` without having to generate the `AsList` view again.
```idris
containsVowels : (count : Nat) -> String -> Bool
@ -58,11 +82,18 @@ containsVowels count str with (asList str)
### At least one letter appears twice in a row
For this one, since we need to inspect two letters at a time, we break out a nested `with` block, with the tail of the `AsList` as the argument of the block, to also pattern match on the next character of the string.
For this one, since we need to inspect two letters at a time, we break out a
nested `with` block, with the tail of the `AsList` as the argument of the block,
to also pattern match on the next character of the string.
Since the `AsList` view is lazy, we need to use `force` in the inner with block to force the evaluation of the next component of the view, this is due to a [bug in the compiler](https://github.com/idris-lang/Idris2/issues/3461).
Since the `AsList` view is lazy, we need to use `force` in the inner with block
to force the evaluation of the next component of the view, this is due to a
[bug in the compiler](https://github.com/idris-lang/Idris2/issues/3461).
The logic here is pretty simple, if we hit the empty string or get down to one character, return `False`, if we have two characters available, compare them, returning `True` if they match, and recursing to the outer with block, only consuming one of the two characters, if they don't match.
The logic here is pretty simple, if we hit the empty string or get down to one
character, return `False`, if we have two characters available, compare them,
returning `True` if they match, and recursing to the outer with block, only
consuming one of the two characters, if they don't match.
```idris
doubleLetter : String -> Bool
@ -85,7 +116,10 @@ disallowedSubstrs : List String
disallowedSubstrs = ["ab", "cd", "pq", "xy"]
```
Idris's standard library does not currently define a function to check if a string is a substring of another, so we instead use our own `isSubstr` function, defined via use of the `AsList` view, from our [Util](../../Util.md#issubstr) module.
Idris's standard library does not currently define a function to check if a
string is a substring of another, so we instead use our own `isSubstr` function,
defined via use of the `AsList` view, from our [Util](../../Util.md#issubstr)
module.
```idris
noDisallowed : String -> Bool
@ -95,7 +129,8 @@ noDisallowed str =
### isNice
Combine all three of our above functions together to check if a string is a "nice" string
Combine all three of our above functions together to check if a string is a
"nice" string
```idris
isNice : String -> Bool
@ -106,7 +141,9 @@ isNice str = containsVowels 3 str && doubleLetter str && noDisallowed str
### Pair of letters that appears twice
Use a similar approach to `doubleLetter` above, but instead of comparing the two chars for equality, pack them into a string and check if they are a substring of the rest of the string.
Use a similar approach to `doubleLetter` above, but instead of comparing the two
chars for equality, pack them into a string and check if they are a substring of
the rest of the string.
```idris
pairTwice : String -> Bool
@ -122,7 +159,9 @@ pairTwice str with (asList str)
### Letter that repeats after one letter
More of the same, but this one gets extra fun because we are matching 3 letters at a time. This would be a lot nicer if we could get away without nesting the `with` blocks, but due to the aformentioned compiler bug, we need the nesting.
More of the same, but this one gets extra fun because we are matching 3 letters
at a time. This would be a lot nicer if we could get away without nesting the
`with` blocks, but due to the aformentioned compiler bug, we need the nesting.
```idris
letterRepeatGap : String -> Bool
@ -151,7 +190,8 @@ isNice' str = pairTwice str && letterRepeatGap str
### Part 1
Split our input up into a list of its component strings, and then count how many satisfy the "nice" criteria.
Split our input up into a list of its component strings, and then count how many
satisfy the "nice" criteria.
```idris
part1 : Eff (PartEff String) (Nat, ())

48
src/Years/Y2015/Day6.md
View file

@ -27,7 +27,9 @@ import Data.IORef
### Grid structure
Since this is our first 2d grid problem, we'll keep it simple and use a `Vect` of `Vect`s to store our problem state, we'll revisit a more complicated but more efficient structure for storing a 2d `Grid` in a later problem.
Since this is our first 2d grid problem, we'll keep it simple and use a `Vect`
of `Vect`s to store our problem state, we'll revisit a more complicated but more
efficient structure for storing a 2d `Grid` in a later problem.
This alias adds 1 to each of its arguments to ensure non-emptyness.
@ -36,7 +38,8 @@ Grid : (rows, cols : Nat) -> Type -> Type
Grid rows cols e = Vect (S rows) (Vect (S cols) e)
```
We also provide a type alias for the coordinates in this grid, a simple pair of `Fin`s.
We also provide a type alias for the coordinates in this grid, a simple pair of
`Fin`s.
```idris
Coord : (rows, cols : Nat) -> Type
@ -93,7 +96,9 @@ Show (Range rows cols) where
Helper function to extract a range of values from our Grid.
First extracts the range of rows this `Range` touches, then maps a an extractor for the range of columns it touches across them, before lazily concatenating the resulting lists.
First extracts the range of rows this `Range` touches, then maps a an extractor
for the range of columns it touches across them, before lazily concatenating the
resulting lists.
```idris
extractRange : Range rows cols -> Grid rows cols e -> LazyList e
@ -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.
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

36
src/Years/Y2015/Day7.md
View file

@ -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
module Years.Y2015.Day7
@ -32,7 +39,8 @@ import Decidable.Equality
### Problem structure
Define type aliases for wires and literals, and specify that an input can be either a literal or a wire.
Define type aliases for wires and literals, and specify that an input can be
either a literal or a wire.
```idris
Wire : Type
@ -128,9 +136,16 @@ parseGate str = do
_ => throw "Invalid Gate: \{str}"
```
Break the input into lines, traverse `parseGate` over the lines, and collect the results into our circut DMap.
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.
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 =>
@ -150,7 +165,8 @@ parseGates input = do
## Solver Functions
Recursively solve for the value on a wire, keeping a cache of already solved wires
Recursively solve for the value on a wire, keeping a cache of already solved
wires
```idris
covering
@ -197,7 +213,10 @@ 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 well as the output signal from wire 'a' 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
@ -214,7 +233,8 @@ part1 = do
### 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.
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