Fix build-book output directory

Contains views for seeing integers as lists of digits

.gitignore

@@ -4,3 +4,5 @@ inputs/
 support/*.o
 support/advent-support
 tmp/
+book/
+index.html

README.md

@@ -1,10 +1,33 @@
 # 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
+
+This entire book is a single literate code base, the source code is available at
+<https://git.stranger.systems/Idris/advent>.
+
+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)
 
@@ -26,13 +49,96 @@ 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.
+
+- [Array](src/Array.md)
+
+  Provider wrappers over the standard library `IOArray` type to make them more
+  ergonomic to use.
+
+- [Parser](src/Parser.md)
+
+  Effectful parser mini-library
+
+  - [Interface](src/Parser/Interface.md)
+
+    Effectful parser API
+
+  - [ParserState](src/Parser/ParserState.md)
+
+    Internal state of a parser
+
+  - [Numbers](src/Parser/Numbers.md)
+
+    Parsers for numerical values in multiple bases
+
+  - [JSON](src/Parser/JSON.md)
+
+  JSON Parser
+
+## 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
+
+  - [Day 12](src/Years/Y2015/Day12.md)
+
+    New Parser Effect stack and DLists
+
+  - [Day 13](src/Years/Y2015/Day13.md)
+
+    Naive ring buffer and `parameters` blocks[^2]
+
+## References
+
+[^1]: Idris 2 Manual:
+    [Views and the "with" rule](https://idris2.readthedocs.io/en/latest/tutorial/views.html#views-and-the-with-rule)
+
+[^2]: <https://idris2.readthedocs.io/en/latest/tutorial/modules.html#parameterised-blocks-parameters-blocks>

advent.ipkg

@@ -16,17 +16,25 @@ authors = "Nathan McCarty"
 depends = base
         , contrib
         , structures
+        , tailrec
         , eff
         , elab-util
+        , sop
         , ansi
         , if-unsolved-implicit
         , c-ffi
+        , refined
 
 -- modules to install
 modules = Runner
         , Util
         , Util.Eff
-        , Grid
+        , Util.Digits
+        , Array
+        , Parser
+        , Parser.Interface
+        , Parser.Numbers
+        , Parser.JSON
 
 -- main file (i.e. file to load at REPL)
 main = Main

book.toml

@@ -0,0 +1,13 @@
+[book]
+authors = ["Nathan McCarty"]
+language = "en"
+multilingual = false
+src = "src"
+title = "Idris 2 by Highly Contrived Example"
+
+[build]
+create-missing = false
+# use-default-preprocessors = false
+
+[output.html]
+preferred-dark-theme = "ayu"

scripts/build-book

@@ -0,0 +1,115 @@
+#!/usr/bin/env raku
+
+use File::Temp;
+use Shell::Command;
+use paths;
+
+unit sub MAIN(Bool :$upload);
+
+my $tempdir = tempdir.IO;
+my $ttc-number = dir('build/ttc').first.basename;
+my $ttc = "build/ttc/$ttc-number".IO;
+
+# Filenames to ignore while processing source files
+my Str:D @ignored = ["README.md", "SUMMARY.md"];
+# Check to see if a filename is ignored
+sub not-ignored($path) {
+    for @ignored -> $ignored {
+        return False if $path.ends-with: $ignored;
+    }
+    return True;
+}
+
+# Copy a file from the current directory to the temporary directory, preserving
+# realtive path. Resolves symlinks in source, but does not reflect symlink
+# resoultion in the output path
+sub copy-to-dest($src) {
+   my $src-path = do given $src {
+       when Str {
+           $src.IO
+       }
+       when IO::Path {
+           $src
+       }
+       default {
+           die "Invalid source $src, {$src.WHAT}"
+       }
+   }
+   my $output-path = $tempdir.add($src-path.relative).IO;
+   # Create the parent directory if needed
+   if !$output-path.parent.d {
+       $output-path.parent.mkdir;
+
+   }
+   # Copy the file
+   $src-path.resolve.copy: $output-path;
+}
+
+# Special handling for our readme file, we need to butcher up it's links
+my $readme-contents = 'README.md'.IO.slurp;
+$readme-contents ~~ s:g/'src/'//;
+my $readme-dest = $tempdir.add('src/README.md');
+$readme-dest.parent.mkdir;
+$readme-dest.spurt: $readme-contents;
+
+# Copy our metadata files
+copy-to-dest "book.toml";
+copy-to-dest "src/SUMMARY.md";
+
+# Katla over the source files
+for paths("src", :file(*.&not-ignored)) -> $path {
+    my $ttc-path = $ttc.add($path.IO.relative: "src").extension: "ttm";
+    katla $path.IO.relative, $ttc-path.relative;
+}
+
+# Build the book
+
+indir $tempdir, {
+    my $mdbook = run <mdbook build>;
+    die "Ooops" unless $mdbook;
+}
+
+# Copy it over
+rm_rf "book";
+cp $tempdir.add("book"), "book", :r;
+
+if $upload {
+    my $rsync = run 'rsync', '-avzh', $tempdir.add("book/").Str,
+                'ubuntu@static.stranger.systems:/var/www/static.stranger.systems/idris-by-contrived-example';
+    die "rsync went bad" unless $rsync;
+}
+
+# This function goes at the end because it breaks emacs fontification after it
+# for some bizzare reason.
+#
+# Invoke katla on a source file, streaming its output to the temporary directory
+sub katla($src, $ttc-src) {
+    # Run katla and collect the output
+    my $katla = run 'katla', 'markdown', $src, $ttc-src, :out;
+    my $output = $katla.out.slurp(:close);
+    # Post process them to set themeing correctly
+    # TODO: We need to remove the extra new line after the start of code blocks
+    # still
+    $output ~~ s:g/'<style>' .* '</style>'//;
+    $output ~~ s:g/'<br />'//;
+    $output ~~ s:g/'\\*'/*/;
+    $output ~~ s:g/'\\_'/_/;
+    $output ~~ s:g/'\\\\'/\\/;
+    $output ~~ s:g/'<code'/<pre><code/;
+    $output ~~ s:g/'</code>'/<\/code><\/pre>/;
+    $output ~~ s:g/'="IdrisKeyword"'/="hljs-keyword"/;
+    $output ~~ s:g/'="IdrisModule"'/="hljs-symbol hljs-emphasis"/;
+    $output ~~ s:g/'="IdrisComment"'/="hljs-comment"/;
+    $output ~~ s:g/'="IdrisFunction"'/="hljs-symbol"/;
+    $output ~~ s:g/'="IdrisBound"'/="hljs-name"/;
+    $output ~~ s:g/'="IdrisData"'/="hljs-title"/;
+    $output ~~ s:g/'="IdrisType"'/="hljs-type"/;
+    $output ~~ s:g/'="IdrisNamespace"'/="hljs-symbol hljs-emphasis"/;
+
+    # Spurt the output to the temporary directory
+    my $output-path = $tempdir.add: $src;
+    if !$output-path.parent.d {
+        $output-path.parent.mkdir;
+    }
+    $output-path.spurt($output);
+}

src/Array.md

