diff --git a/README.md b/README.md index 6dfd540..95cd2ee 100644 --- a/README.md +++ b/README.md @@ -1,25 +1,10 @@ # 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. -## 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 +# Index of non-day modules - [Runner](src/Runner.md) @@ -41,61 +26,16 @@ solution. Extend the functionality of the effects included in the [eff](https://github.com/stefan-hoeck/idris2-eff/) library - - [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 +# 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) diff --git a/advent.ipkg b/advent.ipkg index c9776ba..e915d93 100644 --- a/advent.ipkg +++ b/advent.ipkg @@ -21,7 +21,6 @@ depends = base , ansi , if-unsolved-implicit , c-ffi - , refined -- modules to install modules = Runner diff --git a/src/Grid.md b/src/Grid.md new file mode 100644 index 0000000..ceb6a22 --- /dev/null +++ b/src/Grid.md @@ -0,0 +1,371 @@ +# 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 +``` diff --git a/src/Main.md b/src/Main.md index f602362..a913135 100644 --- a/src/Main.md +++ b/src/Main.md @@ -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 `Logger` into -the effects list. +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 @@ -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 -Makes use of `Logger`'s `handleLoggerIO` function to "lower" logging actions -into `IO` 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 diff --git a/src/Runner.md b/src/Runner.md index 31b036e..500821b 100644 --- a/src/Runner.md +++ b/src/Runner.md @@ -22,15 +22,16 @@ import public Util.Eff # 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 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 `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 +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 will come in handy if a part needs `IO` for performance +doing any IO, this may come in handy if a part needs `IO` for performance reasons. ```idris @@ -45,19 +46,19 @@ PartEff err = # 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. +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 +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`. +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 @@ -79,9 +80,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. 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`. +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 @@ -90,7 +91,8 @@ 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 `()`. +`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 @@ -104,8 +106,8 @@ The `First` constructor only accepts a `part1`, it does the work of filling in ### Both -The `Both` constructor does less heavy lifting, the only thing it needs to do 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 @@ -121,17 +123,16 @@ 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 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. +[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 compare the day numbers of the two `Day`s using the less-than(`<`) +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 of `Day`s is sorted in ascending order and that no two `Day`s have -the same day number. +Fresh List is sorted in ascending order and that no two `Day`s have the same day +number. ```idris ||| Freshness criteria for days @@ -149,7 +150,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, also containing the year number for this collection. +year, and is mostly just a simple container. ```idris ||| Collect all the days in a given year @@ -165,10 +166,9 @@ 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,7 +186,8 @@ 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. +`Year` collects a number of days, sorting the `Year`s in a `FreshList` to +provide API defensiveness. ```idris ||| Collect all years diff --git a/src/Util/Eff.md b/src/Util/Eff.md index 1baa453..1b51cba 100644 --- a/src/Util/Eff.md +++ b/src/Util/Eff.md @@ -22,18 +22,9 @@ 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 : Type where - Err : Level - Warn : Level - Info : Level - Debug : Level - Trace : Level - Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level +data Level = Err | Warn | Info | Debug | Trace | Other Nat ``` # Days @@ -88,12 +87,6 @@ y2015 = MkYear 2015 [ , day10 ``` -## [Day 11](Y2015/Day11.md) - -```idris - , day11 -``` - ```idris ] ``` diff --git a/src/Years/Y2015/Day1.md b/src/Years/Y2015/Day1.md index f8820d3..cfc4950 100644 --- a/src/Years/Y2015/Day1.md +++ b/src/Years/Y2015/Day1.md @@ -1,4 +1,4 @@ -# [Year 2015 Day 1](https://adventofcode.com/2015/day/1) +# Year 2015 Day 1 Pretty simple, basic warmup problem, nothing really novel is on display here except the effectful part computations. diff --git a/src/Years/Y2015/Day10.md b/src/Years/Y2015/Day10.md index 201e0c5..7971126 100644 --- a/src/Years/Y2015/Day10.md +++ b/src/Years/Y2015/Day10.md @@ -1,4 +1,4 @@ -# [Year 2015 Day 10](https://adventofcode.com/2015/day/10) +# Year 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. diff --git a/src/Years/Y2015/Day11.md b/src/Years/Y2015/Day11.md deleted file mode 100644 index 0f6ccc6..0000000 --- a/src/Years/Y2015/Day11.md +++ /dev/null @@ -1,227 +0,0 @@ -# [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 -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 -``` - - - -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, ()) -``` - - - -## References - -[^1]: https://github.com/stefan-hoeck/idris2-refined/ diff --git a/src/Years/Y2015/Day2.md b/src/Years/Y2015/Day2.md index 22081b2..43ca0b1 100644 --- a/src/Years/Y2015/Day2.md +++ b/src/Years/Y2015/Day2.md @@ -1,4 +1,4 @@ -# [Year 2015 Day 2](https://adventofcode.com/2015/day/2) +# Year 2015 Day 2 This day provides us our first little taste of effectful parsing diff --git a/src/Years/Y2015/Day3.md b/src/Years/Y2015/Day3.md index 195d1d9..9dd7ecc 100644 --- a/src/Years/Y2015/Day3.md +++ b/src/Years/Y2015/Day3.md @@ -1,4 +1,4 @@ -# [Year 2015 Day 3](https://adventofcode.com/2015/day/3) +# Year 2015 Day 3 This day provides a gentle introduction to `mutual` blocks and mutually recursive functions. diff --git a/src/Years/Y2015/Day4.md b/src/Years/Y2015/Day4.md index f907fa1..a1fee57 100644 --- a/src/Years/Y2015/Day4.md +++ b/src/Years/Y2015/Day4.md @@ -1,4 +1,4 @@ -# [Year 2015 Day 4](https://adventofcode.com/2015/day/4) +# Year 2015 Day 4 This day introduces us to a little bit of FFI, linking to openssl to use it's `MD5` functionality. diff --git a/src/Years/Y2015/Day5.md b/src/Years/Y2015/Day5.md index e41bd96..d947885 100644 --- a/src/Years/Y2015/Day5.md +++ b/src/Years/Y2015/Day5.md @@ -1,4 +1,4 @@ -# [Year 2015 Day 5](https://adventofcode.com/2015/day/5) +# Year 2015 Day 5 This day provides a nice chance to introduce [views](https://idris2.readthedocs.io/en/latest/tutorial/views.html), diff --git a/src/Years/Y2015/Day6.md b/src/Years/Y2015/Day6.md index 131be48..a2b5cd0 100644 --- a/src/Years/Y2015/Day6.md +++ b/src/Years/Y2015/Day6.md @@ -1,8 +1,4 @@ -# \[Year 2015 Day 6\](https://adventofcode.com/2015/day/ - -6. - -Introduction to the advent of code classic 2d grid problem. +# Year 2015 Day 6