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
+of one single idris application, and thoroughly document the results as literate
-Idris files.
+idris files.
 
-## Authors Note
+# Index of non-day modules
-
-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)
 
@@ -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)
+# Index of years and days
-
-    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)

advent.ipkg

@@ -21,7 +21,6 @@ depends = base
         , ansi
         , if-unsolved-implicit
         , c-ffi
-        , refined
 
 -- modules to install
 modules = Runner

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
+```

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
+blackhole the logs. Afterwards, use `logHandler` to introduce the logging
-the effects list.
+`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
+This function uses the provided `String -> IO ()` to remove the `Writer` from
-into `IO` within the effect.
+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

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
+the available effects are meant to be the same across both parts, only varying
-type of the error value for the `Except` effect, we construct a type level
+in the type of the error value in the `Except` effect, I construct a type level
-function to have a single source of truth. The `err` type can be any type with a
+function to have a single source of truth for this. The `err` type can be any
-`Show` implementation, but that constraint will be tacked on in the next step.
+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
+A `Writer` effect is provided for logging, and a `Reader` effect is provided to
-to pass in the input, to make the top level API a little bit cleaner. `IO` is
+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
+effectful `part2` computation, the day number, and does some type wrangling to
-get the type system out of our way.
+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
+resulting from parsing, between `part1` and `part2`, and this is achieved by the
-the erased `ctx` type, which is totally opaque to the runner. The code in `Main`
+erased `ctx` type, which is totally opaque here. The runner code in `Main` will
-will provide the value of the `ctx` type produced as part of the output of
+provide the value of the `ctx` type produced as part of the output of `part1` as
-`part1` and as the input of `part2`.
+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
+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`, as well as one
+pair of constructors for the case where there is only a `part1` and for where
-for when there is a `part1` and a `part2`.
+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
+The `Both` constructor does a little bit less heavy lifting, the only thing it
-wrap `part2` in a `Just`.
+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
+[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build
-API defensively against duplicate days and cosmetically annoying out of order
+defensiveness into the API. A Fresh List structurally only allows you to prepend
-day registration. A Fresh List structurally only allows you to prepend/cons an
+an element onto it when it satisfies some _freshness_ criteria relative to the
-element onto it when it satisfies some _freshness criteria_ relative to the
+elements already in the list.
-elements already contained 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
+Fresh List is sorted in ascending order and that no two `Day`s have the same day
-the same day number.
+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.
+`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
-We do so by applying the less-than relationship against the year number of the
+with `FreshDay`.
-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

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
+data Level = Err | Warn | Info | Debug | Trace | Other Nat 
-  Err : Level
-  Warn : Level
-  Info : Level
-  Debug : Level
-  Trace : Level
-  Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level
 ```
 
 <!-- idris
@@ -53,7 +44,7 @@ natToLevel 1 = Warn
 natToLevel 2 = Info
 natToLevel 3 = Debug
 natToLevel 4 = Trace
-natToLevel (S (S (S (S (S k))))) = Other (5 + k)
+natToLevel k = Other k
 
 export
 Eq Level where
@@ -139,8 +130,10 @@ handleLoggerIO max_level x =
     else pure . ignore $ x
 ```
 
-Provide a family of effectful actions that emit log messages at the different
+Use the `WriterL "log" String` effect like a logging library. We'll provide a
-log levels.
+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
@@ -162,10 +155,6 @@ 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

src/Years/Y2015.md

@@ -17,7 +17,6 @@ import Years.Y2015.Day7
 import Years.Y2015.Day8
 import Years.Y2015.Day9
 import Years.Y2015.Day10
-import Years.Y2015.Day11
 -->
 
 # Days
@@ -88,12 +87,6 @@ y2015 = MkYear 2015 [
   , day10
 ```
 
-## [Day 11](Y2015/Day11.md)
-
-```idris
-  , day11
-```
-
 ```idris
   ]
 ```

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.

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.

src/Years/Y2015/Day11.md

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

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
 

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.

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.

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

src/Years/Y2015/Day6.md

@@ -1,8 +1,4 @@
-# \[Year 2015 Day 6\](https://adventofcode.com/2015/day/
+# Year 2015 Day 6
-
-6.
-
-Introduction to the advent of code classic 2d grid problem.
 
 <!-- idris
 module Years.Y2015.Day6

src/Years/Y2015/Day7.md

@@ -1,6 +1,4 @@
-# \[Year 2015 Day 7\](https://adventofcode.com/2015/day/
+# Year 2015 Day 7
-
-7.
 
 This day provides us a gentle introduction to dependent maps.
 
@@ -55,10 +53,7 @@ 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

src/Years/Y2015/Day8.md

@@ -1,4 +1,4 @@
-# [Year 2015 Day 8](https://adventofcode.com/2015/day/8)
+# Year 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.

src/Years/Y2015/Day9.md

@@ -1,4 +1,4 @@
-# [Year 2015 Day 9](https://adventofcode.com/2015/day/9)
+# Year 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