@@ -0,0 +1,537 @@
+# Array Wrappers
+
+```idris
+module Array
+
+import Data.IOArray
+import Data.Vect
+import Data.List.Lazy
+import Data.Fin
+import Data.Iterable
+import Decidable.Equality
+import Control.WellFounded
+```
+
+```idris hide
+import System
+```
+
+```idris
+%default total
+%hide Prelude.Types.elem
+```
+
+Provide some wrappers over the standard library IO arrays, using plenty of
+unsafe operations along the way.
+
+## Internal Utility Functions
+
+Unsafely unwrap a `Maybe`, making the assumption that it is a `Just`.
+
+```idris
+%unsafe
+unwrapUnsafe : Maybe a -> a
+unwrapUnsafe x = assert_total $ unwrapUnsafe' x
+  where 
+    partial
+    unwrapUnsafe' : Maybe a -> a
+    unwrapUnsafe' (Just x) = x
+```
+
+Insert an element into an `IOArray` at the index described by the given `Fin`.
+
+```idris
+insertPair : IOArray e -> (e, Fin n) -> IO ()
+insertPair arr (elem, idx) = do
+  let idx : Int = cast . finToInteger $ idx
+  _ <- writeArray arr idx elem
+  pure ()
+```
+
+### Tail safe monadic recursion with lazy lists
+
+Generate all of the fins of a given size, lazily.
+
+```idris
+allFins : (n : Nat) -> LazyList (Fin n)
+allFins 0 = []
+allFins (S k) = FZ :: map FS (allFins k)
+```
+
+LazyLists have a size
+
+```idris
+Sized (LazyList e) where
+  size [] = 0
+  size (x :: xs) = S (size xs)
+```
+
+Convert a `Vect` to a `LazyList`
+
+```idris
+vectLazy : Vect n e -> LazyList e
+vectLazy [] = []
+vectLazy (x :: xs) = x :: vectLazy xs
+```
+
+LazyLists are iterable
+
+```idris
+refl : {k : Nat} -> LTE k k
+refl = reflexive {x = k}
+
+Iterable (LazyList a) a where
+  iterM accum done ini seed =
+    trSized seed ini $
+      \case Nil    => pure . Done . done
+            h :: t => map (Cont t refl) . accum h
+```
+
+## Immutable arrays
+
+```idris hide
+namespace Immutable
+```
+
+Immutable arrays created from vectors that provide constant time indexing and
+slicing operations.
+
+As an invariant of the the type, every "slot" in the inner `IOArray` must always
+be a `Just`, unsafe operations are performed that depend on that.
+
+```idris
+  ||| An immutable array of length `n`
+  export
+  data IArray : Nat -> Type -> Type where
+    MkIArray : (size : Nat) -> (offset : Int) -> (inner : IOArray e) 
+      -> IArray size e
+  %name IArray xs, ys, zs
+```
+
+### Basic Interface
+
+Indexing operation
+
+```idris
+  export
+  index : (idx : Fin n) -> IArray n e -> e
+  index idx (MkIArray size offset inner) = unsafePerformIO index' 
+    where
+      index' : IO e
+      index' = do
+        -- Convert the index to an Int for use in the IO array
+        let idx : Int = cast . finToInteger $ idx
+        map unwrapUnsafe $ readArray inner (idx + offset) 
+```
+
+Getting the length of an `IArray`, as well as a proof of correctness for the
+length function
+
+```idris
+  export
+  length : IArray n e -> Nat
+  length (MkIArray n _ inner) = n
+  
+  export
+  lengthCorrect : (array : IArray n e) -> length array = n
+  lengthCorrect (MkIArray n _ inner) = Refl
+```
+
+Basic conversion operations
+
+```idris
+  export
+  fromVect : {n : Nat} -> Vect n e -> IArray n e
+  fromVect xs = unsafePerformIO fromVect'
+    where
+      fromVect' : IO $ IArray n e
+      fromVect' = do
+        let pairs = zip (vectLazy xs) (allFins n)
+        array <- newArray (cast n)
+        forM_ (insertPair array) pairs
+        pure $ MkIArray n 0 array
+  
+  export
+  replicate : (n : Nat) -> e -> IArray n e
+  replicate n x = unsafePerformIO replicate'
+    where
+      insertR : IOArray e -> Fin n -> IO ()
+      insertR arr idx = do
+        let idx : Int = cast . finToInteger $ idx
+        _ <- writeArray arr idx x
+        pure ()
+      replicate' : IO $ IArray n e
+      replicate' = do
+        array <- newArray (cast n)
+        forM_ (insertR array) (Array.allFins n)
+        pure $ MkIArray n 0 array
+
+  export
+  toVect : IArray n e -> Vect n e
+  toVect xs = 
+    let xs' : IArray (length xs) e = rewrite lengthCorrect xs in xs
+        values : Vect _ e = map (flip index $ xs') (allFins _)
+    in rewrite sym $ lengthCorrect xs in values
+  
+  arrayToList : IArray n e -> List e
+  arrayToList xs = 
+    let xs' : IArray (length xs) e = rewrite lengthCorrect xs in xs
+    in map (flip index $ xs') (allFins (length xs))
+```
+
+Unsafely create an array from a lazy list of values, for internal use only. Will
+cause crashes if the provided `LazyList` isn't the right length.
+
+```idris
+  %unsafe
+  unsafeFromLazy : {n : Nat} -> LazyList e -> IO (IArray n e)
+  unsafeFromLazy xs = do
+    array <- newArray (cast n)
+    let pairs = zip xs (allFins n)
+    forM_ (insertPair array) pairs
+    pure $ MkIArray _ 0 array
+```
+
+Typical drop and take operations, implemented in constant time
+
+```idris
+  -- TODO: Minimize whatever compiler bug is requiring us to use this
+  newOffset : Nat -> Int -> Int
+  newOffset k i = cast k + i
+
+  export
+  drop : (n : Nat) -> IArray (n + m) e -> IArray m e
+  drop n xs@(MkIArray _ offset inner) = 
+    believe_me $ MkIArray (length xs `minus` n) (newOffset n offset) inner
+
+  export
+  drop' : (n : Nat) -> IArray l e -> IArray (minus l n) e
+  drop' n (MkIArray l offset inner) = 
+    if n >= l
+      then believe_me $ fromVect [] {e}
+      else MkIArray (l `minus` n) (newOffset n offset) inner
+  
+  export
+  take : (n : Nat) -> IArray (n + m) e -> IArray n e
+  take n (MkIArray _ offset inner) = MkIArray n offset inner
+```
+
+A view for pattern matching on `IArray`s as if they were lists
+
+```idris
+  namespace View
+    public export
+    data AsList : IArray n e -> Type where
+      Nil : {0 tail : IArray 0 e} -> AsList tail
+      (::) : {0 xs : IArray (S n) e} -> {rest : IArray n e} 
+        -> (head : e) -> (tail : Lazy (AsList rest)) -> AsList xs
+    
+    public export 
+    asList : (xs : IArray n e) -> AsList xs
+    asList (MkIArray 0 offset inner) = []
+    asList xs@(MkIArray (S k) offset inner) = 
+      let head = 0 `index` xs
+          rest = drop 1 xs
+      in head :: (asList rest)
+```
+
+Convert to a `LazyList` using our view
+
+```idris
+  export
+  toLazy : IArray n e -> LazyList e
+  toLazy xs with (asList xs)
+    toLazy xs | [] = []
+    toLazy xs | (head :: tail) = 
+      head :: toLazy _ | tail
+```
+
+Typical filtering and finding interface
+
+```idris
+  -- Don't know if this one is really worth optimizing
+  export
+  filter : (e -> Bool) -> IArray n e -> (p : Nat ** IArray p e)
+  filter f xs = 
+    let (_ ** ps) = filter f (toVect xs)
+    in (_ ** fromVect ps)
+ 
+  export
+  find : (e -> Bool) -> IArray n e -> Maybe e
+  find f xs with (asList xs)
+    find f xs | [] = Nothing
+    find f xs | (head :: tail) = 
+      if f head
+        then Just head
+        else find f _ | tail
+ 
+  export
+  findIndex : (e -> Bool) -> IArray n e -> Maybe (Fin n)
+  findIndex f xs = 
+    let indexed = zip (toLazy xs) (allFins (length xs))
+    in findIndex' f indexed
+    where
+      findIndex' : (e -> Bool) -> LazyList (e, Fin (length xs)) -> Maybe (Fin n)
+      findIndex' f [] = Nothing
+      findIndex' f ((e, idx) :: ys) = 
+        if f e
+          then rewrite sym $ lengthCorrect xs in Just idx
+          else findIndex' f ys
+ 
+  export
+  findIndices : (e -> Bool) -> IArray n e -> List (Fin n)
+  findIndices f xs@(MkIArray n _ _) = 
+    let pairs = zip (toLazy xs) (allFins n)
+    in toList . map snd . filter (f . fst) $ pairs
+```
+
+### Interface Implementations
+
+Provide a `Foldable` implementation by performing indexing within the context of
+`unsafePerformIO`.
+
+```idris
+  export
+  Foldable (IArray n) where
+    foldl f acc_val (MkIArray n offset inner) = unsafePerformIO $ foldl'
+      where 
+        liftF : Fin n -> acc -> IO acc
+        liftF idx acc_val = do
+          let idx : Int = cast . finToInteger $ idx
+          val <- map unwrapUnsafe $ readArray inner (idx + offset)
+          pure $ f acc_val val
+        foldl' : IO acc
+        foldl' = iterM liftF id acc_val (Array.allFins n)
+    foldr f acc_val (MkIArray n offset inner) = unsafePerformIO $ foldr'
+      where
+        liftF : Fin n -> acc -> IO acc
+        liftF idx acc_val = do
+          let idx : Int = cast . finToInteger $ idx
+          val <- map unwrapUnsafe $ readArray inner (idx + offset)
+          pure $ f val acc_val
+        foldr' : IO acc
+        -- TODO: Make a lazy reverse allFins function so we aren't instantiating
+        -- the full index list here
+        foldr' = iterM liftF id acc_val (reverse $ List.allFins n)
+    toList = arrayToList
+```
+
+Provide implementations of `Eq`, `Ord`, and `DecEq` in terms of our `AsList`
+view. The `DecEq` implementation requires use of unsafe `believe_me`, as arrays
+are primitive types the compiler has no insight into the structure of.
+
+```idris
+  export
+  Eq e => Eq (IArray n e) where
+    xs == ys = (toLazy xs) == (toLazy ys)
+  
+  export
+  Ord e => Ord (IArray n e) where
+    compare xs ys = compare (toLazy xs) (toLazy ys)
+  
+  -- TODO : Optimize IArray DecEq
+  decEq' : DecEq e => {m : Nat} -> (xs, ys : IArray m e) -> Dec (xs = ys)
+  decEq' xs ys with (asList xs, asList ys)
+    decEq' xs ys | ([], []) = believe_me $ the (xs = xs) Refl
+    decEq' xs ys | ((h_x :: t_x), (h_y :: t_y)) = 
+      case decEq h_x h_y of
+        Yes prf => 
+          believe_me $ decEq' _ _ | (t_x, t_y)
+        No contra => believe_me contra
+
+  export
+  DecEq e => DecEq (IArray n e) where
+    decEq xs@(MkIArray n _ _) ys = decEq' xs ys
+```
+
+Provide `Functor`, `Applicative`, `Monad`, and `Traverseable` implementations by
+building a new array in an `IO` context
+
+```idris
+  map' : (f : a -> b) -> IArray n a -> IO (IArray n b)
+  map' f xs@(MkIArray n _ _) = do
+    array <- newArray (cast n)
+    let pairs = zip (map f . toLazy $ xs) (Array.allFins n)
+    forM_ (insertPair array) pairs
+    pure $ MkIArray n 0 array
+
+  export
+  Functor (IArray k) where
+    map f xs = unsafePerformIO $ map' f xs
+  
+  apply' : {n : Nat} -> IArray n (a -> b) -> IArray n a -> IO (IArray n b)
+  apply' fs xs = do
+    array <- newArray (cast n)
+    let applied = map (\(f, x) => f x) $ zip (toLazy fs) (toLazy xs)
+    let pairs = zip applied (allFins n)
+    forM_ (insertPair array) pairs
+    pure $ MkIArray n 0 array
+ 
+  -- Applicative requires the length of the array to be available at runtime at
+  -- the type level for `replicate`
+  export
+  {k : Nat} -> Applicative (IArray k) where
+    pure = replicate _
+    fs <*> xs = unsafePerformIO $ apply' fs xs
+
+  -- Like `Vect`'s `join`, this takes the diagonal elements
+  export
+  {k : Nat} -> Monad (IArray k) where 
+    join xs = 
+      let lazys = join' . map toLazy $ toLazy xs
+      in assert_total $ unsafePerformIO $ unsafeFromLazy lazys
+      where
+        covering
+        join' : LazyList (LazyList a) -> LazyList a
+        join' [] = []
+        join' ([] :: y) = []
+        join' ((x :: _) :: xs) = 
+          x :: join' (map (drop 1) xs)
+    -- join xs = fromVect . join . map toVect . toVect $ xs
+ 
+  -- TODO: Maybe take another pass at optimizing this? 
+  export
+  Traversable (IArray k) where 
+    traverse fun xs@(MkIArray k _ _) = 
+      map (unsafePerformIO . unsafeFromLazy . fromList) 
+      . Prelude.traverse fun 
+      . toList 
+      $ xs
+```
+
+Provide a `Show` implementation in terms of our `AsList` view through the
+`asLazy` wrapper.
+
+```idris
+  export
+  Show e => Show (IArray n e) where
+    show xs = 
+      let elements = map show $ toLazy xs
+      in case elements of
+        [] => "[]"
+        (x :: xs) => "[\{join' xs x}]"
+      where
+        join' : LazyList String -> (acc : String) -> String
+        join' [] acc = acc
+        join' (x :: []) acc = "\{acc}, \{x}"
+        join' (x :: (y :: xs)) acc = 
+          join' (y :: xs) "\{acc}, \{x}"
+```
+
+Provide a `Zippable` implementation by roundtripping through a `Vect`. This
+isn't the most efficient, but this provides a workable starter implementation.
+
+```idris
+  export
+  Zippable (IArray k) where 
+    zipWith f xs@(MkIArray k _ _) ys = 
+      unsafePerformIO . unsafeFromLazy $ zipWith f (toLazy xs) (toLazy ys)
+    zipWith3 f xs@(MkIArray k _ _) ys zs = 
+      unsafePerformIO . unsafeFromLazy $ zipWith3 f (toLazy xs) (toLazy ys) (toLazy zs)
+    unzipWith f xs@(MkIArray k _ _) = 
+      let (xs, ys) = unzipWith f (toLazy xs)
+      in (unsafePerformIO . unsafeFromLazy $ xs, 
+          unsafePerformIO . unsafeFromLazy $ ys)
+    unzipWith3 f xs@(MkIArray k _ _) = 
+      let (xs, ys, zs) = unzipWith3 f (toLazy xs)
+      in (unsafePerformIO . unsafeFromLazy $ xs, 
+          unsafePerformIO . unsafeFromLazy $ ys, 
+          unsafePerformIO . unsafeFromLazy $ zs)
+```
+
+Provide `Semigroup` and `Monoid` implementations, matching those for `Vect`, in
+terms of our other interfaces.
+
+```idris
+  export
+  Semigroup a => Semigroup (IArray k a) where 
+    xs <+> ys = zipWith (<+>) xs ys
+  
+  -- Monoid requires the length argument to be available at runtime for 
+  -- `replicate` to work
+  export
+  {k : Nat} -> Monoid a => Monoid (IArray k a) where 
+    neutral = replicate _ neutral
+```
+
+## Unit tests
+
+### IArray
+
+```idris
+-- @@test IArray RoundTrip
+iRoundTrip : IO Bool
+iRoundTrip = do
+  let test_vect : Vect _ Nat = [1, 2, 3, 4, 5]
+  putStrLn "test_vect: \{show test_vect}"
+  let xs = fromVect test_vect
+  putStrLn "xs: \{show xs}"
+  let round_tripped = toVect xs 
+  putStrLn "round_tripped: \{show round_tripped}"
+  pure $ test_vect == round_tripped
+
+-- @@test IArray drop/take
+iDropTake : IO Bool
+iDropTake = do
+  let test = fromVect [1, 2, 3, 4, 5]
+  putStrLn "test: \{show test}"
+  let dropped = drop 2 test
+  putStrLn "dropped: \{show dropped}"
+  let taked = take 3 test
+  putStrLn "taked: \{show taked}"
+  pure $ (toVect dropped) == [3, 4, 5] && (toVect taked) == [1, 2, 3]
+
+-- @@test IArray toLazy
+iLazy : IO Bool
+iLazy = do
+  let test_vect : Vect _ Nat = [1, 2, 3, 4, 5]
+  let test_array = fromVect test_vect
+  putStrLn "test_array: \{show test_array}"
+  let output_lazy = toLazy test_array
+  putStrLn "output_lazy: \{show output_lazy}"
+  pure $ vectLazy test_vect == output_lazy
+
+-- @@test IArray foldl/foldr
+iFold : IO Bool
+iFold = do
+  let test = fromVect [1, 2, 3, 4, 5]
+  putStrLn "test: \{show test}"
+  let foldl_test = foldl (flip (::)) [] test
+  putStrLn "foldl_test: \{show foldl_test}"
+  let foldr_test = foldr (::) [] test
+  putStrLn "foldr_test: \{show foldr_test}"
+  pure $ foldl_test == [5, 4, 3, 2, 1] && foldr_test == [1, 2, 3, 4, 5]
+
+-- @@test IArray functor
+iFunctor : IO Bool
+iFunctor = do
+  let test = fromVect [1, 2, 3, 4, 5]
+  putStrLn "test: \{show test}"
+  let output = map (+ 1) test
+  putStrLn "output: \{show output}"
+  pure $ toVect output == [2, 3, 4, 5, 6]
+  
+-- @@test IArray show
+iShow : IO Bool
+iShow = do
+  let test = fromVect [1, 2, 3, 4, 5]
+  putStrLn "test: \{show test}"
+  let empty : IArray _ Nat = fromVect []
+  putStrLn "empty: \{show empty}"
+  let singleton = fromVect [1]
+  putStrLn "singleton: \{show singleton}"
+  pure $ 
+    show test == "[1, 2, 3, 4, 5]"  
+    && show empty == "[]"  
+    && show singleton == "[1]"  
+
+-- @@test IArray monad
+iMonad : IO Bool
+iMonad = do
+  let test_vect : Vect 3 (Vect 3 Nat) = [[1, 2, 3], [4, 5, 6], [7, 8 ,9]]
+  let test_array = fromVect $ map fromVect test_vect
+  let vect_out = join test_vect
+  let array_out = join test_array
+  putStrLn "vect: \{show vect_out} array: \{show array_out}"
+  pure $ toVect array_out == vect_out
+```

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/Main.md

@@ -76,7 +76,7 @@ data Error : Type where
 A `Show` implementation for `Error` is provided, hidden in this document for
 brevity.
 
-<!-- idris
+```idris hide
 Show Error where
   show (OptionsError errs) =
     let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
@@ -98,7 +98,7 @@ Show Error where
   show (SolveError year day part err) =
     let err = unlines . map ("  " ++) . lines . show $ err
     in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
--->
+```
 
 ## Extract the year and day
 
@@ -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

src/Parser.md

@@ -0,0 +1,8 @@
+# Parsing Utilties
+
+```idris
+module Parser
+
+import public Parser.Interface as Parser
+import public Parser.ParserState as Parser
+```

src/Parser/Interface.md

@@ -0,0 +1,333 @@
+# The interface of a `Parser`
+
+```idris
+module Parser.Interface
+  
+import public Data.List1
+
+import public Parser.ParserState
+
+import public Control.Eff
+
+export infixr 4 >|
+export infixr 5 >&
+```
+
+## Parser Errors
+
+Combine the parser state at time of error with an error message.
+
+```idris
+public export
+data ParseError : Type where
+  -- TODO: Rename this constructor
+  MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
+  BeforeParse : (message : String) -> ParseError
+  NestedErrors : (state : ParserInternal Id) -> (message : String)
+    -> (rest : List ParseError) -> ParseError
+```
+
+```idris hide
+export
+Show ParseError where
+  show (MkParseError state message) = 
+    let (line, col) = positionPair state
+        (line, col) = (show line, show col)
+        position = show state.position.index
+    in "Error at line \{line}, column \{col} (\{position}): \{message}"
+  show (BeforeParse message) =
+    "Error before parsing: \{message}"
+  show (NestedErrors state message rest) = 
+    let rest = assert_total $joinBy "\n" . map (("  " ++) . show) $ rest
+        (line, col) = positionPair state
+        (line, col) = (show line, show col)
+        position = show state.position.index
+        first = "Error at line \{line}, column \{col} (\{position}): \{message}"
+    in "\{first}\n\{rest}"
+```
+
+## Type Alias
+
+```idris
+public export
+Parser : Type -> Type
+Parser a = Eff [ParserState, Except ParseError] a
+```
+
+## Error Generation
+
+Provide a few effectful actions to generate an error from an error message, and
+either return it or throw it.
+
+```idris
+export
+parseError : Has ParserState fs => (message : String) -> Eff fs ParseError
+parseError message = do
+  state <- save
+  pure $ MkParseError state message
+
+export
+throwParseError : Has ParserState fs => Has (Except ParseError) fs =>
+  (message : String) -> Eff fs a
+throwParseError message = do
+  err <- parseError message
+  throw err
+
+export
+guardMaybe : Has ParserState fs => Has (Except ParseError) fs =>
+  (message : String) -> Eff fs (Maybe a) -> Eff fs a
+guardMaybe message x = do
+  Just x <- x
+    | _ => throwParseError message
+  pure x
+
+export
+replaceError : (message : String) -> Parser (a -> Parser b)
+replaceError message = do
+  state <- save
+  pure (\_ => throw $ MkParseError state message)
+```
+
+## Running a parser
+
+We will use the phrasing "rundown" to refer to running all the effects in the
+parser effect stack except `ParserState`, which is left in the effect stack to
+facilitate handling in the context of another monad or effect stack, since it
+benefits from mutability.
+
+Rundown a parser, accepting the first returning parse, which may be failing or
+succeding, and automatically generating a "no valid parses" message in the event
+no paths in the `Choice` effect produce a returning parse.
+
+```idris
+export
+rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a)
+rundownFirst f = 
+  runExcept f
+```
+
+Provide wrappers for `rundownFirst` for evaluating it in various contexts.
+
+```idris
+export
+runFirstIO : HasIO io => MonadRec io =>
+  (f : Parser a) -> String -> io (Either ParseError a)
+runFirstIO f str = do
+  Just state <- newInternalIO str
+    | _ => pure . Left $ BeforeParse "Empty input"
+  runEff (rundownFirst f) [handleParserStateIO state]
+
+export
+runFirstIODebug : (f : Parser a) -> String -> IO (Either ParseError a)
+runFirstIODebug f str = do
+  Just state <- newInternalIO str
+    | _ => pure . Left $ BeforeParse "Empty input"
+  runEff (rundownFirst f) [handleParserStateIODebug state]
+
+export
+runFirst : (f : Parser a) -> String -> Eff fs (Either ParseError a)
+runFirst f str = do
+  Just state <- pure $ newInternal str
+    | _ => pure . Left $ BeforeParse "Empty input"
+  (result, _) <- lift . runParserState state . rundownFirst $ f
+  pure result
+
+export
+runFirst' : (f : Parser a) -> String -> Either ParseError a
+runFirst' f str = extract $ runFirst f str {fs = []}
+```
+
+## Utility functionality
+
+### Parser combinators
+
+Try to run a computation in the context of the `Parser` effect stack, if it
+fails (via `Except`), reset the state and resort to the supplied callback
+
+Also supply a version specialized to ignore the error value, returning `Just a`
+if the parse succeeds, and `Nothing` if it fails.
+
+```idris
+export
+try : (f : Parser a) -> (err : ParseError -> Parser a) -> Parser a
+try f err = do
+  starting_state <- save
+  result <- lift . runExcept $ f
+  case result of
+    Left error => do
+      load starting_state
+      err error 
+    Right result => pure result
+
+export
+tryMaybe : (f : Parser a) -> Parser (Maybe a)
+tryMaybe f = try (map Just f) (\_ => pure Nothing)
+  
+export
+tryEither : (f : Parser a) -> Parser (Either ParseError a)
+tryEither f = try (map Right f) (pure . Left)
+```
+
+Attempt to parse one of the given input parsers, in the provided order, invoking
+the provided error action on failure.
+
+The state will not be modified when an input parser fails
+
+```idris
+export
+oneOfE : (err : String) -> List (Parser a) -> Parser a
+oneOfE err xs = do
+  start <- save
+  oneOfE' err start [] xs
+  where
+    oneOfE' : (err : String) -> (start : ParserInternal Id) 
+      -> (errs : List ParseError) -> List (Parser a) -> Parser a
+    oneOfE' err start errs [] = do
+      throw $ NestedErrors start err (reverse errs) 
+    oneOfE' err start errs (x :: xs) = do
+      x <- tryEither x
+      case x of
+        Right val => pure val
+        Left error => oneOfE' err start (error :: errs) xs
+```
+
+Attempt to parse 0+ of an item
+
+```idris
+export
+many : (f : Parser a) -> Parser (List a)
+many f = do
+  Just next <- tryMaybe f
+    | _ => pure []
+  map (next ::) $ many f
+```
+
+Attempt to parse 1+ of an item, invoking the supplied error action on failure
+
+```idris
+export
+atLeastOne : (err : ParseError -> Parser (List1 a)) -> (f : Parser a)
+  -> Parser (List1 a)
+atLeastOne err f = do
+  Right next <- tryEither f
+    | Left e => err e
+  map (next :::) $ many f
+```
+
+Lift a parser producing a `List` or `List1` of `Char` into a parser producing a
+`String`
+
+```idris
+-- TODO: Rename these
+export
+liftString : Parser (List Char) -> Parser String
+liftString x = do
+  xs <- x
+  pure $ pack xs
+
+export
+liftString' : Parser (List1 Char) -> Parser String
+liftString' x = liftString $ map forget x
+```
+
+Attempt to parse a specified character
+
+```idris
+export
+charExact : Char -> Parser Char
+charExact c = do
+  result <- charExact' c
+  case result of
+    GotChar char => pure char
+    GotError err => throwParseError "Got \{show err} Expected \{show c}"
+    EndOfInput => throwParseError "End of input"
+```
+
+Attempt to parse one of a list of chars
+
+```idris
+export
+theseChars : List Char -> Parser Char
+theseChars cs = do
+  pnote "Parsing one of: \{show cs}"
+  result <- charPredicate (\x => any (== x) cs)
+  case result of
+    GotChar char => pure char
+    GotError err => throwParseError "Got \{show err} Expected one of \{show cs}"
+    EndOfInput => throwParseError "End of input"
+```
+
+Attempt to parse an exact string
+
+```idris
+export
+exactString : String -> Parser String
+exactString str with (asList str)
+  exactString "" | [] = do
+    pnote "Parsing the empty string"
+    pure ""
+  exactString input@(strCons c str) | (c :: x) = do
+    pnote "Parsing exact string \{show input}"
+    GotChar next <- charPredicate (== c)
+      | GotError err => throwParseError "Got \{show err} expected \{show c}"
+      | EndOfInput => throwParseError "End of input"
+    rest <- exactString str | x
+    pure input
+```
+
+Wrap a parser in delimiter characters, discarding the value of the delimiters
+
+```idris
+export
+delimited : (before, after : Char) -> Parser a -> Parser a
+delimited before after x = do
+  pnote "Parsing delimited by \{show before} \{show after}"
+  starting_state <- save
+  _ <- charExact before
+  Right val <- tryEither x
+    | Left err => do
+      load starting_state
+      throw err
+  Just _ <- tryMaybe $ charExact after
+    | _ => do
+      load starting_state
+      throw $ MkParseError starting_state "Unmatched delimiter \{show before}"
+  pure val
+```
+
+Consume any number of characters of the provided character class and discard the
+result. Also a version for doing so on both sides of a provided parser
+
+```idris
+export
+nom : Parser Char -> Parser ()
+nom x = do
+  pnote "Nomming"
+  _ <- many x
+  pure ()
+
+export
+surround : (around : Parser Char) -> (item : Parser a) -> Parser a
+surround around item = do
+  pnote "Surrounding"
+  nom around
+  val <- item
+  nom around
+  pure val
+```
+
+### Composition of boolean functions
+
+```idris
+||| Return true if both of the predicates evaluate to true
+public export
+(>&) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool)
+(>&) a b x = a x && b x 
+```
+
+```idris
+||| Return true if either of the predicates evaulates to true
+public export
+(>|) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool)
+(>|) a b x = a x || b x 
+```

