Compare commits
8 commits
13b05ceb86
...
c47f522c50
| Author | SHA1 | Date | |
|---|---|---|---|
| c47f522c50 | |||
| 7e05cc1e8b | |||
| f7afecb550 | |||
| 8162210b21 | |||
| 76fcb6c34b | |||
| 407149dd4a | |||
| 9489721e29 | |||
| d6330fec9b |
18 changed files with 374 additions and 431 deletions
68
README.md
68
README.md
|
|
@ -1,10 +1,25 @@
|
|||
# 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.
|
||||
of one single Idris application, and thoroughly document the results as literate
|
||||
Idris files.
|
||||
|
||||
# Index of non-day modules
|
||||
## Authors Note
|
||||
|
||||
The solutions contained in this project are intended to be read in sequential
|
||||
order, though can reasonably be read in any order if you have a good level of
|
||||
familiarity with more advanced functional programming topics.
|
||||
|
||||
The solutions will involve progressively more advanced topics as day and year
|
||||
number increase, though I try not to introduce too much within the scope of any
|
||||
one day.
|
||||
|
||||
Suggestions and other feedback are highly welcome, please reach out to me via
|
||||
any platform you know me on, or send an email to the
|
||||
[~thatonelutenist/public-inbox](https://lists.sr.ht/~thatonelutenist/public-inbox)
|
||||
mailing list on source hut.
|
||||
|
||||
## Index of non-day modules
|
||||
|
||||
- [Runner](src/Runner.md)
|
||||
|
||||
|
|
@ -26,16 +41,61 @@ solution.
|
|||
Extend the functionality of the effects included in the
|
||||
[eff](https://github.com/stefan-hoeck/idris2-eff/) library
|
||||
|
||||
# Index of years and days
|
||||
- [Util.Digits](src/Util/Digits.md)
|
||||
|
||||
Provide views that enable recursively pattern matching numbers as lists of
|
||||
digits, in both ascending and descending order of significance.
|
||||
|
||||
## Index of years and days
|
||||
|
||||
- 2015
|
||||
- [Day 1](src/Years/Y2015/Day1.md)
|
||||
|
||||
Warm up problem, breaks in our new runner and not much else interesting.
|
||||
|
||||
- [Day 2](src/Years/Y2015/Day2.md)
|
||||
|
||||
An early hint of effectful parsing.
|
||||
|
||||
- [Day 3](src/Years/Y2015/Day3.md)
|
||||
|
||||
Peculiarities of writing mutually recursive functions in dependently typed
|
||||
languages.
|
||||
|
||||
- [Day 4](src/Years/Y2015/Day4.md)
|
||||
|
||||
Basic FFI to openssl to steal its MD5 function for Idris's use.
|
||||
|
||||
- [Day 5](src/Years/Y2015/Day5.md)
|
||||
|
||||
First introduction to views and dependent pattern matching[^1].
|
||||
|
||||
- [Day 6](src/Years/Y2015/Day6.md)
|
||||
|
||||
Naive approach to handling the first 2d grid problem.
|
||||
|
||||
- [Day 7](src/Years/Y2015/Day7.md)
|
||||
|
||||
Introduces dependent maps and indexed type families.
|
||||
|
||||
- [Day 8](src/Years/Y2015/Day8.md)
|
||||
|
||||
Proper effectful parsers and non-determinism in effect stacks.
|
||||
|
||||
- [Day 9](src/Years/Y2015/Day9.md)
|
||||
|
||||
Naive approach to handling the first graph traversal problem.
|
||||
|
||||
- [Day 10](src/Years/Y2015/Day10.md)
|
||||
|
||||
Introduce our `Digits`, dependent pattern matching on integers as lists of
|
||||
digits.
|
||||
|
||||
- [Day 11](src/Years/Y2015/Day11.md)
|
||||
|
||||
Introduces refinement types
|
||||
|
||||
## References
|
||||
|
||||
[^1]: Idris 2 Manual:
|
||||
[Views and the "with" rule](https://idris2.readthedocs.io/en/latest/tutorial/views.html#views-and-the-with-rule)
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ depends = base
|
|||
, ansi
|
||||
, if-unsolved-implicit
|
||||
, c-ffi
|
||||
, refined
|
||||
|
||||
-- modules to install
|
||||
modules = Runner
|
||||
|
|
|
|||
371
src/Grid.md
371
src/Grid.md
|
|
@ -1,371 +0,0 @@
|
|||
# 2D Grid utilities
|
||||
|
||||
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.
|
||||
|
||||
```idris
|
||||
module Grid
|
||||
|
||||
import Data.Seq.Sized
|
||||
import Data.Fin
|
||||
import Data.Fin.Extra
|
||||
import Data.List.Lazy
|
||||
import Data.Zippable
|
||||
import Data.Vect
|
||||
import Data.String
|
||||
import Decidable.Equality
|
||||
|
||||
%default total
|
||||
```
|
||||
|
||||
## Coordinates
|
||||
|
||||
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
|
||||
|
||||
```idris
|
||||
public export
|
||||
Coord : (rows, cols : Nat) -> Type
|
||||
Coord rows cols = (Fin (S rows), Fin (S cols))
|
||||
```
|
||||
|
||||
### Coordinate utility functions
|
||||
|
||||
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.
|
||||
|
||||
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.
|
||||
|
||||
```idris
|
||||
export
|
||||
allCords : {rows, cols : Nat} -> LazyList (Coord rows cols)
|
||||
allCords = concat . map row $ all
|
||||
where
|
||||
all : {n : Nat} -> LazyList (Fin (S n))
|
||||
all = FZ :: all' FZ
|
||||
where
|
||||
all' : {n : Nat} -> (acc : Fin (S n)) -> LazyList (Fin (S n))
|
||||
all' acc =
|
||||
if acc < last
|
||||
then finS acc :: all' (assert_smaller acc (finS acc))
|
||||
else []
|
||||
row : Fin (S rows) -> LazyList (Coord rows cols)
|
||||
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.
|
||||
|
||||
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
|
||||
step : {rows, cols : Nat} -> (input : Coord rows cols) -> (direction : (Integer, Integer))
|
||||
-> Maybe (Coord rows cols)
|
||||
step (row, col) (d_row, d_col) = do
|
||||
let (row, col) = (finToInteger row, finToInteger col)
|
||||
row <- integerToFin (row + d_row) (S rows)
|
||||
col <- integerToFin (col + d_col) (S cols)
|
||||
pure (row, col)
|
||||
```
|
||||
|
||||
## Grid
|
||||
|
||||
A grid is a `Seq` of `Seq`s with the given size bounds.
|
||||
|
||||
The inner `Seq`s are kept opaque to maintain flexability in the implementation
|
||||
|
||||
```idris
|
||||
export
|
||||
record Grid (rows, cols : Nat) (e : Type) where
|
||||
constructor MkGrid
|
||||
grid : Seq (S rows) (Seq (S cols) e)
|
||||
%name Grid grid, grid2, grid3
|
||||
```
|
||||
|
||||
### Constructors
|
||||
|
||||
Construct a `Grid` by filling every slot with identical copies of the provided
|
||||
element
|
||||
|
||||
```idris
|
||||
export
|
||||
replicate : {rows, cols : Nat} -> (seed : e) -> Grid rows cols e
|
||||
replicate seed =
|
||||
let row = replicate (S cols) seed
|
||||
grid = replicate (S rows) row
|
||||
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.
|
||||
|
||||
We make heavy use of the `Maybe` monad to keep the code clean here.
|
||||
|
||||
```idris
|
||||
export
|
||||
fromFoldable : Traversable a => Foldable a => Foldable b => a (b e) ->
|
||||
Maybe (rows : Nat ** cols : Nat ** Grid rows cols e)
|
||||
fromFoldable xs = do
|
||||
-- First collect the number of rows from the outer foldable
|
||||
let (S rows) = foldl (\acc, e => acc + 1) 0 xs
|
||||
| _ => Nothing -- Return Nothing if there are no rows
|
||||
-- Get the number of columns in the largest row in the inner foldable
|
||||
let (S cols) = foldl (\acco, eo => max acco (foldl (\acci, ei => acci +1) 0 eo)) 0 xs
|
||||
| _ => Nothing -- Return Nothing if all the rows are empty
|
||||
-- Convert the rows by traversing our foldToSeq function over the outer foldable
|
||||
xs <- traverse (foldToSeq (S cols)) xs
|
||||
-- Reuse our foldToSeq helper function to convert the outer foldable
|
||||
xs <- foldToSeq (S rows) xs
|
||||
-- wrap it up and return
|
||||
pure (rows ** cols ** MkGrid xs)
|
||||
where
|
||||
-- Convert each row to a seq using an intermediate list
|
||||
foldToSeq : Foldable c => (n : Nat) -> c f -> Maybe (Seq n f)
|
||||
foldToSeq n x =
|
||||
let list = toList x
|
||||
-- Check to see if the list is of the correct length, then rewrite the
|
||||
-- output type to match if that's the case, otherwise return Nothing
|
||||
in case decEq (length list) n of
|
||||
Yes Refl => Just $ fromList list
|
||||
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.
|
||||
|
||||
```idris
|
||||
export
|
||||
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
|
||||
|
||||
```idris
|
||||
export
|
||||
coordinateGrid : {rows, cols : Nat} -> Grid rows cols (Coord rows cols)
|
||||
coordinateGrid =
|
||||
let row = fromVect $ allFins (S cols)
|
||||
grid = zip (fromVect $ allFins (S rows)) (replicate _ row)
|
||||
grid = map (\(x, xs) => map (x,) xs) grid
|
||||
in MkGrid grid
|
||||
```
|
||||
|
||||
### Accessors and Mutators
|
||||
|
||||
Get the value at a specific index in the grid
|
||||
|
||||
```idris
|
||||
export
|
||||
index : Coord rows cols -> Grid rows cols e -> e
|
||||
index (row, col) grid =
|
||||
index' (index' grid.grid row) col
|
||||
```
|
||||
|
||||
Replace the value at a specific index in the grid
|
||||
|
||||
```idris
|
||||
export
|
||||
replaceAt : Coord rows cols -> e -> Grid rows cols e -> Grid rows cols e
|
||||
replaceAt (row, col) x (MkGrid grid) =
|
||||
let r = index' grid row
|
||||
r = update (finToNat col) x r @{elemSmallerThanBound col}
|
||||
grid = update (finToNat row) r grid @{elemSmallerThanBound row}
|
||||
in MkGrid grid
|
||||
```
|
||||
|
||||
Update the value at a specific index in the grid
|
||||
|
||||
```idris
|
||||
export
|
||||
updateAt : Coord rows cols -> (e -> e) -> Grid rows cols e -> Grid rows cols e
|
||||
updateAt (row, col) f (MkGrid grid) =
|
||||
let r = index' grid row
|
||||
r = adjust f (finToNat col) r @{elemSmallerThanBound col}
|
||||
grid = update (finToNat row) r grid @{elemSmallerThanBound row}
|
||||
in MkGrid grid
|
||||
```
|
||||
|
||||
Lazily provide all the values in the grid as a flat collection
|
||||
|
||||
```idris
|
||||
export
|
||||
flat : {rows, cols : Nat} -> Grid rows cols e -> LazyList e
|
||||
flat (MkGrid grid) =
|
||||
let grid = seqToLazy . map (seqToLazy {n = S cols}) $ grid
|
||||
grid = grid []
|
||||
in foldrLazy (\a, acc => a acc) [] grid
|
||||
where
|
||||
seqToLazy : {n : Nat} -> (seq : Seq n a) -> (rest : LazyList a) -> LazyList a
|
||||
seqToLazy {n = 0} seq rest = rest
|
||||
seqToLazy {n = (S k)} seq rest =
|
||||
let (head, tail) = viewl seq
|
||||
in head :: seqToLazy tail rest
|
||||
```
|
||||
|
||||
### Interface Implementations
|
||||
|
||||
#### Show
|
||||
|
||||
```idris
|
||||
export
|
||||
{rows, cols : Nat} -> Show e => Show (Grid rows cols e) where
|
||||
show (MkGrid grid) =
|
||||
show . toVect . map toVect $ grid
|
||||
```
|
||||
|
||||
#### Eq/Ord
|
||||
|
||||
```idris
|
||||
export
|
||||
Eq e => Eq (Grid rows cols e) where
|
||||
(MkGrid grid_x) == (MkGrid grid_y) = grid_x == grid_y
|
||||
|
||||
export
|
||||
Ord e => Ord (Grid rows cols e) where
|
||||
compare (MkGrid grid_x) (MkGrid grid_y) = compare grid_x grid_y
|
||||
```
|
||||
|
||||
#### Functor
|
||||
|
||||
```idris
|
||||
export
|
||||
Functor (Grid rows cols) where
|
||||
map f (MkGrid grid) =
|
||||
MkGrid . map (map f) $ grid
|
||||
```
|
||||
|
||||
#### Foldable
|
||||
|
||||
Cheeze it a little and use our `flat` function internally here.
|
||||
|
||||
Also, `null` can statically return false, as `Grid` is structurally non-empty
|
||||
|
||||
```idris
|
||||
export
|
||||
{rows, cols : Nat} -> Foldable (Grid rows cols) where
|
||||
foldr f acc grid = foldr f acc (flat grid)
|
||||
foldl f acc grid = foldl f acc (flat grid)
|
||||
null _ = False
|
||||
toList grid = toList (flat grid)
|
||||
```
|
||||
|
||||
#### Applicative
|
||||
|
||||
```idris
|
||||
export
|
||||
{rows, cols : Nat} -> Applicative (Grid rows cols) where
|
||||
pure a = replicate a
|
||||
(MkGrid f) <*> (MkGrid grid) =
|
||||
MkGrid . map (\(a,b) => a <*> b) . zip f $ grid
|
||||
```
|
||||
|
||||
#### Traversable
|
||||
|
||||
```idris
|
||||
export
|
||||
{rows, cols : Nat} -> Traversable (Grid rows cols) where
|
||||
traverse f (MkGrid grid) =
|
||||
map MkGrid . traverse (traverse f) $ grid
|
||||
```
|
||||
|
||||
#### Zippable
|
||||
|
||||
```idris
|
||||
export
|
||||
Zippable (Grid rows cols) where
|
||||
zipWith f (MkGrid grid_x) (MkGrid grid_y) =
|
||||
let xs = zip grid_x grid_y
|
||||
in MkGrid . map (\(a,b) => zipWith f a b) $ xs
|
||||
unzipWith f (MkGrid grid) =
|
||||
let (xs, ys) = unzip . map (unzipWith f) $ grid
|
||||
in (MkGrid xs, MkGrid ys)
|
||||
zipWith3 f (MkGrid as) (MkGrid bs) (MkGrid cs) =
|
||||
let xs = zip3 as bs cs
|
||||
in MkGrid . map (\(a, b, c) => zipWith3 f a b c) $ xs
|
||||
unzipWith3 f (MkGrid grid) =
|
||||
let (a, b, c) = unzip3 . map (unzipWith3 f) $ grid
|
||||
in (MkGrid a, MkGrid b, MkGrid c)
|
||||
```
|
||||
|
||||
### Extra
|
||||
|
||||
Extensions of the above functionality
|
||||
|
||||
#### Indexing
|
||||
|
||||
Convert this grid to one with both the index of the location and the element in
|
||||
each location
|
||||
|
||||
```idris
|
||||
export
|
||||
indexed : {rows, cols : Nat} -> Grid rows cols e -> Grid rows cols (Coord rows cols, e)
|
||||
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)
|
||||
flatIndexed = flat . indexed
|
||||
```
|
||||
|
||||
#### String functionality
|
||||
|
||||
Attempts to convert a string, with newline delimited rows, to a grid of
|
||||
characters
|
||||
|
||||
```idris
|
||||
export
|
||||
stringToGrid : String -> Maybe (rows : Nat ** cols : Nat ** Grid rows cols Char)
|
||||
stringToGrid = fromFoldable . map (unpack . trim) . lines . trim
|
||||
```
|
||||
|
||||
Converts a grid of chars to a string, delimiting the rows with newlines
|
||||
|
||||
```idris
|
||||
export
|
||||
gridToString : Grid rows cols Char -> String
|
||||
gridToString (MkGrid grid) = unlines . toList . map (pack . toList) $ grid
|
||||
```
|
||||
|
||||
#### Conversion
|
||||
|
||||
Convert a grid to a vect of vects
|
||||
|
||||
```idris
|
||||
export
|
||||
toVects : {rows, cols : Nat} -> Grid rows cols e -> Vect (S rows) (Vect (S cols) e)
|
||||
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)
|
||||
toLists (MkGrid grid) = toList . map toList $ grid
|
||||
```
|
||||
|
|
@ -181,8 +181,8 @@ failures doing so.
|
|||
## 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.
|
||||
blackhole the logs. Afterwards, use `logHandler` to introduce the `Logger` into
|
||||
the effects list.
|
||||
|
||||
```idris
|
||||
-- If the verbose flag is set, hook up the logging writer to stderr
|
||||
|
|
@ -259,8 +259,8 @@ a `SolveError`, then print out the result, then return, closing out the program.
|
|||
|
||||
### 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.
|
||||
Makes use of `Logger`'s `handleLoggerIO` function to "lower" logging actions
|
||||
into `IO` within the effect.
|
||||
|
||||
```idris
|
||||
-- Lowers logging into IO within the effect using the given IO function
|
||||
|
|
|
|||
|
|
@ -22,16 +22,15 @@ 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 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.
|
||||
|
||||
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
|
||||
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 may come in handy if a part needs `IO` for performance
|
||||
doing any IO, this will come in handy if a part needs `IO` for performance
|
||||
reasons.
|
||||
|
||||
```idris
|
||||
|
|
@ -46,19 +45,19 @@ 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.
|
||||
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
|
||||
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`.
|
||||
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
|
||||
|
|
@ -80,9 +79,9 @@ record Day where
|
|||
|
||||
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.
|
||||
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
|
||||
|
|
@ -91,8 +90,7 @@ 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.'
|
||||
`part2` with `Nothing` and setting all of `part2`'s type arguments to `()`.
|
||||
|
||||
```idris
|
||||
||| Constructor for a day with only part one ready to run
|
||||
|
|
@ -106,8 +104,8 @@ us.'
|
|||
|
||||
### 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 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
|
||||
|
|
@ -123,16 +121,17 @@ needs to do for us is wrap `part2` in a `Just`.
|
|||
## 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.
|
||||
[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.
|
||||
|
||||
Here, we compare the day numbers of the two `Day`s using the less-than
|
||||
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.
|
||||
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
|
||||
|
|
@ -150,7 +149,7 @@ 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.
|
||||
year, also containing the year number for this collection.
|
||||
|
||||
```idris
|
||||
||| Collect all the days in a given year
|
||||
|
|
@ -166,9 +165,10 @@ record Year where
|
|||
|
||||
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`.
|
||||
`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
|
||||
|
|
@ -186,8 +186,7 @@ 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.
|
||||
`Year` collects a number of days.
|
||||
|
||||
```idris
|
||||
||| Collect all years
|
||||
|
|
|
|||
|
|
@ -22,9 +22,18 @@ import System.File
|
|||
Basic enumeration describing log levels, we define some (hidden) utility
|
||||
functions for working with these.
|
||||
|
||||
The `Other n` log level is restricted to `n` greater than 4, to prevent
|
||||
ambiguity between custom log levels and predefined log levels.
|
||||
|
||||
```idris
|
||||
public export
|
||||
data Level = Err | Warn | Info | Debug | Trace | Other Nat
|
||||
data Level : Type where
|
||||
Err : Level
|
||||
Warn : Level
|
||||
Info : Level
|
||||
Debug : Level
|
||||
Trace : Level
|
||||
Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level
|
||||
```
|
||||
|
||||
<!-- idris
|
||||
|
|
@ -44,7 +53,7 @@ natToLevel 1 = Warn
|
|||
natToLevel 2 = Info
|
||||
natToLevel 3 = Debug
|
||||
natToLevel 4 = Trace
|
||||
natToLevel k = Other k
|
||||
natToLevel (S (S (S (S (S k))))) = Other (5 + k)
|
||||
|
||||
export
|
||||
Eq Level where
|
||||
|
|
@ -130,10 +139,8 @@ 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.
|
||||
Provide a family of effectful actions that emit log messages at the different
|
||||
log levels.
|
||||
|
||||
```idris
|
||||
export
|
||||
|
|
@ -155,6 +162,10 @@ debug x = send $ Log Debug x
|
|||
export
|
||||
trace : Has Logger fs => Lazy String -> Eff fs ()
|
||||
trace x = send $ Log Trace x
|
||||
|
||||
export
|
||||
logAt : Has Logger fs => Level -> Lazy String -> Eff fs ()
|
||||
logAt level x = send $ Log level x
|
||||
```
|
||||
|
||||
## Choose
|
||||
|
|
|
|||
|
|
@ -17,6 +17,7 @@ import Years.Y2015.Day7
|
|||
import Years.Y2015.Day8
|
||||
import Years.Y2015.Day9
|
||||
import Years.Y2015.Day10
|
||||
import Years.Y2015.Day11
|
||||
-->
|
||||
|
||||
# Days
|
||||
|
|
@ -87,6 +88,12 @@ y2015 = MkYear 2015 [
|
|||
, day10
|
||||
```
|
||||
|
||||
## [Day 11](Y2015/Day11.md)
|
||||
|
||||
```idris
|
||||
, day11
|
||||
```
|
||||
|
||||
```idris
|
||||
]
|
||||
```
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 1
|
||||
# [Year 2015 Day 1](https://adventofcode.com/2015/day/1)
|
||||
|
||||
Pretty simple, basic warmup problem, nothing really novel is on display here
|
||||
except the effectful part computations.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 10
|
||||
# [Year 2015 Day 10](https://adventofcode.com/2015/day/10)
|
||||
|
||||
This day doesn't really add anything new, but we will show off our new views for
|
||||
viewing integers as lists of digits.
|
||||
|
|
|
|||
227
src/Years/Y2015/Day11.md
Normal file
227
src/Years/Y2015/Day11.md
Normal file
|
|
@ -0,0 +1,227 @@
|
|||
# [Year 2015 Day 11](https://adventofcode.com/2015/day/11)
|
||||
|
||||
This day provides a gentle introduction to refinement types, types which augment
|
||||
other types with a predicate that must hold for all the values of the refined
|
||||
type, which allow easily defining types as subsets of other types based on some
|
||||
property of the acceptable elements.
|
||||
|
||||
While refinement types are quite easy to implement in Idris, and we easily could
|
||||
implement the one we need for today's task as a throw away data structure just
|
||||
for this module, we will be using the `refined`[^1] library's implementation for
|
||||
the sake of getting on with it.
|
||||
|
||||
<!-- idris
|
||||
module Years.Y2015.Day11
|
||||
|
||||
import Control.Eff
|
||||
|
||||
import Runner
|
||||
-->
|
||||
|
||||
```idris
|
||||
import Data.Vect
|
||||
import Data.String
|
||||
import Data.Refined.Char
|
||||
|
||||
import Util
|
||||
```
|
||||
|
||||
## Data Structures and Parsing
|
||||
|
||||
Provide a predicate which establishes that a char is a lowercase alphabetic
|
||||
character, the only type of character that passwords are allowed to contain. We
|
||||
use the `FromTo` predicate from the `refined`[^1] library to restrict chars to
|
||||
within the range from `a` to `z`.
|
||||
|
||||
This predicate has multiplicity 0, a full discussion of multiplicites and linear
|
||||
types is out of scope for today, but put simply this enforces that a value of
|
||||
this predicate type can be "used" at most 0 times, having the effect of erasing
|
||||
the value at runtime, making this more or less a zero-cost abstraction.
|
||||
|
||||
```idris
|
||||
0 IsPasswordChar : Char -> Type
|
||||
IsPasswordChar = FromTo 'a' 'z'
|
||||
```
|
||||
|
||||
Combine a `Char` with its corresponding `IsPasswordChar` predicate into a
|
||||
combined "refined" type, whose elements are the subset of `Char`s that are
|
||||
lowercase alphabetic characters.
|
||||
|
||||
```idris
|
||||
record PasswordChar where
|
||||
constructor MkPC
|
||||
char : Char
|
||||
{auto 0 prf : IsPasswordChar char}
|
||||
%name PasswordChar pc
|
||||
```
|
||||
|
||||
<!-- idris
|
||||
Show PasswordChar where
|
||||
show (MkPC char) = singleton char
|
||||
|
||||
Eq PasswordChar where
|
||||
x == y = x.char == y.char
|
||||
-->
|
||||
|
||||
A function to fallible convert `Char`s into refined `PasswordChar`s, this will
|
||||
return `Just` if the `Char` satisfies the predicate, and `Nothing` otherwise,
|
||||
aligning with the type-level guarantees of the `PasswordChar` type.
|
||||
|
||||
```idris
|
||||
refineChar : Char -> Maybe PasswordChar
|
||||
refineChar c = map fromSubset $ refine0 c
|
||||
where
|
||||
fromSubset : Subset Char IsPasswordChar -> PasswordChar
|
||||
fromSubset (Element char prf) = MkPC char
|
||||
```
|
||||
|
||||
Convenience function returning `a` as a `PasswordChar`
|
||||
|
||||
```idris
|
||||
lowest : PasswordChar
|
||||
lowest = MkPC 'a'
|
||||
```
|
||||
|
||||
"Increment" a `PasswordChar`, changing it to the next letter (`a` becomes `b`,
|
||||
`b` becomes `c`, so on), returning nothing if we go past `z`, corresponding to a
|
||||
carry.
|
||||
|
||||
We do this by converting the internal `Char` to an integer, adding one to it,
|
||||
then converting back to a `Char`. This low-level conversion loses the refinement
|
||||
context, forcing us to call `refineChar` on the new value to bring it back into
|
||||
the refined type, providing us type-level assurance that this function will
|
||||
return `Nothing` if an overflow occurs.
|
||||
|
||||
```idris
|
||||
incriment : PasswordChar -> Maybe PasswordChar
|
||||
incriment (MkPC char) =
|
||||
let next = chr $ ord char + 1
|
||||
in refineChar next
|
||||
```
|
||||
|
||||
A `Password` is a `Vect` of 8 `PasswordChar`s. This `Vect` is sorted in reverse
|
||||
order compared to the `String` it corresponds to, with the right-most letter
|
||||
first, to make implementing the `incrimentPassword` function a little easier and
|
||||
cleaner.
|
||||
|
||||
We also provide conversion to/from a `String`
|
||||
|
||||
```idris
|
||||
Password : Type
|
||||
Password = Vect 8 PasswordChar
|
||||
|
||||
parsePassword : Has (Except String) fs => String -> Eff fs Password
|
||||
parsePassword str = do
|
||||
cs <- note "Password has incorrect number of characters: \{str}"
|
||||
. toVect 8 . reverse . unpack $ str
|
||||
cs <- note "Password contained invalid characters: \{str}"
|
||||
$ traverse refineChar cs
|
||||
pure cs
|
||||
|
||||
passwordToString : Password -> String
|
||||
passwordToString = pack . toList . reverse . map char
|
||||
```
|
||||
|
||||
Define a function to increment a `Password`, this function will "roll over",
|
||||
producing `aaaaaaaa` if provided `zzzzzzzz`.
|
||||
|
||||
```idris
|
||||
incrimentPassword : Vect n PasswordChar -> Vect n PasswordChar
|
||||
incrimentPassword [] = []
|
||||
incrimentPassword (x :: xs) =
|
||||
case incriment x of
|
||||
Nothing => lowest :: incrimentPassword xs
|
||||
Just x => x :: xs
|
||||
```
|
||||
|
||||
### Password validity
|
||||
|
||||
A password must contain a run of at least 3 incrementing characters, check this
|
||||
by converting the `PasswordChar`s to their integer representations. Remember
|
||||
that our `Password` `Vect` is backwards compared to the string representation.
|
||||
|
||||
```idris
|
||||
incrimentingChars : Vect n PasswordChar -> Bool
|
||||
incrimentingChars (z :: next@(y :: (x :: xs))) =
|
||||
let [x, y, z] : Vect _ Int = map (ord . char) [x, y, z]
|
||||
in if y == x + 1 && z == y + 1
|
||||
then True
|
||||
else incrimentingChars next
|
||||
incrimentingChars _ = False
|
||||
```
|
||||
|
||||
A password may not contain `i`, `o`, or `l`
|
||||
|
||||
```idris
|
||||
noInvalidChars : Vect n PasswordChar -> Bool
|
||||
noInvalidChars = not . (any (flip contains $ ['i', 'o', 'l'])) . map char
|
||||
```
|
||||
|
||||
A password contains at least two different non-overlapping pairs.
|
||||
|
||||
We check this by pattern matching our password two characters at a time,
|
||||
consuming both characters if a matched pair is found, and tacking on the `Char`
|
||||
the list is composed of to an accumulator list as we go. This list is then
|
||||
reduced to only its unique elements (it's `nub`), and checking to see if it's
|
||||
length is at least 2.
|
||||
|
||||
```idris
|
||||
containsPairs : Vect n PasswordChar -> Bool
|
||||
containsPairs xs = length (nub $ pairs (reverse xs) []) >= 2
|
||||
where
|
||||
pairs : Vect m PasswordChar -> (acc : List Char) -> List Char
|
||||
pairs [] acc = acc
|
||||
pairs (x :: []) acc = acc
|
||||
pairs (x :: (y :: xs)) acc =
|
||||
if x == y
|
||||
-- If there is a pair, consume it to prevent detecting overlapping pairs
|
||||
then pairs xs (x.char :: acc)
|
||||
-- If there isn't a pair, only consume one character
|
||||
else pairs (y :: xs) acc
|
||||
```
|
||||
|
||||
Combine our password criteria into one function
|
||||
|
||||
```idris
|
||||
part1Critera : Vect n PasswordChar -> Bool
|
||||
part1Critera xs = incrimentingChars xs && noInvalidChars xs && containsPairs xs
|
||||
```
|
||||
|
||||
### Find the next password
|
||||
|
||||
Find the next password based on a criteria function
|
||||
|
||||
```idris
|
||||
findNextPassword :
|
||||
(f : Vect n PasswordChar -> Bool) -> (password : Vect n PasswordChar)
|
||||
-> Vect n PasswordChar
|
||||
findNextPassword f password =
|
||||
let next = incrimentPassword password
|
||||
in if f next
|
||||
then next
|
||||
else findNextPassword f next
|
||||
```
|
||||
|
||||
## Part Functions
|
||||
|
||||
### Part 1
|
||||
|
||||
```idris
|
||||
part1 : Eff (PartEff String) (String, ())
|
||||
part1 = do
|
||||
input <- map trim $ askAt "input"
|
||||
password <- parsePassword input
|
||||
info "Starting password: \{show password} -> \{passwordToString password}"
|
||||
let next_password = findNextPassword part1Critera password
|
||||
pure (passwordToString next_password, ())
|
||||
```
|
||||
|
||||
<!-- idris
|
||||
public export
|
||||
day11 : Day
|
||||
day11 = First 11 part1
|
||||
-->
|
||||
|
||||
## References
|
||||
|
||||
[^1]: https://github.com/stefan-hoeck/idris2-refined/
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 2
|
||||
# [Year 2015 Day 2](https://adventofcode.com/2015/day/2)
|
||||
|
||||
This day provides us our first little taste of effectful parsing
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 3
|
||||
# [Year 2015 Day 3](https://adventofcode.com/2015/day/3)
|
||||
|
||||
This day provides a gentle introduction to `mutual` blocks and mutually
|
||||
recursive functions.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 4
|
||||
# [Year 2015 Day 4](https://adventofcode.com/2015/day/4)
|
||||
|
||||
This day introduces us to a little bit of FFI, linking to openssl to use it's
|
||||
`MD5` functionality.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 5
|
||||
# [Year 2015 Day 5](https://adventofcode.com/2015/day/5)
|
||||
|
||||
This day provides a nice chance to introduce
|
||||
[views](https://idris2.readthedocs.io/en/latest/tutorial/views.html),
|
||||
|
|
|
|||
|
|
@ -1,4 +1,8 @@
|
|||
# Year 2015 Day 6
|
||||
# \[Year 2015 Day 6\](https://adventofcode.com/2015/day/
|
||||
|
||||
6.
|
||||
|
||||
Introduction to the advent of code classic 2d grid problem.
|
||||
|
||||
<!-- idris
|
||||
module Years.Y2015.Day6
|
||||
|
|
|
|||
|
|
@ -1,4 +1,6 @@
|
|||
# Year 2015 Day 7
|
||||
# \[Year 2015 Day 7\](https://adventofcode.com/2015/day/
|
||||
|
||||
7.
|
||||
|
||||
This day provides us a gentle introduction to dependent maps.
|
||||
|
||||
|
|
@ -53,7 +55,10 @@ Input : Type
|
|||
Input = Either Literal Wire
|
||||
```
|
||||
|
||||
Description of a Gate, tagged in the type with the name of the output wire
|
||||
Description of a Gate, tagged in the type with the name of the output wire.
|
||||
|
||||
This creates what is referred to as an "indexed type family", in this case a
|
||||
family of `Gate` types indexed by values of type `Wire`.
|
||||
|
||||
```idris
|
||||
data Gate : Wire -> Type where
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 8
|
||||
# [Year 2015 Day 8](https://adventofcode.com/2015/day/8)
|
||||
|
||||
This day provides a more in depth introduction to writing effectful parsers,
|
||||
making use of state and non-determinism in our parsers.
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
# Year 2015 Day 9
|
||||
# [Year 2015 Day 9](https://adventofcode.com/2015/day/9)
|
||||
|
||||
This day provides our first example of a graph traversal problem. We'll use a
|
||||
`Choose` based effectful breath first search to identify all the possible paths
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue