Year 2015 Day 11 Part 2

README.md

@@ -1,10 +1,30 @@
 # Advent
 
 The goal of this project is to get all 500 currently available stars in the form
-of one single idris application, and thoroughly document the results as literate
-idris files.
+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.
+
+While this project is intended to read more like a book, while it is still a
+work in progress, you can follow its development as a psuedo-blog by subscribing
+to the rss feed for the repository in your feed reader:
+https://git.stranger.systems/Idris/advent.rss
+
+## Index of non-day modules
 
 - [Runner](src/Runner.md)
 
@@ -31,17 +51,56 @@ solution.
     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)

advent.ipkg

@@ -28,7 +28,6 @@ modules = Runner
         , Util
         , Util.Eff
         , Util.Digits
-        , Grid
 
 -- main file (i.e. file to load at REPL)
 main = Main

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

src/Years/Y2015/Day1.md

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

src/Years/Y2015/Day10.md

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

src/Years/Y2015/Day11.md

@@ -1,4 +1,4 @@
-# Year 2015 Day 11
+# [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
@@ -183,8 +183,8 @@ containsPairs xs = length (nub $ pairs (reverse xs) []) >= 2
 Combine our password criteria into one function
 
 ```idris
-part1Critera : Vect n PasswordChar -> Bool
-part1Critera xs = incrimentingChars xs && noInvalidChars xs && containsPairs xs
+passwordCriteria : Vect n PasswordChar -> Bool
+passwordCriteria xs = incrimentingChars xs && noInvalidChars xs && containsPairs xs
 ```
 
 ### Find the next password
@@ -207,19 +207,32 @@ findNextPassword f password =
 ### Part 1
 
 ```idris
-part1 : Eff (PartEff String) (String, ())
+part1 : Eff (PartEff String) (String, Password)
 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, ())
+  let next_password = findNextPassword passwordCriteria password
+  pure (passwordToString next_password, next_password)
+```
+
+### Part 2
+
+```idris
+part2 : Password -> Eff (PartEff String) String
+part2 password = do
+  info 
+    "Second starting password: \{show password} -> \{passwordToString password}"
+  let next_password = findNextPassword passwordCriteria password
+  pure $ passwordToString next_password
 ```
 
 <!-- idris
 public export
 day11 : Day
-day11 = First 11 part1
+day11 = Both 11 part1 part2
 -->
 
+## References
+
 [^1]: https://github.com/stefan-hoeck/idris2-refined/

src/Years/Y2015/Day2.md

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

src/Years/Y2015/Day3.md

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

src/Years/Y2015/Day4.md

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

src/Years/Y2015/Day5.md

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

src/Years/Y2015/Day6.md

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

src/Years/Y2015/Day7.md

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

src/Years/Y2015/Day8.md

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

src/Years/Y2015/Day9.md

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