src/Parser/JSON.md

@@ -0,0 +1,380 @@
+# JSON Parser
+
+```idris
+module Parser.JSON
+
+import public Parser
+import public Parser.Numbers
+
+import Control.Monad.Eval
+
+import Structures.Dependent.DList
+```
+
+```idris hide
+import System
+import Derive.Prelude
+import Generics.Derive
+
+%hide Generics.Derive.Eq
+%hide Generics.Derive.Ord
+%hide Generics.Derive.Show
+
+%language ElabReflection
+```
+
+## JSON components
+
+Types a JSON value is allowed to have
+
+```idris
+public export
+data JSONType : Type where
+  TObject : JSONType
+  TArray : JSONType
+  TString : JSONType
+  TNumber : JSONType
+  TBool : JSONType
+  TNull : JSONType
+%runElab derive "JSONType" [Generic, Meta, Eq, Ord, Show, DecEq]
+%name JSONType type, type2, type3
+```
+
+A JSON value indexed by its type
+
+```idris
+public export
+data JSONValue : JSONType -> Type where
+  VObject : {types : List JSONType} 
+    -> DList JSONType (\t => (String, JSONValue t)) types -> JSONValue TObject
+  VArray : {types : List JSONType}
+    -> DList JSONType JSONValue types -> JSONValue TArray
+  VString : (s : String) -> JSONValue TString
+  VNumber : (d : Double) -> JSONValue TNumber
+  VBool : (b : Bool) -> JSONValue TBool
+  VNull : JSONValue TNull
+%name JSONValue value, value2, value3
+```
+
+```idris hide
+export
+Show (JSONValue t) where
+  show (VObject xs) = 
+    let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
+    in assert_total $ "{\{joinBy "," xs}}"
+  show (VArray xs) = 
+    let xs = dMap (\_,e => show e) xs
+    in assert_total $ "[\{joinBy "," xs}]"
+  show (VString s) = "\"\{s}\""
+  show (VNumber d) = show d
+  show (VBool False) = "false"
+  show (VBool True) = "true"
+  show VNull = "null"
+
+-- TODO: Deal with keys potentially having different orders in different objects
+export
+Eq (JSONValue t) where
+  (VObject xs) == (VObject ys) = 
+    assert_total $ xs $== ys
+  (VArray xs) == (VArray ys) = 
+    assert_total $ xs $== ys
+  (VString s) == (VString str) = s == str
+  (VNumber d) == (VNumber dbl) = d == dbl
+  (VBool b) == (VBool x) = b == x
+  VNull == VNull = True
+
+%hide Language.Reflection.TT.WithFC.value
+```
+
+### JSON Functions
+
+`foldl` Analog for consuming a JSON structure by values. Ignores the keys in
+objects.
+
+```idris
+export
+dFoldL : {t : JSONType} 
+  -> (acc -> (type : JSONType) -> (val : JSONValue type) -> acc) 
+  -> acc -> JSONValue t -> acc
+dFoldL f acc' (VObject xs) = 
+  let recur : acc -> (v : JSONType) -> (String, JSONValue v) -> acc
+      recur acc' v (key, value) = dFoldL f acc' value
+  in DList.dFoldL recur acc' xs
+dFoldL f acc' (VArray xs) = 
+  let recur : acc -> (v : JSONType) -> JSONValue v -> acc
+      recur acc' v value = dFoldL f acc' value
+  in DList.dFoldL recur acc' xs
+dFoldL f acc (VString s) = f acc _ (VString s)
+dFoldL f acc (VNumber d) = f acc _ (VNumber d)
+dFoldL f acc (VBool b) = f acc _ (VBool b)
+dFoldL f acc VNull = f acc _ VNull
+```
+
+Look up a property in an object
+
+```idris
+export
+getProperty : (prop : String) -> (object : JSONValue TObject)
+  -> Maybe (type : JSONType ** JSONValue type)
+getProperty prop (VObject xs) = 
+  case dFind (\_, (key, _) => key == prop) xs of
+    Nothing => Nothing
+    Just (type ** (_, val)) => Just (type ** val)
+```
+
+Return the values from an object.
+
+```idris
+export
+getValues : (object : JSONValue TObject) 
+  -> (types : List JSONType ** DList JSONType JSONValue types)
+getValues (VObject xs) = 
+  dMap' (\t, (k, v) => (t ** v)) xs
+```
+
+Recursively apply a filter to a JSON structure.
+
+```idris
+export
+dFilter : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
+  -> {t : JSONType} -> JSONValue t -> Maybe (JSONValue t)
+dFilter f value = eval $ dFilter' f value
+  where
+    dFilter' : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) 
+      -> {t : JSONType} -> JSONValue t -> Eval $ Maybe (JSONValue t)
+    dFilter' f (VObject xs) = do
+      True <- pure $ f _ (VObject xs)
+        | _ => pure Nothing
+      let xs = toList xs
+      xs : List (Maybe (x : JSONType ** (String, JSONValue x))) <- 
+        traverse
+          (\(t ** (k, v)) => do
+            Just v <- dFilter' f v
+              | _ => pure Nothing
+            pure $ Just (t ** (k, v)))
+          xs
+      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
+        fromList $ catMaybes xs
+      pure . Just $ VObject xs
+    dFilter' f (VArray xs) = do 
+      True <- pure $ f _ (VArray xs)
+        | _ => pure Nothing
+      let xs = toList xs
+      xs : List (Maybe (x : JSONType ** JSONValue x)) <- 
+        traverse
+          (\(t ** v) => do
+            Just v <- dFilter' f v
+              | _ => pure Nothing
+            pure $ Just (t ** v))
+          xs
+      let (_ ** xs) : (t : List JSONType ** DList _ _ t) = 
+        fromList $ catMaybes xs
+      pure . Just $ VArray xs
+    dFilter' f x =
+      pure $ case f _ x of
+        False => Nothing
+        True => Just x
+```
+
+## Parsers
+
+We are going to get mutually recursive here. Instead of using a `mutual` block,
+we will use the more modern style of declaring all our types ahead of our
+definitions.
+
+```idris
+export
+object : Parser (JSONValue TObject)
+export
+array : Parser (JSONValue TArray)
+export
+string : Parser (JSONValue TString)
+export
+number : Parser (JSONValue TNumber)
+export
+bool : Parser (JSONValue TBool)
+export
+null : Parser (JSONValue TNull)
+```
+
+Define a `whitespace` character class based on the json specifications
+
+```idris
+whitespace : Parser Char
+whitespace = do
+  pnote "Whitespace character"
+  theseChars [' ', '\n', '\r', '\t']
+```
+
+Convenience function
+
+```idris
+dpairize : {t : JSONType} -> 
+  Parser (JSONValue t) -> Parser (t' : JSONType ** JSONValue t')
+dpairize x = do
+  x <- x
+  pure (_ ** x)
+```
+
+Top level json value parser
+
+```idris
+export 
+value : Parser (t : JSONType ** JSONValue t)
+value = do 
+  pnote "JSON Value"
+  surround whitespace $ oneOfE 
+    "Expected JSON Value" 
+    [
+      dpairize object
+    , dpairize array
+    , dpairize string
+    , dpairize number
+    , dpairize bool
+    , dpairize null
+    ]
+```
+
+Now go through our json value types
+
+```idris
+object = do
+  pnote "JSON Object"
+  oneOfE 
+    "Expected Object" 
+    [emptyObject, occupiedObject]
+  where
+    emptyObject : Parser (JSONValue TObject)
+    emptyObject = do
+      delimited '{' '}' (nom whitespace)
+      pure $ VObject Nil
+    keyValue : Parser (t : JSONType ** (String, JSONValue t))
+    keyValue = do
+      VString key <- surround whitespace string
+      _ <- charExact ':'
+      (typ ** val) <- value
+      pure (typ ** (key, val))
+    restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
+    restKeyValue = do
+      _ <- charExact ','
+      keyValue
+    pairs : Parser (List1 (t : JSONType ** (String, JSONValue t)))
+    pairs = do
+      first <- keyValue
+      rest <- many restKeyValue
+      -- TODO: headTail combinator for this
+      pure $ first ::: rest
+    occupiedObject : Parser (JSONValue TObject)
+    occupiedObject = do
+      val <- delimited '{' '}' pairs
+      let (types ** xs) = DList.fromList (forget val)
+      pure $ VObject xs
+```
+
+```idris
+array = do
+  pnote "JSON Array"
+  oneOfE 
+    "Expected Array" 
+    [emptyArray, occupiedArray]
+  where
+    emptyArray : Parser (JSONValue TArray)
+    emptyArray = do
+      delimited '[' ']' (nom whitespace)
+      pure $ VArray Nil
+    restValue : Parser (t : JSONType ** JSONValue t)
+    restValue = do
+      _ <- charExact ','
+      value
+    values : Parser (List1 (t : JSONType ** JSONValue t))
+    values = do
+      first <- value
+      rest <- many restValue
+      pure $ first ::: rest 
+    occupiedArray : Parser (JSONValue TArray)
+    occupiedArray = do
+      xs <- delimited '[' ']' values
+      let (types ** xs) = DList.fromList (forget xs)
+      pure $ VArray xs
+```
+
+```idris
+string = do
+  pnote "JSON String"
+  str <- liftString $ delimited '"' '"' (many stringCharacter)
+  pure $ VString str
+  where
+    -- TODO: Handle control characters properly
+    stringCharacter : Parser Char
+    stringCharacter = do
+      result <- charPredicate (not . (== '"'))
+      case result of
+        GotChar char => pure char
+        GotError err =>
+          throwParseError "Expected string character, got \{show err}"
+        EndOfInput => throwParseError "Unexpected end of input"
+```
+
+```idris
+number = do
+  pnote "JSON Number"
+  d <- double
+  pure $ VNumber d
+```
+
+```idris
+bool = do
+  pnote "JSON Bool"
+  oneOfE
+    "Expected Bool"
+    [true, false]
+  where
+    true : Parser (JSONValue TBool)
+    true = do
+      _ <- exactString "true" 
+      pure $ VBool True
+    false : Parser (JSONValue TBool)
+    false = do
+      _ <- exactString "false" 
+      pure $ VBool False
+```
+
+```idris
+null = do
+  pnote "JSON null"
+  _ <- exactString "null"
+  pure VNull
+```
+
+## Unit tests
+
+Quick smoke test
+
+```idris
+-- @@test JSON Quick Smoke
+quickSmoke : IO Bool
+quickSmoke = do
+  let input = "{\"string\":\"string\",\"number\":5,\"true\":true,\"false\":false,\"null\":null,\"array\":[1,2,3]}"
+  putStrLn input
+  Right (type ** parsed) <- runFirstIODebug value input
+    | Left err => do
+      printLn err
+      pure False
+  putStrLn "Input: \{input}\nOutput: \{show type} -> \{show parsed}"
+  let reference_object = 
+    VObject [
+      ("string", VString "string")
+    , ("number", VNumber 5.0)
+    , ("true", VBool True)
+    , ("false", VBool False)
+    , ("null", VNull)
+    , ("array", VArray [
+        VNumber 1.0
+      , VNumber 2.0
+      , VNumber 3.0
+      ])
+    ]
+  case type of
+    TObject => pure $ parsed == reference_object
+    _ => pure False
+```

src/Parser/Numbers.md

