223 lines
7 KiB
Markdown
223 lines
7 KiB
Markdown
# 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 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
|
|
|
|
import Control.Eff
|
|
import Structures.Dependent.FreshList
|
|
|
|
import public Util.Eff
|
|
|
|
%default total
|
|
```
|
|
|
|
# Effectful Parts
|
|
|
|
The solution to each part of a day is run as an effectful computation, and as
|
|
the effect stack is meant to be the same across both parts, only varying in the
|
|
type of the error value for the `Except` effect, we construct a type level
|
|
function to have a single source of truth. The `err` type can be any type with a
|
|
`Show` implementation, but that constraint will be tacked on in the next step.
|
|
|
|
The `Logger` effect is provided for logging, and a `Reader` effect is provided
|
|
to pass in the input, 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 will 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
|
|
||| different error types, so we calucate it here
|
|
public export
|
|
PartEff : (err : Type) -> List (Type -> Type)
|
|
PartEff err =
|
|
[IO, Except err, Logger, ReaderL "input" String]
|
|
```
|
|
|
|
# The `Day` Record
|
|
|
|
The `Day` type groups together an effectful `part1` computation, an optional
|
|
effectful `part2` computation, and the day number, with some type wrangling to
|
|
get the type system out of our way.
|
|
|
|
`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`. This is achieved through
|
|
the erased `ctx` type, which is totally opaque to the runner. The code in `Main`
|
|
will provide the value of the `ctx` type produced as part of the output of
|
|
`part1` and as the input of `part2`.
|
|
|
|
```idris
|
|
||| Model solving a single day
|
|
public export
|
|
record Day where
|
|
constructor MkDay
|
|
day : Nat
|
|
{0 out1, out2, err1, err2 : Type}
|
|
{auto showOut1 : Show out1}
|
|
{auto showOut2 : Show out2}
|
|
{auto showErr1 : Show err1}
|
|
{auto showErr2 : Show err2}
|
|
part1 : Eff (PartEff err1) (out1, ctx)
|
|
part2 : Maybe (ctx -> Eff (PartEff err2) out2)
|
|
%name Day day, day2, day3
|
|
```
|
|
|
|
## 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. We provide a
|
|
pair of constructors for the case where there is only a `part1`, as well as one
|
|
for when there is a `part1` and a `part2`.
|
|
|
|
```idris
|
|
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 `()`.
|
|
|
|
```idris
|
|
||| Constructor for a day with only part one ready to run
|
|
public export
|
|
First : Show err => Show out =>
|
|
(day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
|
|
-> Day
|
|
First day part1 =
|
|
MkDay day part1 Nothing {out2 = ()} {err2 = ()}
|
|
```
|
|
|
|
### Both
|
|
|
|
The `Both` constructor does less heavy lifting, the only thing it needs to do is
|
|
wrap `part2` in a `Just`.
|
|
|
|
```idris
|
|
||| Constructor for a day with both parts ready to run
|
|
public export
|
|
Both : Show o1 => Show o2 => Show e1 => Show e2 =>
|
|
(day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
|
|
(part2 :ctx' -> Eff (PartEff e2) o2)
|
|
-> Day
|
|
Both day part1 part2 =
|
|
MkDay day part1 (Just part2)
|
|
```
|
|
|
|
## Freshness
|
|
|
|
We will be using a _Fresh List_ from the
|
|
[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build our
|
|
API defensively against duplicate days and cosmetically annoying out of order
|
|
day registration. A Fresh List structurally only allows you to prepend/cons an
|
|
element onto it when it satisfies some _freshness criteria_ relative to the
|
|
elements already contained in the list.
|
|
|
|
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 of `Day`s is sorted in ascending order and that no two `Day`s have
|
|
the same day number.
|
|
|
|
```idris
|
|
||| Freshness criteria for days
|
|
|||
|
|
||| A day is fresh compared to another if the day number of the former day is
|
|
||| strictly less than the day number of the latter day
|
|
|||
|
|
||| This ensures that the days list is always in incrimenting sorted order
|
|
||| (since we are consing to the front of the list) with no duplicate days
|
|
public export
|
|
FreshDay : Day -> Day -> Bool
|
|
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, also containing the year number for this collection.
|
|
|
|
```idris
|
|
||| Collect all the days in a given year
|
|
public export
|
|
record Year where
|
|
constructor MkYear
|
|
year : Nat
|
|
days : FreshList FreshDay Day
|
|
%name Year year, year2, year3
|
|
```
|
|
|
|
## 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`.
|
|
|
|
```idris
|
|
||| Freshness criteria for years
|
|
|||
|
|
||| A year is fresh compared to another if the year number of the former year is
|
|
||| strictly less than the year number of the latter year
|
|
|||
|
|
||| This ensures that the years list is always in incrimenting sorted order
|
|
||| (since we are consing to the front of the list) with no duplicate years
|
|
public export
|
|
FreshYear : Year -> Year -> Bool
|
|
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.
|
|
|
|
```idris
|
|
||| Collect all years
|
|
public export
|
|
record Advent where
|
|
constructor MkAdvent
|
|
years : FreshList FreshYear Year
|
|
%name Advent advent, advent2, advent3
|
|
```
|
|
|
|
## Methods
|
|
|
|
```idris
|
|
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.
|
|
|
|
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
|
|
export
|
|
locate : (year, day : Nat) -> Advent -> Maybe Day
|
|
locate year day advent = do
|
|
year <- find (\x => x.year == year) advent.years
|
|
find (\x => x.day == day) year.days
|
|
```
|