@@ -0,0 +1,257 @@
+# Numerical Parsers
+
+```idris
+module Parser.Numbers
+  
+import public Parser
+
+import Data.Vect
+import Control.Eff
+```
+
+```idris hide
+import System
+```
+
+## Base Abstraction
+
+```idris
+public export
+record Base where
+  constructor MkBase
+  base : Nat
+  digits : Vect base Char
+%name Base b
+
+export
+hasDigit : Base -> Char -> Bool
+hasDigit (MkBase base digits) c = any (== c) digits
+
+export
+digitValue : Base -> Char -> Maybe Nat
+digitValue (MkBase base digits) c = digitValue' digits 0
+  where
+  digitValue' : Vect n Char -> (idx : Nat) -> Maybe Nat
+  digitValue' [] idx = Nothing
+  digitValue' (x :: xs) idx = 
+    if x == c
+    then Just idx
+    else digitValue' xs (S idx)
+
+public export
+base10 : Base
+base10 = MkBase 10 
+  ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9'] 
+
+public export
+hex : Base
+hex = MkBase 16 
+  ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f'] 
+```
+
+## Parsers
+
+### Nat
+
+```idris
+export
+nat : Base -> Parser Nat
+nat b = do
+  error <- replaceError "Expected digit"
+  (first ::: rest) <- atLeastOne error parseDigit
+  pure $ foldl (\acc, e => 10 * acc + e) first rest
+  where
+    parseDigit : Parser Nat
+    parseDigit = do
+      GotChar char <- charPredicate (hasDigit b)
+        | GotError e => throwParseError "\{show e} is not a digit"
+        | EndOfInput => throwParseError "End Of Input"
+      case digitValue b char of
+        Nothing =>
+          throwParseError "Failed to parse as base \{show b.base}: \{show char}"
+        Just x => pure x
+
+export
+natBase10 : Parser Nat
+natBase10 = nat base10
+```
+
+### Integer
+
+```idris
+export
+integer : Base -> Parser Integer
+integer b = do
+  negative <- map isJust . tryMaybe $ charExact '-'
+  value <- map natToInteger $ nat b
+  if negative
+    then pure $ negate value
+    else pure $ value
+
+export
+integerBase10 : Parser Integer
+integerBase10 = integer base10
+```
+
+### Double
+
+```idris
+-- TODO: Replicate `parseDouble` logic and make this base-generic
+export
+double : Parser Double
+double = do
+  starting_state <- save
+  integer <- integer
+  fraction <- tryMaybe fraction
+  exponent <- tryMaybe exponent
+  let str = case (fraction, exponent) of
+       (Nothing, Nothing) => 
+         integer
+       (Nothing, (Just exponent)) => 
+         "\{integer}e\{exponent}"
+       ((Just fraction), Nothing) => 
+         "\{integer}.\{fraction}"
+       ((Just fraction), (Just exponent)) => 
+         "\{integer}.\{fraction}e\{exponent}"
+  Just out <- pure $ parseDouble str
+    | _ => 
+      throw $ MkParseError starting_state "Std failed to parse as double: \{str}"
+  pure out
+  where
+    parseDigit : Parser Char
+    parseDigit = do
+      GotChar char <- charPredicate (hasDigit base10)
+        | GotError e => throwParseError "\{show e} is not a digit"
+        | EndOfInput => throwParseError "End Of Input"
+      pure char
+    integer : Parser String
+    integer = do
+      sign <- tryMaybe $ charExact '-'
+      error <- replaceError "Expected digit"
+      digits <- map forget $ atLeastOne error parseDigit
+      case sign of
+        Nothing => pure $ pack digits
+        Just x => pure $ pack (x :: digits)
+    fraction : Parser String
+    fraction = do
+      decimal <- charExact '.'
+      error <- replaceError "Expected digit"
+      digits <- map forget $ atLeastOne error parseDigit
+      pure $ pack digits
+    exponent : Parser String
+    exponent = do
+      e <- theseChars ['e', 'E']
+      sign <- theseChars ['+', '-']
+      error <- replaceError "Expected digit"
+      digits <- map forget $ atLeastOne error parseDigit
+      pure . pack $ sign :: digits
+```
+
+## Unit tests
+
+Test roundtripping a value through the provided parser
+
+```idris
+roundtrip : Eq a => Show a => a -> (p : Parser a) -> IO Bool
+roundtrip x p = do
+  let string = show x
+  putStrLn "Roundtripping \{string}"
+  Just state <- newInternalIO string
+    | _ => do
+      putStrLn "Failed to produce parser for \{string}"
+      pure False
+  Right result <- runEff (rundownFirst p) [handleParserStateIO state] {m = IO}
+    | Left err => do
+      printLn err
+      pure False
+  putStrLn "Input: \{string} Output: \{show result}"
+  pure $ x == result
+```
+
+Do some roundtrip tests with the nat parser
+
+```idris
+-- @@test Nat round trip
+natRoundTrip : IO Bool
+natRoundTrip = pure $ 
+  !(roundtrip 0 natBase10) 
+  && !(roundtrip 1 natBase10) 
+  && !(roundtrip 100 natBase10) 
+  && !(roundtrip 1234 natBase10) 
+  && !(roundtrip 1234567890 natBase10) 
+  && !(roundtrip 1234567890000 natBase10) 
+  && !(roundtrip 12345678901234567890 natBase10) 
+```
+
+```idris
+-- @@test Integer round trip
+integerRoundTrip : IO Bool
+integerRoundTrip = pure $ 
+  !(roundtrip 0 integerBase10) 
+  && !(roundtrip 1 integerBase10) 
+  && !(roundtrip 100 integerBase10) 
+  && !(roundtrip 1234 integerBase10) 
+  && !(roundtrip 1234567890 integerBase10) 
+  && !(roundtrip 1234567890000 integerBase10) 
+  && !(roundtrip 12345678901234567890 integerBase10) 
+  && !(roundtrip (-1) integerBase10) 
+  && !(roundtrip (-100) integerBase10) 
+  && !(roundtrip (-1234) integerBase10) 
+  && !(roundtrip (-1234567890) integerBase10) 
+  && !(roundtrip (-1234567890000) integerBase10) 
+  && !(roundtrip (-12345678901234567890) integerBase10) 
+```
+
+Compare our parsing of a double to the standard library's
+
+```idris
+compareDouble : String -> IO Bool
+compareDouble string = do
+  Just state <- newInternalIO string
+    | _ => do
+      putStrLn "Failed to produce parser for \{string}"
+      pure False
+  Right result <- 
+    runEff (rundownFirst double) [handleParserStateIO state] {m = IO}
+    | Left err => do
+      printLn err
+      pure False
+  putStrLn "Input: \{string} Output: \{show result}"
+  Just double' <- pure $ parseDouble string
+    | _ => do
+      printLn "Std failed to parse as double: \{string}"
+      pure False
+  pure $ result == double'
+```
+
+```idris
+-- @@test Double Std Comparison 
+doubleRoundTrip : IO Bool
+doubleRoundTrip = pure $ 
+  !(compareDouble "0") 
+  && !(compareDouble "1") 
+  && !(compareDouble "100") 
+  && !(compareDouble "1234") 
+  && !(compareDouble "1234567890") 
+  && !(compareDouble "1234567890000") 
+  && !(compareDouble "12345678901234567890") 
+  && !(compareDouble "-1") 
+  && !(compareDouble "-100") 
+  && !(compareDouble "-1234") 
+  && !(compareDouble "-1234567890") 
+  && !(compareDouble "-1234567890000") 
+  && !(compareDouble "-12345678901234567890") 
+  && !(compareDouble "0.0") 
+  && !(compareDouble "1.0") 
+  && !(compareDouble "-1.0") 
+  && !(compareDouble "-0.0") 
+  && !(compareDouble "-0.0") 
+  && !(compareDouble "0.1234") 
+  && !(compareDouble "0.01234") 
+  && !(compareDouble "-0.1234") 
+  && !(compareDouble "-0.01234") 
+  && !(compareDouble "1.234e+5") 
+  && !(compareDouble "1.234e-5") 
+  && !(compareDouble "-1.234e+5") 
+  && !(compareDouble "-1.234e-5") 
+```

src/Parser/ParserState.md

@@ -0,0 +1,369 @@
+# Parser State
+
+An effectful description of the text a parser consumes
+
+```idris
+module Parser.ParserState
+
+import public Data.String
+import public Data.DPair
+import public Data.Refined
+import public Data.Refined.Int64
+import public Data.SortedMap
+import public Data.IORef
+
+import Data.Primitives.Interpolation
+import System.File
+
+import public Control.Eff
+```
+
+## Barbie Basics
+
+Barbies are types that can "change their clothes", in Idris, this manifests as a
+type indexed by a type-level function that affects the types of the fields.
+
+Since we know our usage here is going to be quite simple, and not even really
+making use of dependently typed fun, we are going to implement all the barbie
+functionality we need by hand, but if you feel like barbies might be a good fit
+for your problem, or you simply want to learn more, please check out a library
+like `barbies`[^1]
+
+```idris
+public export
+Id : Type -> Type
+Id x = x
+```
+
+## Internal State of a Parser
+
+Type alias for our refined `Int64`s
+
+```idris
+public export
+0 IsIndex : (length : Int64) -> Int64 -> Type
+IsIndex length = From 0 && LessThan length 
+
+public export
+record Index (length : Int64) where
+  constructor MkIndex
+  index : Int64
+  {auto 0 prf : IsIndex length index}
+```
+
+```idris hide
+export
+Eq (Index i) where
+  x == y = x.index == y.index
+
+export
+Ord (Index i) where
+  compare x y = compare x.index y.index
+
+export
+Show (Index i) where
+  show (MkIndex index) = show index
+```
+
+Stores the location we are currently at in the string, and metadata about it for
+providing good error messages. Parsing an empty input isn't very interesting, so
+we exclude inputs of length zero, since that will make other things easier.
+
+```idris
+||| State representing a parser's position in the text
+public export
+record ParserInternal (f : Type -> Type) where
+  constructor MkInternal
+  -- IDEA: Maybe go full barbie and have this be a field, so that we can, say,
+  -- read directly from a file instead of from an already loaded string using the
+  -- same parser
+  ||| The input string
+  input : String
+  ||| The length of the input string
+  length : Int64
+  {auto 0 len_prf : length = cast (strLength input)}
+  ||| A sorted set containing the positions of the start of each line
+  line_starts : SortedMap (Index length) Nat
+  ||| The position of the next character to read in the input
+  position : f (Index length) 
+  ||| True if we have hit the end of input
+  end_of_input : f Bool
+%name ParserInternal pi, pj, pk
+```
+
+### ParserInternal Methods
+
+Construct a `ParserInternal` from an input string. Will fail if the input is
+empty, because then we can't index it.
+
+```idris
+export
+newInternal : (input : String) -> Maybe (ParserInternal Id)
+newInternal input = 
+  -- Check if we have at least one character in the input
+  case refine0 0 {p = IsIndex (cast (strLength input))} of
+    Nothing => Nothing
+    Just (Element position _) => Just $ 
+      MkInternal input 
+                 (cast (strLength input)) 
+                 (mkStarts' input (MkIndex position)) 
+                 (MkIndex position) 
+                 False
+  where
+    partial
+    mkStarts : 
+      (str : String) -> (acc : List (Index (cast (strLength str)), Nat))
+      -> (idx : Index (cast (strLength str))) -> (count : Nat) -> (next : Bool)
+      -> List (Index (cast (strLength str)), Nat)
+    mkStarts str acc idx count True = 
+      mkStarts str ((idx, count) :: acc) idx (S count) False
+    mkStarts str acc idx count False = 
+      case refine0 (idx.index + 1) {p = IsIndex (cast (strLength str))} of
+        Nothing => acc
+        Just (Element next _) => 
+          if strIndex str (cast idx.index) == '\n'
+            then mkStarts str acc (MkIndex next) count True
+            else mkStarts str acc (MkIndex next) count False
+    mkStarts' : (str : String) -> (start : Index (cast (strLength str)))
+      -> SortedMap (Index (cast (strLength str))) Nat
+    mkStarts' str start = 
+      let 
+        pairs = assert_total $ 
+          mkStarts str [] start 0 True
+      in fromList pairs
+```
+
+Get the current line and column number
+
+```idris
+||| Returns the current position of the parser cursor in, zero indexed, (line, 
+||| column) form
+export
+positionPair : (pi : ParserInternal Id) -> (Nat, Nat)
+positionPair pi = 
+  case lookup pi.position pi.line_starts of
+    Just line => (line, 0)
+    Nothing => 
+      case lookupBetween pi.position pi.line_starts of
+        -- There will always be at least one line start, and we would have hit
+        -- the previous case if we were at the start of the first one, so if
+        -- there isn't a before, we can return a nonsense value safely
+        (Nothing, _) => (0, 0)
+        (Just (start, linum), after) => 
+          -- Our index will always be after the start of the line, for previously
+          -- mentioned reasons, so this cast is safe
+          let col = cast {to = Nat} $ pi.position.index - start.index
+          in (linum, col)
+```
+
+```idris hide
+export
+Show (ParserInternal Id) where
+  show pi = 
+    let (line, col) = positionPair pi
+        current = assert_total $ strIndex pi.input (cast pi.position.index) 
+        pos = pi.position.index
+        eof = show pi.end_of_input
+    in "Position: \{pos}(\{line}, \{col}}) Value: \{show current} EoF: \{eof}"
+```
+
+### More Barbie Functionality
+
+Provide the barbie analogs of `map` and `traverse` for our `ParserInternal`
+type, allowing us to change the type the values in a `ParserInternal` by mapping
+over those values.
+
+```idris
+export
+bmap : ({0 a : Type} -> f a -> g a) -> ParserInternal f -> ParserInternal g
+-- bmap f = bmap_ (\_ => f)
+bmap fun (MkInternal input length line_starts position end_of_input) = 
+  let position' = fun position
+      end_of_input' = fun end_of_input 
+  in MkInternal input length line_starts position' end_of_input'
+
+export
+btraverse : Applicative e => ({0 a : Type} -> f a -> e (g a)) 
+  -> ParserInternal f -> e (ParserInternal g)
+btraverse fun (MkInternal input length line_starts position end_of_input) = 
+  let pures = (MkInternal input length line_starts)
+  in [| pures (fun position) (fun end_of_input)|]
+```
+
+## Three way result
+
+```idris
+||| Three way result returned from attempting to parse a single char
+public export
+data ParseCharResult : Type where
+  GotChar : (char : Char) -> ParseCharResult
+  GotError : (err : Char) -> ParseCharResult
+  EndOfInput : ParseCharResult
+```
+
+## The Effect Type
+
+```idris
+export
+data ParserState : Type -> Type where
+  Save : ParserState (ParserInternal Id)
+  Load : (ParserInternal Id) -> ParserState ()
+  -- TODO: Maybe add a ParseString that parses a string of characters as a 
+  -- string using efficent slicing?
+  ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult
+  ParseExactChar : (char : Char) -> ParserState ParseCharResult
+  ParseEoF : ParserState Bool
+  Note : Lazy String -> ParserState ()
+```
+
+```idris hide
+Show (ParserState t) where
+  show Save = "Saving state"
+  show (Load pi) = "Loading state \{show pi}"
+  show (ParseChar predicate) = "Parsing char"
+  show (ParseExactChar char) = "Parsing char \{show char}"
+  show ParseEoF = "Parsing EoF"
+  show (Note _) = "Note"
+```
+
+### Actions
+
+```idris
+||| Return the current state, for potential later reloading
+export
+save : Has ParserState fs => Eff fs (ParserInternal Id)
+save = send Save
+
+||| Reset to the provided state
+export
+load : Has ParserState fs => ParserInternal Id -> Eff fs ()
+load pi = send $ Load pi
+
+||| Attempt to parse a char, checking to see if it complies with the supplied 
+||| predicate, updates the state if parsing succeeds, does not alter it in an 
+||| error condition.
+export 
+charPredicate : Has ParserState fs => (predicate : Char -> Bool)
+  -> Eff fs ParseCharResult
+charPredicate predicate = send $ ParseChar predicate 
+
+||| Parse a char by exact value
+export 
+charExact' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult
+charExact' chr = send $ ParseExactChar chr
+
+||| "Parse" the end of input, returning `True` if the parser state is currently
+||| at the end of the input
+export
+parseEoF : Has ParserState fs => Eff fs Bool
+parseEoF = send ParseEoF
+
+||| Make a note to be output when running with a debug handler
+export
+pnote : Has ParserState fs => Lazy String -> Eff fs ()
+pnote x = send $ Note x
+```
+
+## Handling a ParserState
+
+### IO Context
+
+```idris
+export
+handleParserStateIO : HasIO io => 
+  IORef (ParserInternal IORef) -> ParserState t -> io t
+handleParserStateIO pi Save = do
+  pi <- readIORef pi
+  btraverse readIORef pi
+handleParserStateIO pi (Load pj) = do
+  pj <- btraverse newIORef pj
+  writeIORef pi pj
+handleParserStateIO pi (ParseChar predicate) = do
+  pi <- readIORef pi
+  False <- readIORef pi.end_of_input
+    | _ => pure EndOfInput
+  position <- readIORef pi.position
+  let char = assert_total $ strIndex pi.input (cast position.index)
+  True <- pure $ predicate char
+    | _ => pure $ GotError char
+  -- Our refinement type on the position forces us to check that the length is
+  -- in bounds after incrementing it, if its out of bounds, set the end_of_input
+  -- flag
+  case refine0 (position.index + 1) {p = IsIndex pi.length} of
+    Nothing => do
+      writeIORef pi.end_of_input True
+      pure $ GotChar char
+    Just (Element next _) => do
+      writeIORef pi.position $ MkIndex next
+      pure $ GotChar char
+handleParserStateIO pi (ParseExactChar chr) = do
+  -- TODO: do this directly?
+  handleParserStateIO pi (ParseChar (== chr))
+handleParserStateIO pi ParseEoF = do
+  pi <- readIORef pi
+  readIORef pi.end_of_input
+-- We ignore notes in non-debug mode
+handleParserStateIO pi (Note _) = pure ()
+
+export
+newInternalIO : HasIO io => String -> io $ Maybe (IORef (ParserInternal IORef))
+newInternalIO str = do
+  Just internal <- pure $ newInternal str
+    | _ => pure Nothing
+  internal <- btraverse newIORef internal
+  map Just $ newIORef internal
+```
+
+Wrapper with debugging output
+
+```idris
+export
+handleParserStateIODebug : HasIO io => 
+  IORef (ParserInternal IORef) -> ParserState t -> io t
+handleParserStateIODebug x (Note note) = do
+  state <- readIORef x
+  state <- btraverse readIORef state
+  _ <- fPutStrLn stderr "Note \{note} -> \{show state}"
+  pure ()
+handleParserStateIODebug x y = do
+  state <- readIORef x
+  state <- btraverse readIORef state
+  _ <- fPutStrLn stderr "\{show y} -> \{show state}"
+  handleParserStateIO x y
+```
+
+### State context
+
+```idris
+unPS : ParserInternal Id -> ParserState a -> (a, ParserInternal Id)
+unPS pi Save = (pi, pi)
+unPS pi (Load pj) = ((), pi)
+unPS pi (ParseChar predicate) = 
+  if pi.end_of_input
+    then (EndOfInput, pi)
+    else let
+      char = assert_total $ strIndex pi.input (cast pi.position.index)
+    in if predicate char
+      then case refine0 (pi.position.index + 1) {p = IsIndex pi.length} of
+        Nothing => 
+          (GotChar char, {end_of_input := True} pi)
+        Just (Element next _) => 
+          (GotChar char, {position := MkIndex next} pi)
+      else (GotError char, pi)
+unPS pi (ParseExactChar chr) = unPS pi (ParseChar (== chr))
+unPS pi ParseEoF = (pi.end_of_input, pi)
+unPS pi (Note _) = ((), pi)
+
+export
+runParserState : Has ParserState fs => 
+  (s : ParserInternal Id) -> Eff fs t 
+  -> Eff (fs - ParserState) (t, ParserInternal Id)
+runParserState s = 
+  handleRelayS s (\x, y => pure (y, x)) $ \s2,ps,f =>
+    let (a, st) = unPS s2 ps 
+    in f st a
+```
+
+## Footnotes
+
+[^1]: <https://github.com/stefan-hoeck/idris2-barbies>

src/README.md

@@ -0,0 +1 @@
+../README.md

src/Runner.md

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

src/SUMMARY.md

@@ -0,0 +1,37 @@
+# Summary
+
+[README](README.md)
+
+# Running the code
+
+- [Runner - Divide Code Into Years and Days](Runner.md)
+- [Main - Select a Day and Year to Run](Main.md)
+
+# Utility Mini-Library
+
+- [Util - Extend Standard Types](Util.md)
+  - [Util.Eff - Effects and Effect Accessories](Util/Eff.md)
+  - [Util.Digits - Pattern Matching Integers as Lists of Digits](Util/Eff.md)
+- [Array - Arrays With Constant Time Indexing and Slicing](Array.md)
+- [Parser - Recursive Descent Parsing, With Effects](Parser.md)
+  - [Interface - Core Parsing Functionality](Parser/Interface.md)
+  - [ParserState - Custom Effect for Parser Internal State](Parser/ParserState.md)
+  - [Numbers - Parsers for Numerical Values](Parser/Numbers.md)
+  - [JSON - A JSON Parser](Parser/JSON.md)
+
+# Problems
+
+- [2015](Years/Y2015.md)
+  - [Day 1 - Warmup](Years/Y2015/Day1.md)
+  - [Day 2 - Early Effectful Parsing](Years/Y2015/Day2.md)
+  - [Day 3 - Mutually Recursive Functions](Years/Y2015/Day3.md)
+  - [Day 4 - Basic FFI](Years/Y2015/Day4.md)
+  - [Day 5 - Views and Dependent Pattern Matching](Years/Y2015/Day5.md)
+  - [Day 6 - Naive 2D Grid](Years/Y2015/Day6.md)
+  - [Day 7 - Dependent Maps and Indexed Type Familes](Years/Y2015/Day7.md)
+  - [Day 8 - Proper Effectful Parsers](Years/Y2015/Day8.md)
+  - [Day 9 - Naive Graph Traversal](Years/Y2015/Day9.md)
+  - [Day 10 - Digits View](Years/Y2015/Day10.md)
+  - [Day 11 - Refinement Types](Years/Y2015/Day11.md)
+  - [Day 12 - Custom Parser Effect and DLists](Years/Y2015/Day12.md)
+  - [Day 13 - Naive Ring Buffer and parameters blocks](Years/Y2015/Day13.md)

src/Util.md

@@ -9,15 +9,69 @@ module Util
 import Data.SortedSet
 import Data.String
 import Data.List.Lazy
+import Data.List1
+import Data.Vect
+import Data.Fin
 
 %default total
 ```
 
+## Foldable
+
+General utility functions for foldables
+
+```idris hide
+namespace Foldable
+```
+
+### minBy
+
+```idris
+  ||| Get the minimum element of a collection using the provided comparison
+  ||| function and seed value
+  export
+  minBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
+  minBy cmp acc x = 
+    foldl 
+      (\acc, e => 
+        case e `cmp` acc of
+          LT => e
+          _ => acc)
+      acc x
+```
+
+```idris
+  ||| Get the maximum element of a collection using the provided comparison
+  ||| function and seed value
+  export
+  maxBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a
+  maxBy cmp acc x = 
+    foldl 
+      (\acc, e => 
+        case e `cmp` acc of
+          GT => e
+          _ => acc)
+      acc x
+```
+
+## Functions
+
+### repeatN
+
+Recursively applies `f` to `seed` N times
+
+```idris
+export
+repeatN : (times : Nat) -> (f : a -> a) -> (seed : a) -> a
+repeatN 0 f seed = seed
+repeatN (S times') f seed = repeatN times' f (f seed)
+```
+
 ## Either
 
-<!-- idris
+```idris hide
 namespace Either
--->
+```
 
 ### mapLeft
 
@@ -31,18 +85,139 @@ Applies a function to the contents of a `Left` if the value of the given
   mapLeft f (Right x) = Right x
 ```
 
+## List
+
+```idris hide
+namespace List
+```
+
+### contains
+
+Returns `True` if the list contains the given value
+
+```idris
+  export
+  contains : Eq a => a -> List a -> Bool
+  contains x [] = False
+  contains x (y :: xs) = 
+    if x == y 
+      then True
+      else contains x xs
+```
+
+### rotations
+
+Provides all the 'rotations' of a list.
+
+Example:
+
+```
+rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]
+```
+
+```idris
+  export
+  rotations : List a -> List (List a) 
+  rotations xs = rotations' (length xs) xs []
+    where
+      rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
+      rotations' 0 xs acc = acc
+      rotations' (S k) [] acc = acc
+      rotations' (S k) (x :: xs) acc = 
+        let next = xs ++ [x]
+        in rotations' k next (next :: acc)
+```
+
+### permutations
+
+Lazily generate all of the permutations of a list
+
+```idris
+  export
+  permutations : List a -> LazyList (List a)
+  permutations [] = pure []
+  permutations xs = do
+    (head, tail) <- select xs
+    tail <- permutations (assert_smaller xs tail)
+    pure $ head :: tail
+    where 
+      consSnd : a -> (a, List a) -> (a, List a)
+      consSnd x (y, xs) = (y, x :: xs)
+      select : List a -> LazyList (a, List a)
+      select [] = []
+      select (x :: xs) = (x, xs) :: map (consSnd x) (select xs)
+```
+
+## Vect
+
+```idris hide
+namespace Vect
+```
+
+### permutations
+
+Lazily generate all the permutations of a Vect
+
+```idris
+  export
+  permutations : Vect n a -> LazyList (Vect n a)
+  permutations [] = []
+  permutations [x] = [[x]]
+  permutations (x :: xs) = do
+    (head, tail) <- select (x :: xs)
+    tail <- permutations tail
+    pure $ head :: tail
+    where
+      consSnd : a -> (a, Vect m a) -> (a, Vect (S m) a)
+      consSnd x (y, xs) = (y, x :: xs)
+      select : Vect (S m) a -> LazyList (a, Vect m a)
+      select [y] = [(y, [])]
+      select (y :: (z :: ys)) = 
+        (y, z :: ys) :: map (consSnd y) (select (z :: ys))
+```
+
+### minBy and maxBy
+
+```idris
+  ||| Get the minimum element of a non-empty vector by using the provided
+  ||| comparison function 
+  export
+  minBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
+  minBy f (x :: xs) = Foldable.minBy f x xs
+
+  ||| Get the maximum element of a non-empty vector by using the provided
+  ||| comparison function 
+  export
+  maxBy : (f : a -> a -> Ordering) -> Vect (S n) a -> a
+  maxBy f (x :: xs) = Foldable.maxBy f x xs
+```
+
+## Fin
+
+```idris hide
+namespace Fin
+```
+
+```idris
+  ||| Decriment a Fin, wrapping on overflow
+  export
+  unfinS : {n : _} -> Fin n -> Fin n
+  unfinS FZ = last
+  unfinS (FS x) = weaken x
+```
+
 ## Vectors
 
 Define some operations for pairs of numbers, treating them roughly like vectors
 
 ### Addition and Subtraction
 
-<!-- idris
+```idris hide
 export infixl 8 >+<
 export infixl 8 >-<
 
 namespace Pair
--->
+```
 
 ```idris
   public export
@@ -58,9 +233,9 @@ namespace Pair
 
 Extend `Data.SortedSet`
 
-<!-- idris
+```idris hide
 namespace Set
--->
+```
 
 ### length
 
@@ -76,9 +251,9 @@ Count the number of elements in a sorted set
 
 Extend `Data.String`
 
-<!-- idris
+```idris hide
 namespace String
--->
+```
 
 ### isSubstr
 
@@ -109,6 +284,10 @@ off of the string at a time, checking if the needle is a prefix at each step.
 
 ### Cartesian product
 
+```idris hide
+namespace LazyList
+```
+
 Lazily take the cartesian product of two foldables
 
 ```idris
@@ -124,3 +303,47 @@ cartProd x y =
       combine x [] rest = rest
       combine x (y :: ys) rest = (x, y) :: combine x ys rest
 ```
+
+### Concat
+
+Lazily concatenate a LazyList of LazyLists
+
+```idris
+  export
+  lazyConcat : LazyList (LazyList a) -> LazyList a
+  lazyConcat [] = []
+  lazyConcat (x :: xs) = x ++ lazyConcat xs
+```
+
+### Group
+
+Lazily group a LazyList
+
+```idris
+  export
+  lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
+  lazyGroup [] = []
+  lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
+    where
+      lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a)
+        -> LazyList (List1 a)
+      lazyGroup' [] current acc = [acc]
+      lazyGroup' (y :: ys) current acc@(head ::: tail) = 
+        if y == current
+          then lazyGroup' ys current (head ::: (y :: tail))
+          else acc :: lazyGroup (y :: ys)
+```
+
+### length
+
+Calculate the length of a LazyList
+
+```idris
+  export
+  length : LazyList a -> Nat
+  length = length' 0
+    where
+      length' : Nat -> LazyList a -> Nat
+      length' k [] = k
+      length' k (x :: xs) = length' (S k) xs
+```

src/Util/Digits.md

@@ -0,0 +1,192 @@
+# Viewing Integers as lists of digits
+
+```idris
+module Util.Digits
+
+import Data.Monoid.Exponentiation
+```
+
+```idris hide
+import System
+
+%default total
+```
+
+This module provides views and associated functionality for treating `Integers`
+as if they were lists of numbers.
+
+Since `Integer` is a primitive type, that Idris can't directly reason about the
+structure of, we need to use some `believe_me`s, a hideously unsafe operation
+that completely bypasses the type checker, somewhere along the line. For
+teaching purposes, we'll do it here, but please consider a library like
+[prim](https://github.com/stefan-hoeck/idris2-prim) if you find yourself needing
+to prove properties about primitive types.
+
+```idris hide
+-- This mutual block isn't strictly required, but is useful for literate purposes
+mutual
+```
+
+## Primitive functionality
+
+Take the integer log base 10 of an `Integer`
+
+```idris
+  log10 : Integer -> Nat
+  log10 i = assert_total $ log10' i 0
+    where
+      covering
+      log10' : Integer -> (acc : Nat) -> Nat
+      log10' i acc = 
+        if i > 0
+          then log10' (i `div` 10) (S acc)
+          else acc
+```
+
+## Ascending Order
+
+View an integer as a list of digits, ordered from least significant digit to
+most significant digit.
+
+For a clarifying example:
+
+```idris hide
+  -- @@test Ascending Digits Example
+  ascendingExample : IO Bool
+  ascendingExample = do
+    putStrLn "Expecting: \{show [5, 4, 3, 2, 1]}"
+    putStrLn "Got: \{show . ascList $ ascending 12345}"
+    pure $
+```
+
+```idris
+    ascList (ascending 12345) == [5, 4, 3, 2, 1]
+```
+
+The view itself, storing the current digit, and the rest of the number, both as
+a raw integer and by a recursive `Ascending`. Acts as a proof that the number
+can be reproduced by multiplying the rest by 10 and then adding the current
+digit.
+
+```idris
+  ||| A view of an integer as a list of digits in order of ascending signifigance
+  public export
+  data Ascending : Integer -> Type where
+    ||| Indicates that the number was negative
+    NegAsc : (rec : Lazy (Ascending (negate i))) -> Ascending i
+    ||| Indicates we have already seen all the digits of a number
+    End : Ascending 0
+    ||| A digit and all the preceeding ones
+    Next : (digit : Integer) 
+        -> (rest : Integer)
+        -> (rec : Lazy (Ascending rest))
+        -> Ascending (rest * 10 + digit)
+  %name Ascending as, bs, cs
+```
+
+Generate an `Ascending` from an integer.
+
+```idris
+  ||| Covering function for `Ascending`
+  export
+  ascending : (i : Integer) -> Ascending i
+  ascending i = 
+    if i < 0 then NegAsc (ascending (assert_smaller i $ negate i)) else
+    let digit = i `mod` 10
+        rest = i `div` 10
+    in if rest == 0 
+      then believe_me $ Next digit rest (believe_me End)
+      else believe_me $ Next digit rest (ascending (assert_smaller i rest))
+```
+
+Convert an `Ascending` to a list
+
+```idris
+  export
+  ascList : {i : Integer} -> Ascending i -> List Integer
+  ascList as = reverse $ ascList' i as []
+    where
+      ascList' : (j : Integer) -> Ascending j -> (acc : List Integer) 
+        -> List Integer
+      ascList' k (NegAsc rec) acc = ascList' (negate k) rec acc
+      ascList' 0 End acc = acc
+      ascList' ((rest * 10) + digit) (Next digit rest rec) acc = 
+        ascList' rest rec (digit :: acc)
+```
+
+## Descending Order
+
+View an integer as a list of digits, ordered from most significant digit to
+least significant digit.
+
+For a clarifying example:
+
+```idris hide
+  -- @@test Descending Digits Example
+  descendingExample : IO Bool
+  descendingExample = do
+    putStrLn "Expecting: \{show [1, 2, 3, 4, 5]}"
+    putStrLn "Got: \{show . decList $ descending 12345}"
+    pure $
+```
+
+```idris
+    decList (descending 12345) == [1, 2, 3, 4, 5]
+```
+
+The view itself, storing the current digit, and the rest of the number, both as
+a raw integer and by a recursive `Ascending`. Acts as a proof that the number
+can be reproduced by appending the current digit to the rest of the number.
+
+```idris
+  ||| A view of an integer as a list of digits in order of descending 
+  ||| signifigance
+  public export
+  data Descending : Integer -> Type where
+    ||| Indicates that the number was negative
+    NegDec : (rec : Lazy (Descending (negate i))) -> Descending i
+    ||| Indicates we have already seen all the digits of a number
+    Start : Descending 0
+    ||| A digit and all the preceeding ones
+    Prev : (magnitude : Nat)
+        -> (digit : Integer)
+        -> (rest : Integer)
+        -> (rec : Lazy (Descending rest))
+        -> Descending ((digit * 10 ^ magnitude) + rest)
+  %name Descending ds, es, fs
+```
+
+Generate a `Descending` from an `Integer`
+
+```idris
+  export
+  descending : (i : Integer) -> Descending i 
+  descending i = 
+    if i < 0 then NegDec (descending (assert_smaller i $ negate i)) else
+    let magnitude = log10 i
+    in if magnitude == 0
+      then believe_me $ Prev 0 0 0 Start
+      else descending' magnitude i
+    where
+      descending' : (magnitude : Nat) -> (j : Integer) -> Descending j 
+      descending' 0 j = believe_me Start
+      descending' magnitude@(S m) j = 
+        let digit = j `div` 10 ^ m
+            rest = j - digit * 10 ^ m 
+        in believe_me $ Prev m digit rest (descending' m rest) 
+```
+
+Convert a `Descending` to a list
+
+```idris
+  export
+  decList : {i : Integer} -> Descending i -> List Integer
+  decList ds = reverse $ decList' ds []
+    where
+     decList' : {i : Integer} -> Descending i -> (acc : List Integer) -> 
+       List Integer
+     decList' (NegDec rec) acc = decList' rec acc
+     decList' Start acc = acc
+     decList' (Prev magnitude digit rest rec) acc = 
+       decList' rec (digit :: acc)
+```

src/Util/Eff.md

@@ -6,6 +6,7 @@ Contains utility functions extending the functionality of the `eff` package.
 module Util.Eff
 
 import Control.Eff
+import Data.Subset
 import Text.ANSI
 
 import System
@@ -21,12 +22,21 @@ 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
+```idris hide
 export
 levelToNat : Level -> Nat
 levelToNat Err = 0
@@ -43,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
@@ -57,7 +67,7 @@ export infixl 8 >+
 export
 (>+) : Level -> Nat -> Level
 (>+) x k = natToLevel (k + levelToNat x)
--->
+```
 
 Convert a `Level` into a colorized tag
 
@@ -129,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
@@ -154,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
@@ -180,3 +192,66 @@ oneOfM : Has (Choose) fs => Foldable f =>
     f (Eff fs a) -> Eff fs a
 oneOfM x = foldl alt empty x
 ```
+
+## Subset
+
+Reorder the first two elements of the first argument of a subset
+
+```idris
+public export
+subsetReorderLeft : Subset (x :: g :: xs) ys -> Subset (g :: x :: xs) ys
+subsetReorderLeft (e :: (e' :: subset)) = e' :: e :: subset
+```
+
+Add the same element to both arguments of a subset
+
+```idris
+public export
+subsetConsBoth : {0 xs, ys : List a} -> {0 g : a} -> Subset xs ys 
+  -> Subset (g :: xs) (g :: ys)
+subsetConsBoth {xs = []} {ys = ys} [] = [Z]
+subsetConsBoth {xs = (x :: xs)} {ys} (e :: subset) = 
+  let rest = S e :: subsetConsBoth subset {g}
+  in subsetReorderLeft rest
+```
+
+A list is always a subset of itself
+
+```idris
+public export
+subsetReflexive : {xs : List a} -> Subset xs xs
+subsetReflexive {xs = []} = []
+subsetReflexive {xs = (x :: xs)} = 
+  let rest = subsetReflexive {xs} 
+  in subsetConsBoth rest
+```
+
+If `xs` is a subset of `ys`, then it is also a subset of `ys + g`
+
+```idris
+public export
+subsetConsRight : {0 g: _} -> {0 xs, ys: _} -> Subset xs ys -> Subset xs (g :: ys)
+subsetConsRight {xs = []} {ys = ys} [] = []
+subsetConsRight {xs = (x :: xs)} {ys} (e :: subset) = 
+  S e :: subsetConsRight subset {g}
+```
+
+`xs` is always a subset of `xs + g`
+
+```idris
+public export
+trivialSubset : {0 g : a} -> {xs : List a} -> Subset xs (g :: xs)
+trivialSubset = subsetConsRight subsetReflexive
+```
+
+`fs - f` is always a subset of `f`
+
+```idris
+public export
+minusLemma : {fs : List a} -> {0 x : a} -> {auto prf : Has x fs} 
+  -> Subset (fs - x) fs
+minusLemma {fs = (_ :: vs)} {prf = Z} = trivialSubset
+minusLemma {fs = (w :: vs)} {prf = (S y)} = 
+  let rest = minusLemma {fs = vs} {prf = y}
+  in subsetConsBoth rest
+```

src/Years/Y2015.md

@@ -6,7 +6,7 @@ import Structures.Dependent.FreshList
 import Runner
 ```
 
-<!-- idris
+```idris hide
 import Years.Y2015.Day1
 import Years.Y2015.Day2
 import Years.Y2015.Day3
@@ -14,7 +14,13 @@ import Years.Y2015.Day4
 import Years.Y2015.Day5
 import Years.Y2015.Day6
 import Years.Y2015.Day7
--->
+import Years.Y2015.Day8
+import Years.Y2015.Day9
+import Years.Y2015.Day10
+import Years.Y2015.Day11
+import Years.Y2015.Day12
+import Years.Y2015.Day13
+```
 
 # Days
 
@@ -66,6 +72,42 @@ y2015 = MkYear 2015 [
   , day7
 ```
 
+## [Day 8](Y2015/Day8.md)
+
+```idris
+  , day8
+```
+
+## [Day 9](Y2015/Day9.md)
+
+```idris
+  , day9
+```
+
+## [Day 10](Y2015/Day10.md)
+
+```idris
+  , day10
+```
+
+## [Day 11](Y2015/Day11.md)
+
+```idris
+  , day11
+```
+
+## [Day 12](Y2015/Day12.md)
+
+```idris
+  , day12
+```
+
+## [Day 13](Y2015/Day13.md)
+
+```idris
+  , day13
+```
+
 ```idris
   ]
 ```

src/Years/Y2015/Day1.md

@@ -1,9 +1,9 @@
-# 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.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day1
 
 import Control.Eff
@@ -11,7 +11,7 @@ import Control.Eff
 import Runner
 
 %default total
--->
+```
 
 ## Solver Functions
 
@@ -76,8 +76,8 @@ part2 x = do
   pure $ findBasement 1 0 input
 ```
 
-<!-- idris
+```idris hide
 public export
 day1 : Day
 day1 = Both 1 part1 part2
--->
+```

src/Years/Y2015/Day10.md

@@ -0,0 +1,125 @@
+# [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.
+
+```idris hide
+module Years.Y2015.Day10
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+import Data.String
+import Data.List1
+import Data.List.Lazy
+import Data.Monoid.Exponentiation
+import Data.Nat.Views
+
+import Util
+import Util.Digits
+```
+
+```idris hide
+%default total
+```
+
+# Solver Functions
+
+Produce a lazy lists of the digits of a number, in descending order of
+significance. This effectively translates our new
+[`Descending`](../../Util/Digits.md#descending-order) view to a `LazyList`.
+
+```idris
+lazyDigits : Integer -> LazyList Integer
+lazyDigits i with (descending i)
+  lazyDigits i | (NegDec rec) = lazyDigits _ | rec
+  lazyDigits 0 | Start = []
+  lazyDigits ((digit * (10 ^ magnitude)) + rest) | (Prev _ digit rest rec) = 
+    digit :: lazyDigits _ | rec
+```
+
+Apply the look-and-say rule to list of digits. We operate in the list-of-digits
+space for efficiency, this number will grow into the millions of digits, and
+Idris is currently lacking some needed primitive operations to perform this
+operation in `Integer` space reasonably efficiently. A `LazyList` is used here
+to avoid having to actually instantiate the entirety of these reasonably large
+lists.
+
+```idris
+lookAndSay : LazyList Integer -> LazyList Integer
+lookAndSay digits = 
+  -- Flatten the list once more
+  lazyConcat
+  -- Convert the produced numbers into lists of their digits
+  . map lazyDigits
+  -- re-flatten our list
+  . lazyConcat
+  -- Count the number of occurrences of each digit and emit [occurances, digit]
+  . map (\xs@(head ::: tail) => 
+          (the (LazyList _) [natToInteger $ length xs, head])) 
+  -- Group identical digits
+  . lazyGroup 
+  $ digits
+```
+
+Apply the look-and-say rule to an integer, for repl testing
+
+```idris
+lookAndSay' : Integer -> Integer
+lookAndSay' i = 
+  let digits = lazyDigits i
+      res = lookAndSay digits
+  in unDigits res 0
+  where
+    unDigits : LazyList Integer -> (acc : Integer) -> Integer
+    unDigits [] acc = acc
+    unDigits (x :: xs) acc = unDigits xs (acc * 10 + x)
+```
+
+Repeatedly apply `lookAndSay` to a seed value, with logging
+
+```idris
+repeatLogged : Has Logger fs => 
+  (count : Nat) -> (seed : LazyList Integer) -> Eff fs $ LazyList Integer
+repeatLogged 0 seed = pure seed
+repeatLogged (S k) seed = do
+  trace "Remaining iterations: \{show (S k)} digits: \{show . count (const True) $ seed}"
+  repeatLogged k (lookAndSay seed) 
+```
+
+# Part Functions
+
+## Part 1
+
+Parse our input, convert it into a list of digits, then run our `lookAndSay`
+function on it 40 times, and count the output digits.
+
+```idris
+part1 : Eff (PartEff String) (Nat, LazyList Integer)
+part1 = do
+  input <- askAt "input" >>= (note "Invalid input" . parsePositive)
+  let input = lazyDigits input
+  info "Input: \{show input}"
+  output <- repeatLogged 40 input
+  pure (count (const True) output, output)
+```
+
+## Part 2
+
+Same thing, but 10 more times
+
+```idris
+part2 : (digits : LazyList Integer) -> Eff (PartEff String) Nat
+part2 digits = do
+  output <- repeatLogged 10 digits
+  pure $ count (const True) output
+```
+
+```idris hide
+public export
+day10 : Day
+day10 = Both 10 part1 part2
+```

src/Years/Y2015/Day11.md

@@ -0,0 +1,238 @@
+# [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 hide
+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 hide
+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
+passwordCriteria : Vect n PasswordChar -> Bool
+passwordCriteria 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, Password)
+part1 = do
+  input <- map trim $ askAt "input"
+  password <- parsePassword input
+  info "Starting password: \{show password} -> \{passwordToString 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 hide
+public export
+day11 : Day
+day11 = Both 11 part1 part2
+```
+
+## References
+
+[^1]: <https://github.com/stefan-hoeck/idris2-refined/>

src/Years/Y2015/Day12.md

@@ -0,0 +1,132 @@
+# [Year 2015 Day 12](https://adventofcode.com/2015/day/12)
+
+This day provides an introduction to our new
+[`Parser.JSON`](../../Parser/JSON.md) module, as well as the use of `DList`s[^1]
+to collect values from an indexed type family into a single collection.
+
+```idris hide
+module Years.Y2015.Day12
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+import Structures.Dependent.DList
+
+import Parser
+import Parser.JSON
+```
+
+## Parsing
+
+Parse a list of JSON values into a `DList`.
+
+`JSONValue`'s type constructor has the signature `JSONType -> Type`, forming
+what is known as an "Indexed Type Family".
+
+Each type of JSON value has a separate type, e.g. a Bool has type
+`JSONValue TBool`, a String has type `JSONValue TString`, etc. While these are
+all separate types, they all share the `JSONValue` component of the type
+constructor, making them members of the same family.
+
+Despite being members of the same type family, they still have different types,
+so we can't just shove `JSONValue`s of different types into, say, a
+`List JSONValue`, we need a collection with some amount of heterogeneity. While
+a `List (type : JSONType ** JSONValue type)` would _work_, that introduces
+various ergonomic headaches, so instead we return a `DList`[^1], a `List` like
+data structure specifically designed for collecting values from an indexed typed
+family into a single collection.
+
+The parsing logic is otherwise quite simple, we use the `many` combinator to
+turn the `value` parser, which parses a single JSON value, into one that parses
+a list of JSON values, and then use `DList`'s `fromList` method to collect the
+results into a `DList`.
+
+```idris
+parseJsons : Has (Except String) fs => Has IO fs => (input : String)
+  -> Eff fs (types : List JSONType ** DList JSONType JSONValue types) 
+parseJsons input = do
+  result <- runFirstIO (many value) input
+  case result of
+    Left err => throw $ show err
+    Right result => pure $ fromList result
+```
+
+## Solving
+
+A reducer for `DList.dFoldL` that sums all the numbers within the contained JSON
+Value.
+
+The outer function is meant to be called on a top level object, using
+`DList.dFoldL` on a `DList` of `JSONValue`s, where as the inner function
+directly reduces a `JSONValue` using `JSON.dFoldL`.
+
+```idris
+sumNumbers : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+sumNumbers dbl type value = dFoldL sumNumbers' dbl value
+  where
+    sumNumbers' : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+    sumNumbers' dbl TNumber (VNumber d) = dbl + d
+    sumNumbers' dbl _ value = dbl
+```
+
+Filter out objects containing a "red" key
+
+```idris
+noRed  : (type : JSONType) -> (value : JSONValue type) -> Bool
+noRed TObject value = 
+  let (types ** vals) = getValues value
+  in case dFind (\t, v => 
+                  case t of
+                    TString => v == (VString "red")
+                    _ => False
+                ) vals of
+    Nothing => True
+    Just _ => False
+noRed _ value = True
+
+sumNumbersNoRed : 
+  Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+sumNumbersNoRed dbl type value = 
+  case dFilter noRed value of
+    Nothing => dbl
+    Just value => sumNumbers dbl type value
+```
+
+## Part Functions
+
+### Part 1
+
+Parse our JSONs, then fold our `sumNumbers` reducer over them.
+
+```idris
+part1 : Eff (PartEff String) 
+            (Double, (types : List JSONType ** DList JSONType JSONValue types))
+part1 = do
+  input <- askAt "input"
+  (types ** values) <- parseJsons input
+  let result = dFoldL sumNumbers 0.0 values
+  pure (result, (types ** values))
+```
+
+### Part 2
+
+```idris
+part2 : (types : List JSONType ** DList JSONType JSONValue types)
+  -> Eff (PartEff String) Double
+part2 (types ** values) = do
+  let result = dFoldL sumNumbersNoRed 0.0 values
+  pure result
+```
+
+```idris hide
+public export
+day12 : Day
+day12 = Both 12 part1 part2
+```
+
+## References
+
+[^1]: <https://git.sr.ht/~thatonelutenist/Structures/tree/trunk/item/src/Structures/Dependent/DList.md>

src/Years/Y2015/Day13.md

@@ -0,0 +1,263 @@
+# [Year 2015 Day 13](https://adventofcode.com/2015/day/13)
+
+This day exhibits a naive, `Vect` based implementation of a ring buffer, as well
+as our first introduction to `parameters` blocks.
+
+```idris hide
+module Years.Y2015.Day13
+
+import Data.Primitives.Interpolation
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+import Data.String
+import Data.List1
+import Data.List.Lazy
+import Data.Vect
+import Data.Maybe
+import Data.SortedMap.Dependent
+import Decidable.Equality
+
+import Util
+
+%default total
+```
+
+## Parsing and Data Structures
+
+```idris
+Name : Type
+Name = String
+
+Happiness : Type
+Happiness = Integer
+```
+
+Describe a change in happiness from a change in seating arrangement as data
+structure, indexed by the name of the individual whose happiness it describes,
+and provide some projections.
+
+```idris
+data Change : (changee : Name) -> Type where
+  NextTo : (changee : Name) -> (other : Name) -> (amount : Happiness)
+    -> Change (changee)
+
+(.changee) : Change changee -> Name
+(.changee) (NextTo changee _ _) = changee
+
+(.other) : Change changee -> Name
+(.other) (NextTo _ other _) = other
+
+(.amount) : Change changee -> Happiness
+(.amount) (NextTo _ _ amount) = amount
+```
+
+Collect the list of changes provided as input into a structure that encodes our
+assumptions at the type level.
+
+The changes are stored in a in a dependent map, with the name of the individual
+as the key, and lists of potential changes to their happiness as the values.
+
+This problem is a bit nicer to express in terms of a collection of known size,
+and we don't want to be constantly converting the keys list to a `Vect`, so we
+instead store it in `Changes` as a `Vect`. We don't want to accidentally store
+the wrong thing here, so we store an auto-implicit proof of equality,
+`keys_prf`, proving that the `names` list is exactly the list of keys in
+`change_map` converted to a Vect with `fromList`.
+
+It will also make things a bit nicer if we can assume that our `names` list is
+non-empty, after all it really doesn't make sense to talk about seating
+arrangements at a table with 0 people at it, so we store an auto-implict
+`nonempty` proof establishing that the length of `change_map`'s keys list, and
+thus `names`, is at least 1.
+
+```idris
+record Changes where
+  constructor MkChanges
+  change_map : SortedDMap Name (\n => List (Change n))
+  names : Vect (length (keys change_map)) Name
+  {auto keys_prf : names = fromList (keys change_map)}
+  {auto nonempty : IsSucc (length (keys change_map))}
+```
+
+Our usual pattern-matching based parsing of one element of the input, returning
+a dependent pair of the name of the individual this record describes, and the
+change described by that record.
+
+```idris
+parseChange : Has (Except String) fs => 
+  String -> Eff fs (name ** Change name)
+parseChange str = do
+  changee ::: [_, direction, amount, _, _, _, _, _, _, other] 
+    <- pure $ split (== ' ') str
+    | _ => throw "Invalid input string \{str}"
+  amount <- note "Invalid amount \{amount} in \{str}" $ parseInteger amount
+  amount : Happiness <-
+    case direction of
+      "gain" => pure amount
+      "lose" => pure $ negate amount
+      x      => throw "Invalid direction \{x} in \{str}" 
+  let other = pack . filter (/= '.') . unpack $ other
+  pure (_ ** (changee `NextTo` other) amount)
+```
+
+Parse the entire list of changes in the input, collecting them into a dependent
+map as we go along, and performing the checks needed for Idris to be satisfied
+that the conditions encoded by the auto-implict proofs in `Changes` are met.
+
+```idris
+parseChanges : Has (Except String) fs =>
+  List String -> (seed : SortedDMap Name (\n => List (Change n)))
+  -> Eff fs Changes
+parseChanges strs seed = do
+  changes <- traverse parseChange strs
+  let change_map = insertChanges changes seed
+  case isItSucc (length (keys change_map)) of
+    Yes prf => pure $ MkChanges change_map (fromList (keys change_map))
+    No contra => throw "Empty table, not very interesting"
+  where
+    insertChanges : List (name ** Change name) 
+      -> (acc : SortedDMap Name (\n => List (Change n)))
+      -> SortedDMap Name (\n => List (Change n))
+    insertChanges [] acc = acc
+    insertChanges ((name ** change) :: xs) acc = 
+      case lookupPrecise name acc of
+        Nothing => insertChanges xs (insert name [change] acc)
+        Just ys => insertChanges xs (insert name (change :: ys) acc)
+```
+
+## Solver functions
+
+All of these functions are about to take the same first argument,
+`(cs : Changes)`. This is a really common occurrence, especially when dealing
+with dependent proof types, so Idris has syntax sugar to avoid repeating your
+self in theses situations, `parameters` blocks[^1].
+
+A `parameters` block adds the provided arguments to the start of every top level
+signature contained within it, in this case, making the first argument of all of
+these functions have type `(cs : Changes)`. The arguments to the `parameters`
+blocks are also added to the front of the arguments list, using the names
+provided in the signature.
+
+`parameters` blocks also provide another fun bit of functionality that makes
+code within them more concise, within a `parameters` block, the parameters are
+implicitly passed as arguments to calls to functions in the same block.
+
+```idris
+parameters (cs : Changes)
+```
+
+Calculate the happiness change for a given person in a seating arrangement, use
+`finS` and `unfinS` to get the indexes of the parties seated to either side of
+us, and look them up in our map, adding the amount of change described by them
+together.
+
+Notice how `cs` appears neither in the arguments list, nor the type signature,
+yet we can still refer to it as if it was included at the start of both.
+
+```idris
+  happinessFor :
+    (arrangement : Vect (length (keys cs.change_map)) Name)
+    -> (idx : Fin (length (keys cs.change_map)))
+    -> Happiness
+  happinessFor arrangement idx = 
+    let name = idx `index` arrangement
+    in case name `lookupPrecise` cs.change_map of
+      Nothing => 0
+      Just changes => 
+        let name_right = (finS idx) `index` arrangement
+            change_right = 
+              fromMaybe 0 . map (.amount) . find ((== name_right) . (.other)) $ 
+                changes
+            name_left = (unfinS idx) `index` arrangement
+            change_left = 
+              fromMaybe 0 . map (.amount) . find ((== name_left) . (.other)) $ 
+                changes
+        in change_right + change_left
+```
+
+Calculate the overall happiness change for a given arrangement by mapping our
+`happinessFor` function over a list of all possible indexes to the `arrangement`
+vect, and summing the results.
+
+Notice how the `cs` parameter is implicitly passed to `happinessFor`, as we are
+inside the same `parameters` block as it.
+
+```idris
+  happinessChange :
+    (arrangement : Vect (length (keys cs.change_map)) Name)
+    -> Happiness
+  happinessChange arrangement = 
+    let idxes = List.allFins (length (keys cs.change_map))
+        changes = map (happinessFor arrangement) idxes
+    in sum changes
+```
+
+Find the arrangement with the maximum total change in happiness by mapping
+`happinessChange` over a list of all the possible permutations of our seed
+arrangement described by `names`, and using `maxBy` to identify the largest
+positive change in overall happiness.
+
+```idris
+  maxHappiness : Has (Except String) fs =>   
+    Eff fs (Happiness, Vect (length (keys cs.change_map)) Name)
+  maxHappiness =
+    let arrangements = permutations cs.names
+        changes = map happinessChange arrangements
+        pairs = zip changes arrangements
+    in case pairs of
+      [] => throw "No arrangements"
+      (x :: xs) => pure $ maxBy (compare `on` fst) x xs
+```
+
+## Part Functions
+
+### Part 1
+
+Parse our input and feed it into our `maxHappiness` function.
+
+Notice how, since we are outside the `parameters` block, we have to provide the
+`cs` argument to `maxHappiness` explicitly.
+
+```idris
+part1 : Eff (PartEff String) (Happiness, ())
+part1 = do
+  input <- map lines $ askAt "input"
+  changes <- parseChanges input empty
+  (max, arrangement) <- maxHappiness changes
+  pure (max, ())
+```
+
+### Part 2
+
+Our implementation already replaces missing relationships with 0, so we can
+cheese this by injecting ourself with an empty relationship list into the
+`change_map : SortedDMap Name (\n => (List n))`.
+
+The overall `Changes` data structure isn't easy to modify, and since our data
+set is quite small here, we'll just inject this into parsing and reparse our
+data.
+
+```idris
+part2 : () -> Eff (PartEff String) Happiness
+part2 x = do
+  input <- map lines $ askAt "input"
+  let seed = insert "ME!!!!" [] empty
+  changes <- parseChanges input seed
+  (max, arrangement) <- maxHappiness changes
+  pure max
+```
+
+```idris hide
+public export
+day13 : Day
+day13 = Both 13 part1 part2
+```
+
+## References
+
+[^1]: <https://idris2.readthedocs.io/en/latest/tutorial/modules.html#parameterised-blocks-parameters-blocks>

src/Years/Y2015/Day2.md

@@ -1,14 +1,14 @@
-# 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
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day2
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.List
@@ -16,9 +16,9 @@ import Data.List1
 import Data.String
 ```
 
-<!-- idris 
+```idris hide
 %default total
--->
+```
 
 ## Box structure
 
@@ -130,8 +130,8 @@ part2 : (boxes : List Box) -> Eff (PartEff String) Integer
 part2 boxes = pure . sum . map totalRibbon $ boxes
 ```
 
-<!-- idris
+```idris hide
 public export
 day2 : Day
 day2 = Both 2 part1 part2
--->
+```

src/Years/Y2015/Day3.md

@@ -1,15 +1,15 @@
-# 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.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day3
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.SortedSet
@@ -18,9 +18,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -152,8 +152,8 @@ part2 movements = do
   pure . length $ locations
 ```
 
-<!-- idris
+```idris hide
 public export
 day3 : Day
 day3 = Both 3 part1 part2
--->
+```

src/Years/Y2015/Day4.md

@@ -1,15 +1,15 @@
-# 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.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day4
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -196,8 +196,8 @@ part2 seed = do
   pure number
 ```
 
-<!-- idris
+```idris hide
 public export
 day4 : Day
 day4 = Both 4 part1 part2
--->
+```

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),
@@ -6,13 +6,13 @@ specifically `String`'s
 [`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList)
 view, which lets us treat `String`s as if they were lazy lists or iterators.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day5
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -20,9 +20,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Nice Strings
 
@@ -213,8 +213,8 @@ part2 _ = do
   pure x
 ```
 
-<!-- idris
+```idris hide
 public export
 day5 : Day
 day5 = Both 5 part1 part2
--->
+```

src/Years/Y2015/Day6.md

@@ -1,12 +1,14 @@
-# Year 2015 Day 6
+# [Year 2015 Day 6](https://adventofcode.com/2015/day/6)
 
-<!-- idris
+Introduction to the advent of code classic 2d grid problem.
+
+```idris hide
 module Years.Y2015.Day6
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Util
@@ -19,9 +21,9 @@ import Data.String
 import Data.IORef
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -73,12 +75,12 @@ The three types of action that can be performed on a light.
 data Action = On | Off | Toggle
 ```
 
-<!-- idris
+```idris hide
 Show Action where
   show On = "on"
   show Off = "off"
   show Toggle = "toggle"
--->
+```
 
 The range of coordinates that a command affects
 
@@ -88,11 +90,11 @@ record Range (rows, cols : Nat) where
   top_left, bottom_right : Coord rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Range rows cols) where
   show (MkRange top_left bottom_right) = 
     "\{show top_left} -> \{show bottom_right}"
--->
+```
 
 Helper function to extract a range of values from our Grid.
 
@@ -117,11 +119,11 @@ record Command (rows, cols : Nat) where
   range : Range rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Command rows cols) where
   show (MkCmd action range) = 
     "{\{show action}: \{show range}}"
--->
+```
 
 ### Parsing
 
@@ -332,8 +334,8 @@ part2 commands = do
   pure brightness
 ```
 
-<!-- idris
+```idris hide
 public export
 day6 : Day
 day6 = Both 6 part1 part2
--->
+```

src/Years/Y2015/Day7.md

@@ -1,4 +1,4 @@
-# Year 2015 Day 7
+# [Year 2015 Day 7](https://adventofcode.com/2015/day/7)
 
 This day provides us a gentle introduction to dependent maps.
 
@@ -13,13 +13,13 @@ Ensuring that the input contains only one gate outputting for each wire is done
 through throwing a runtime error in the parsing function if a second gate
 outputting to a given wire is found in the input.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day7
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.Bits
@@ -31,9 +31,9 @@ import Data.SortedMap.Dependent
 import Decidable.Equality
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -53,7 +53,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
@@ -249,8 +252,8 @@ part2 (circut, value) = do
   pure value
 ```
 
-<!-- idris
+```idris hide
 public export covering
 day7 : Day
 day7 = Both 7 part1 part2
--->
+```

src/Years/Y2015/Day8.md

@@ -0,0 +1,351 @@
+# [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.
+
+```idris hide
+module Years.Y2015.Day8
+
+import Control.Eff
+
+import Data.Primitives.Interpolation
+
+import Runner
+```
+
+```idris
+import Data.String
+import Data.Vect
+import Data.List.Lazy
+import Data.Either
+```
+
+## Parsing
+
+A "Parser" is an effectful computation that has access to a list of chars as
+state, can throw exceptions of type `String`, and has non-determinism through
+the `Choose` effect, which consumes some of the state to potentially return a
+value.
+
+### Basic operations
+
+Get the next character out of the parser state, updating the state to consume
+that character.
+
+```idris
+nextChar : Has (State (List Char)) fs => Has (Except String) fs => Eff fs Char
+nextChar = do
+  c :: rest <- get
+    | [] => throw "End of input"
+  put rest
+  pure c
+```
+
+Attempt to parse a single character based on the supplied predicate, consuming
+the character from the state and throwing the provided error if the predicate
+does not hold over the consumed character.
+
+```idris
+char : Has (State (List Char)) fs => Has (Except String) fs => 
+  (pred : Char -> Bool) -> (err : Char -> String) -> Eff fs Char
+char pred err = do
+  c <- nextChar
+  unless (pred c) (throw $ err c)
+  pure c
+```
+
+Type alias for a parser
+
+```idris
+Parser : (res : Type) -> Type
+Parser res = Eff [State (List Char), Except String, Choose, Logger] res
+```
+
+Parse 0+ of a thing, speculatively attempting to apply the given parser. In the
+event the supplied parser fails, catch the error, unwind changes to the state,
+and return an empty list, otherwise append the parsed element to the head of the
+returned list and recurse.
+
+The rewinding of the state on failure _could_ be handled implicitly by the
+effect stack if `Except` was structured a bit differently, but that's a topic
+for another day.
+
+```idris
+many : (f : Parser t) -> Parser (List t)
+many f = do
+  state <- get
+  Just x <- lift $ catch (\ _ => pure Nothing) (map Just f)
+    | Nothing => do
+      put state
+      pure []
+  map (x ::) $ many f
+```
+
+"Parse" the end of the input, returning a unit if we are at the end of input,
+throwing an error otherwise.
+
+```idris
+endOfInput : Parser ()
+endOfInput = do
+  [] <- get
+    | xs => throw "Expected end of input, state non empty: `\{pack xs}`"
+  pure ()
+```
+
+### Character Classes
+
+Parse a single `"`, throwing an error if the current character is anything else.
+Returns a unit since there is only one possible character this parses, and this
+avoids us having to discard the character later in our `string` parser.
+
+```idris
+quote : Parser ()
+quote = do
+  _ <- char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`")
+  pure ()
+```
+
+Parse any character except `\` or `"`
+
+```idris
+normal : Parser Char
+normal = 
+  char 
+    (\x => not $ any (== x) (the (List _) ['\\', '"'])) 
+    (\x => "Expected normal, got `\{String.singleton x}`")
+```
+
+#### Escaped Characters
+
+Parse the character sequence `\"`, returning just the `"`. Despite the fact that
+can only return one possible character, like `quote` above, we return the parsed
+character, as we intend to provide all the escaped character parsers to the
+`oneOfM` combinator later.
+
+```idris
+eQuote : Parser Char
+eQuote = do
+  _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`")
+  char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`")
+```
+
+Parse the character sequence `\\`, returning just the second `\`.
+
+```idris
+eSlash : Parser Char
+eSlash = do
+  _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`")
+  char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`")
+```
+
+Convert a lowercase hexadecimal digit to its numerical value.
+
+```idris
+fromHex : Char -> Int
+fromHex c = 
+  if ord c >= 97
+    then ord c - 87
+    else ord c - 48
+```
+
+Parse a character sequence `\xAB`, where `AB` are hexadecimal digits, and decode
+the numerical value of `AB`, as a hexadecimal number, into its corresponding
+character.
+
+```idris
+eHex : Parser Char
+eHex = do
+  _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`")
+  _ <- char (== 'x') (\x => "Expected `x`, got `\{String.singleton x}`")
+  [x, y] <- map (map $ fromHex . toLower) . 
+            sequence . 
+            Vect.replicate 2 $
+            (char 
+              isHexDigit 
+              (\x => "Expected hex digit, got `\{String.singleton x}`"))
+  pure . chr $ x * 0x10 + y
+```
+
+Use the `oneOfM` combinator to combine our escaped character parsers into a
+single character class. `oneOfM` uses the `Choice` effect to try all of the
+provided parsers, conceptually in parallel, returning all of the results.
+
+```idris
+escaped : Parser Char
+escaped = oneOfM $ the (List _) [eQuote, eSlash, eHex]
+```
+
+### Top Level Class
+
+Combine our `normal` and `escaped` parsers into a single parser for non-quote
+characters.
+
+```idris
+character : Parser Char
+character = oneOfM $ the (List _) [normal, escaped]
+```
+
+Parse a string literal by describing its layout as a quote (`"`), followed by
+any number of characters, then another quote, followed by the end of input.
+Return the characters between the outer quotes.
+
+```idris
+string : Parser (List Char)
+string = do
+  quote
+  xs <- many character
+  quote
+  endOfInput
+  pure xs
+```
+
+### Running a parser
+
+Run a parser, with some debug logging, by peeling the parsing effects of of the
+type. The order is important here, remember that function composition "runs"
+right to left.
+
+We peel the state off the type first, so that we can get implicit "rewinding" of
+the state inside of our combinators, like `oneOfM`.
+
+For a full understanding of what's going on here, we need to see how the type
+signature changes as we peel effects off the type, you can uncomment the
+commented lines, and comment out the rest of the function, modifying the
+`let output =` line to follow along yourself, though the types you get may look
+a little different due to idris evaluating type alaises like `Eff` for you, I am
+keeping them in aliased forms, and excluding `Logger`, which doesn't impact the
+semantic of parsing, to keep the examples concise:
+
+- `runstate (unpack str) $ x`
+
+  This produces a value with type
+  `Eff [Except String, Choose] (List Char, List Char)`. In this tuple of values,
+  the first element is the actual output of the parser, and the second element
+  is the state after the parser has run.
+
+- `runExcept . runState (unpack str) $ x`
+
+  This produces a value with type
+  `Eff [Choose] (Either String (List Char, List Char))`. This corresponds to a
+  computation that either returns our tuple of output and state from before, or
+  an error. Important to note here is that, in the error case, we only return a
+  `String` (our error type), our state is discarded.
+
+- `runChoose {f = LazyList} . runExcept . runState (unpack str) $ x`
+
+  The `Choose` effect, works with any type that implements the `Alternative`
+  interface, and the choice of type impacts the semantics. A full discussion of
+  this is beyond the scope for today, but we chose to "run" `Choose` with
+  `LazyList`, which effectively gives us an iterator over all the possible
+  parsings of our input text.
+
+  This produces a value with type
+  `Eff [] (LazyList (Either String (List Char, List Char)))`. When we hit an
+  application of `Choose`, like `oneOfM`, all possibilities will be tried and
+  each one will be added to our output `LazyList`. Because this is a `LazyList`,
+  and not a `List`, only values we actually inspect are generated, allowing
+  parsing to terminate after the first successful parse without having to
+  generate the rest of the list.
+
+  Note that we have an independent possible state value for each slot in the
+  list, this speaks to this effect stack, when run in this order, providing a
+  sort of branching behavior for states, allowing different branches in the
+  `Choose` effect to modify their state without impacting the state of other
+  branches.
+
+From there, we run our `lazyRights` helper function over the outputs `LazyList`
+to discard parsing paths that result in an error, extract the first element of
+each tuple, get the head of the list, if one still exists, and use `pack` to
+convert the contents of the resulting `Maybe (List Char)` to a string. Then a
+little bit of debug logging, and return the output.
+
+```idris
+runParser : Has Logger fs => Parser (List Char) -> String 
+  -> Eff fs $ Maybe String
+runParser x str = do
+  info "Parsing: \{str}"
+  -- let outputs = 
+  --   runChoose {f = LazyList} . runExcept . runState (unpack str) $ x
+  -- ?parser_types
+  outputs <- 
+    lift . runChoose {f = LazyList} . runExcept . runState (unpack str) $ x
+  let output = map pack . head' . map fst . lazyRights $ outputs
+  case output of
+    Nothing =>
+      debug "Failed: \{show outputs}"
+    Just y => do
+      debug "Got: \{y}"
+      trace "\{show outputs}"
+  pure output
+  where
+    lazyRights : LazyList (Either a b) -> LazyList b
+    lazyRights [] = []
+    lazyRights (Left _ :: xs) = lazyRights xs
+    lazyRights (Right x :: xs) = x :: lazyRights xs
+```
+
+## Escaping characters
+
+This is much more boring the the parsing, we just do simple recursive pattern
+matching on the characters of the provided string, escaping `"` and `\`, and
+surround the resulting string with quotes.
+
+```idris
+escape : String -> String
+escape str = "\"\{pack . escape' . unpack $ str}\""
+  where
+  escape' : List Char -> List Char
+  escape' [] = []
+  escape' ('"' :: xs) = '\\' :: '"' :: escape' xs
+  escape' ('\\' :: xs) = '\\' :: '\\' :: escape' xs
+  escape' (x :: xs) = x :: escape' xs
+```
+
+## Part Functions
+
+### Part 1
+
+Convert the inputs into a list of lines, traverse our parser over it, deal with
+possible failures by sequencing the `List (Maybe String)` into a
+`Maybe (List String)`, and the compute the difference in character counts.
+
+```idris
+part1 : Eff (PartEff String) (Int, List String)
+part1 = do
+  inputs <- map lines $ askAt "input"
+  outputs <- traverse (runParser string) inputs
+  Just outputs <- pure $ sequence outputs
+    | _ => throw "Some strings failed to parse"
+  let difference = 
+    sum $ zipWith (\x, y => strLength x - strLength y) inputs outputs
+  pure (difference, inputs)
+```
+
+### Part 2
+
+Map our character escaping function over our input string and compute the
+difference in character counts.
+
+Make a little stop along the way to ensure that escape -> parse round trips
+without changing the content of the string.
+
+```idris
+part2 : List String -> Eff (PartEff String) Int
+part2 inputs = do
+  let outputs = map escape inputs
+  Just reversed_outputs <- map sequence . traverse (runParser string) $ outputs
+    | _ => throw "Reversing escaping of the inputs failed"
+  unless (all id $ zipWith (==) inputs reversed_outputs) $ do
+    debug . delay . joinBy "\n" . map show . filter (\(x, y, z) => x /= z) $ 
+      zip3 inputs outputs reversed_outputs
+    throw "Parsed outputs were not identical to inputs"
+  let difference = 
+    sum $ zipWith (\x, y => strLength y - strLength x) inputs outputs
+  pure difference
+```
+
+```idris hide
+public export
+day8 : Day
+day8 = Both 8 part1 part2
+```

src/Years/Y2015/Day9.md

@@ -0,0 +1,294 @@
+# [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
+meeting the problem criteria, and then figure out the length in a separate step.
+This isn't a particularly efficient solution, but its good enough for this small
+problem size.
+
+```idris hide
+module Years.Y2015.Day9
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+import Data.String
+import Data.List1
+import Data.Vect
+import Data.List.Lazy
+import Data.SortedMap
+import Data.SortedSet
+
+import Util
+```
+
+## Parsing and data structures
+
+### Parsing
+
+Define a location pair as a collection of two locations and a distance between
+them (as this graph is undirected), as well as some type aliases, a `contains`
+method to test if a pair covers a given location, and implement `Foldable` for
+the type to get access to the standard library utility methods.
+
+`DistanceMap` serves as a slightly fancy adjacency list for our graph
+representation. We'll load this into a `Reader` effect to avoid having to pass
+it around as an explicit argument to every function later on once it's been
+computed.
+
+```idris
+Location : Type
+Location = String
+
+Distance : Type
+Distance = Integer
+
+record LocationPair (l : Type) where
+  constructor MkLP
+  locations : Vect 2 l
+  distance : Integer
+%name LocationPair lp, mp, np, op
+
+contains : Eq l => l -> LocationPair l -> Bool
+contains x lp = 
+  case find (== x) lp.locations of
+    Nothing => False
+    Just _ => True
+
+Foldable LocationPair where
+  foldl f acc lp = foldl f acc lp.locations
+  foldr f acc lp = foldr f acc lp.locations
+  toList lp = toList lp.locations
+
+LP : Type
+LP = LocationPair Location
+
+DistanceMap : Type
+DistanceMap = SortedMap Location (List LP)
+```
+
+```idris hide
+Show l => Show (LocationPair l) where
+  show (MkLP [x, y] distance) = "\{show x} <-> \{show y}: \{show distance}"
+```
+
+Perform simple, pattern matching based parsing of a location pair.
+
+```idris
+parseLocationPair : Has (Except String) fs =>
+  String -> Eff fs LP
+parseLocationPair str = do
+  from ::: ["to", to, "=", dist] <- pure $ split (== ' ') str
+    | _ => throw "Badly formatted input string: \{str}"
+  dist <- note "Bad distance: \{dist}" $ parsePositive dist
+  pure $ MkLP [from, to] dist
+```
+
+Convert a list of pairs to a `DistanceMap`, a mapping from a location to all the
+location pairs that cover it. To keep this function readable, we do this inside
+an inner function with the `State DistanceMap` effect.
+
+Since the inner function is recursive, instead of extracting the result after
+running the state effect, we lift it into an unconstrained `fs` so we can borrow
+the stack-saftey from our runner's top level `runEff`.
+
+```idris
+pairsToMap : List LP -> Eff fs DistanceMap
+pairsToMap lps = do
+  (_, out) <- lift . runState empty $ insertPairs lps
+  pure out
+  where
+    insertLoc : LP -> (loc : Fin 2) -> Eff [State DistanceMap] ()
+    insertLoc lp loc = do
+      let loc = (index loc lp.locations)
+      list <- map (lookup loc) get
+      case list of
+        Nothing => modify $ insert loc [lp]
+        Just xs => modify $ insert loc (lp :: xs)
+    insertPair : LP -> Eff [State DistanceMap] ()
+    insertPair lp = traverse_ (insertLoc lp) (the (List _) [0, 1])
+    insertPairs : List LP -> Eff [State DistanceMap] ()
+    insertPairs lps = traverse_ insertPair lps
+```
+
+## Solver functions
+
+Generate all the possible paths originating from `current` with length `depth`,
+which is set to the number of locations in the calling function to provide the
+"visits each node once" property.
+
+The `path` argument accumulates the path taken by this particular branch of the
+breadth first search. It is accumulated in reverse order, but this doesn't
+really matter as this graph is undirected.
+
+We use the `Choose` effect to explore every possible link connecting to the
+current node, after filtering the possible links for ones that satisfy the
+problem constraints.
+
+```idris
+paths : Has (Reader DistanceMap) fs => Has Choose fs => Has Logger fs =>
+  (path : List Location) 
+  -> (depth : Nat)
+  -> (current : Location)
+  -> Eff fs (List Location)
+paths path 0 current = empty
+paths path 1 current = 
+  if contains current path
+    then empty
+    else pure $ current :: path
+paths path (S depth') current = do
+  debug "Paths from \{current} at \{show (S depth')} having visited \{show path}"
+  -- If we are in the path list, we have revisited this node, bail
+  False <- pure $ contains current path
+    | _ => empty
+  -- Update our path list to contain ourself
+  let path = current :: path
+  -- Find our next possible steps, bailing out if there are none
+  Just nexts <- map (lookup current) ask
+    | _ => do empty
+  -- Convert it to a list of locations
+  let nexts = concat . map toList $ nexts
+  -- Filter out any that are already in the path, this would be covered by the
+  -- check at the start of this function, but this cleans up the logs
+  let nexts = filter (not . (flip contains) path) nexts
+  -- Select our next node
+  next <- oneOf nexts
+  paths path depth' next
+```
+
+Calculate all the possible paths that satisfy the problem constraints.
+
+As a minor optimization, we only explore the paths leading out of a single
+arbitrary location to start with, and then take advantage of a symmetry of the
+problem, collecting all the "rotations" of each output path to cheaply calculate
+all the paths that take all the same steps as our "seed" path, but have
+different starting and ending locations.
+
+```idris
+allPaths : 
+  Has (Reader DistanceMap) fs => Has Logger fs => Has (Except String) fs =>
+  Eff fs $ SortedSet (List Location)
+allPaths = do
+  locs <- map keys ask
+  first <- note "No locations" $ head' locs
+  paths <- lift . runChoose {f = LazyList} $ 
+    paths [] (length locs) first {fs = [Choose, Reader _, Logger]}
+  pure $ buildSet paths empty
+  where
+    insertPaths : List (List Location) -> (acc : SortedSet (List Location)) 
+      -> SortedSet (List Location)
+    insertPaths [] acc = acc
+    insertPaths (x :: xs) acc = insertPaths xs (insert x acc)
+    buildSet : LazyList (List Location) -> (acc : SortedSet (List Location))
+      -> SortedSet (List Location)
+    buildSet [] acc = acc
+    buildSet (x :: xs) acc = 
+      let rots = rotations x
+      in buildSet xs (insertPaths rots acc) 
+```
+
+Calculate the length of a path by recursively destructuring the list and looking
+up each pair of locations in our `DistanceMap`.
+
+```idris
+pathLen : Has (Reader DistanceMap) fs => Has (Except String) fs =>
+  (path : List Location) -> Eff fs Integer
+pathLen [] = pure 0
+pathLen (x :: []) = pure 0
+pathLen (x :: (y :: xs)) = do
+  lps <- map (lookup x) ask >>= note "Not found in distance map: \{x}"
+  lp <- note "Pair not found \{x} \{y}" $ 
+    find (\l => contains x l && contains y l) lps
+  map (lp.distance +) $ pathLen (y :: xs)
+```
+
+Calculate the shortest path from a list of paths by recursively comparing
+lengths.
+
+```idris
+shortestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
+  (paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
+shortestPath paths = do
+  shortest paths Nothing
+  where
+    shortest : List (a, Integer) -> (acc : Maybe (a, Integer)) 
+      -> Eff fs (a, Integer)
+    shortest [] acc = note "No paths" acc
+    shortest (x :: xs) acc = 
+      case acc of
+        Nothing => shortest xs (Just x)
+        Just y => 
+          if (snd x) < (snd y)
+            then shortest xs (Just x)
+            else shortest xs (Just y)
+```
+
+Calculate the longest path from a list of paths by recursively comparing
+lengths.
+
+```idris
+longestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
+  (paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
+longestPath paths = do
+  longest paths Nothing
+  where
+    longest : List (a, Integer) -> (acc : Maybe (a, Integer)) 
+      -> Eff fs (a, Integer)
+    longest [] acc = note "No paths" acc
+    longest (x :: xs) acc = 
+      case acc of
+        Nothing => longest xs (Just x)
+        Just y => 
+          if (snd x) > (snd y)
+            then longest xs (Just x)
+            else longest xs (Just y)
+```
+
+## Part Functions
+
+### Part 1
+
+Parse our locations, turn them into a `DistanceMap`, load that into our reader,
+generate our paths, then find the one with the shortest length.
+
+```idris
+part1 : 
+  Eff (PartEff String) (Integer, (DistanceMap, List (List Location, Integer)))
+part1 = do
+  locations <- map lines (askAt "input") >>= traverse parseLocationPair
+  info "Locations: \{show locations}"
+  distance_map <- pairsToMap locations
+  info "Distance map: \{show distance_map}"
+  runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do
+  paths <- map Prelude.toList allPaths
+  trace "Paths: \{show paths}"
+  info "Found \{show $ length paths} paths"
+  distances <- traverse pathLen paths
+  let pairs = zip paths distances
+  (path, len) <- shortestPath pairs
+  info "Shortest Path: \{show path} \{show len}"
+  pure (len, (distance_map, pairs))
+```
+
+### Part 2
+
+Feed the locations back into a longest path function
+
+```idris
+part2 : (DistanceMap, List (List Location, Integer))
+  -> Eff (PartEff String) Integer
+part2 (distance_map, pairs) = do
+  runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do
+  (path, len) <- longestPath pairs
+  info "Longest Path: \{show path} \{show len}"
+  pure len
+```
+
+```idris hide
+public export
+day9 : Day
+day9 = Both 9 part1 part2
+```