From aa33fe6004ad6d9ca18f4c37e11a3ee20c39d86a Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 17:06:08 -0500
Subject: [PATCH 01/19] Some notes

---
 book.toml          | 2 +-
 scripts/build-book | 2 ++
 src/Parser/JSON.md | 1 +
 3 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/book.toml b/book.toml
index 4ad1625..a4387d0 100644
--- a/book.toml
+++ b/book.toml
@@ -7,7 +7,7 @@ title = "Idris 2 by Highly Contrived Example"
 
 [build]
 create-missing = false
-use-default-preprocessors = false
+# use-default-preprocessors = false
 
 [output.html]
 preferred-dark-theme = "ayu"
diff --git a/scripts/build-book b/scripts/build-book
index 8513e4d..f1d8b7b 100755
--- a/scripts/build-book
+++ b/scripts/build-book
@@ -77,6 +77,8 @@ sub katla($src, $ttc-src) {
 
 # Copy our metadata files
 cp-temp "book.toml";
+# TODO: Special Handling for the README so we don't need the symlink and the
+# links work
 cp-temp "src/README.md";
 cp-temp "src/SUMMARY.md";
 
diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 6602210..7699d29 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -168,6 +168,7 @@ object = do
     pairs = do
       first <- keyValue
       rest <- many restKeyValue
+      -- TODO: headTail combinator for this
       pure $ first ::: rest
     occupiedObject : Parser (JSONValue TObject)
     occupiedObject = do

From 83afb8a7c41fcebe899d41aa2c1594caa1946839 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 18:30:30 -0500
Subject: [PATCH 02/19] Add JSON dFoldL

---
 src/Parser/JSON.md | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 7699d29..b69db49 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -82,6 +82,30 @@ Eq (JSONValue t) where
 %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
+```
+
 ## Parsers
 
 We are going to get mutually recursive here. Instead of using a `mutual` block,

From 6afe8c2a4e3ee28ebd923059d55dffafa7bbcc90 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 19:55:35 -0500
Subject: [PATCH 03/19] Make runFirstIO more generic

---
 src/Parser/Interface.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md
index 79583cf..53be055 100644
--- a/src/Parser/Interface.md
+++ b/src/Parser/Interface.md
@@ -110,7 +110,8 @@ Provide wrappers for `rundownFirst` for evaluating it in various contexts.
 
 ```idris
 export
-runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a)
+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"

From cd4949b2f8cefcfed4eee0579b357bb5bbeae93f Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 20:15:04 -0500
Subject: [PATCH 04/19] Export JSON show and Eq

---
 src/Parser/JSON.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index b69db49..60386ef 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -55,6 +55,7 @@ data JSONValue : JSONType -> Type where
 ```
 
 ```idris hide
+export
 Show (JSONValue t) where
   show (VObject xs) = 
     let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
@@ -69,6 +70,7 @@ Show (JSONValue t) where
   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

From e00ec274ca2a8c0cbcafebae421aaf41e086641d Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 19:47:47 -0500
Subject: [PATCH 05/19] Year 2015 Day 12 Part 1

---
 README.md                |  4 ++
 src/SUMMARY.md           |  1 +
 src/Years/Y2015.md       |  7 +++
 src/Years/Y2015/Day12.md | 99 ++++++++++++++++++++++++++++++++++++++++
 4 files changed, 111 insertions(+)
 create mode 100644 src/Years/Y2015/Day12.md

diff --git a/README.md b/README.md
index 1598931..731d675 100644
--- a/README.md
+++ b/README.md
@@ -128,6 +128,10 @@ solution.
 
     Introduces refinement types
 
+  - [Day 12](src/Years/Y2015/Day12.md)
+
+    New Parser Effect stack and DLists
+
 ## References
 
 [^1]: Idris 2 Manual:
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 2cf1e0b..f0b09eb 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -33,3 +33,4 @@
   - [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)
diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md
index c2a0326..8f94f4f 100644
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@@ -18,6 +18,7 @@ import Years.Y2015.Day8
 import Years.Y2015.Day9
 import Years.Y2015.Day10
 import Years.Y2015.Day11
+import Years.Y2015.Day12
 ```
 
 # Days
@@ -94,6 +95,12 @@ y2015 = MkYear 2015 [
   , day11
 ```
 
+## [Day 12](Y2015/Day12.md)
+
+```idris
+  , day12
+```
+
 ```idris
   ]
 ```
diff --git a/src/Years/Y2015/Day12.md b/src/Years/Y2015/Day12.md
new file mode 100644
index 0000000..92ce6dc
--- /dev/null
+++ b/src/Years/Y2015/Day12.md
@@ -0,0 +1,99 @@
+# [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
+```
+
+## Part Functions
+
+### Day 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))
+```
+
+```idris hide
+public export
+day12 : Day
+day12 = First 12 part1
+```
+
+## References
+
+[^1]: <https://git.sr.ht/~thatonelutenist/Structures/tree/trunk/item/src/Structures/Dependent/DList.md>

From e91db14c115b21a31ba0a26a53ff372793036cbb Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 21:02:07 -0500
Subject: [PATCH 06/19] Improve build-book script

---
 scripts/build-book | 79 ++++++++++++++++++++++++++--------------------
 1 file changed, 44 insertions(+), 35 deletions(-)

diff --git a/scripts/build-book b/scripts/build-book
index f1d8b7b..62af9b9 100755
--- a/scripts/build-book
+++ b/scripts/build-book
@@ -23,7 +23,7 @@ sub not-ignored($path) {
 # 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 cp-temp($src) {
+sub copy-to-dest($src) {
    my $src-path = do given $src {
        when Str {
            $src.IO
@@ -45,42 +45,16 @@ sub cp-temp($src) {
    $src-path.resolve.copy: $output-path;
 }
 
-# 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);
-    # TODO: Post process them to set themeing correctly
-    $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/'class="IdrisKeyword"'/class="hljs-keyword"/;
-    $output ~~ s:g/'class="IdrisModule"'/class="hljs-symbol hljs-emphasis"/;
-    $output ~~ s:g/'class="IdrisComment"'/class="hljs-comment"/;
-    $output ~~ s:g/'class="IdrisFunction"'/class="hljs-symbol"/;
-    $output ~~ s:g/'class="IdrisBound"'/class="hljs-name"/;
-    $output ~~ s:g/'class="IdrisData"'/class="hljs-title"/;
-    $output ~~ s:g/'class="IdrisType"'/class="hljs-type"/;
-    $output ~~ s:g/'class="IdrisNamespace"'/class="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);
-}
+# 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
-cp-temp "book.toml";
-# TODO: Special Handling for the README so we don't need the symlink and the
-# links work
-cp-temp "src/README.md";
-cp-temp "src/SUMMARY.md";
+copy-to-dest "book.toml";
+copy-to-dest "src/SUMMARY.md";
 
 # Katla over the source files
 for paths("src", :file(*.&not-ignored)) -> $path {
@@ -104,3 +78,38 @@ if $upload {
        '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);
+}

From b5547ccb58307f820f456024b737ee7a1bc3e236 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 21:26:47 -0500
Subject: [PATCH 07/19] Add getProperty method to JSON

---
 src/Parser/JSON.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 60386ef..35f6312 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -108,6 +108,18 @@ 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)
+```
+
 ## Parsers
 
 We are going to get mutually recursive here. Instead of using a `mutual` block,

From 5760da96eb71876ef1dc4a416fd1a22f67badb6f Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 22:25:12 -0500
Subject: [PATCH 08/19] Add dFilter to json

---
 src/Parser/JSON.md | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 35f6312..c71d95c 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -6,6 +6,8 @@ module Parser.JSON
 import public Parser
 import public Parser.Numbers
 
+import Control.Monad.Eval
+
 import Structures.Dependent.DList
 ```
 
@@ -120,6 +122,50 @@ getProperty prop (VObject xs) =
     Just (type ** (_, val)) => Just (type ** val)
 ```
 
+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,

From b2704dcbcc3a303e3224b7fffc242c1d595825d5 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 22:45:18 -0500
Subject: [PATCH 09/19] Add getValues to JSON

---
 src/Parser/JSON.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index c71d95c..7baf9fa 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -122,6 +122,16 @@ getProperty prop (VObject xs) =
     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

From c632ab023dec68d9206f8a7dd1e18b73ef99b315 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 27 Jan 2025 23:00:02 -0500
Subject: [PATCH 10/19] Year 2015 Day 12 Part 2

---
 src/Years/Y2015/Day12.md | 37 +++++++++++++++++++++++++++++++++++--
 1 file changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/Years/Y2015/Day12.md b/src/Years/Y2015/Day12.md
index 92ce6dc..2829698 100644
--- a/src/Years/Y2015/Day12.md
+++ b/src/Years/Y2015/Day12.md
@@ -72,9 +72,32 @@ sumNumbers dbl type value = dFoldL sumNumbers' dbl value
     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
 
-### Day 1
+### Part 1
 
 Parse our JSONs, then fold our `sumNumbers` reducer over them.
 
@@ -88,10 +111,20 @@ part1 = do
   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 = First 12 part1
+day12 = Both 12 part1 part2
 ```
 
 ## References

From ac93582e969ed92415f8d3a002e6f73161667185 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 28 Jan 2025 09:48:11 -0500
Subject: [PATCH 11/19] Add permutations and LazyList.length to Util

---
 src/Util.md | 154 +++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 111 insertions(+), 43 deletions(-)

diff --git a/src/Util.md b/src/Util.md
index 4e8de44..c2979cb 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -10,6 +10,7 @@ import Data.SortedSet
 import Data.String
 import Data.List.Lazy
 import Data.List1
+import Data.Vect
 
 %default total
 ```
@@ -56,13 +57,13 @@ namespace List
 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
+  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
@@ -76,16 +77,64 @@ 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)
+  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))
 ```
 
 ## Vectors
@@ -166,20 +215,24 @@ 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
-export
-cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
-cartProd x y = 
-  let y = foldToLazy y
-  in foldr (\e, acc => combine e y acc) [] x
-  where
-    foldToLazy : Foldable a' => a' e' -> LazyList e'
-    foldToLazy x = foldr (\e, acc => e :: acc) [] x
-    combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
-    combine x [] rest = rest
-    combine x (y :: ys) rest = (x, y) :: combine x ys rest
+  export
+  cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
+  cartProd x y = 
+    let y = foldToLazy y
+    in foldr (\e, acc => combine e y acc) [] x
+    where
+      foldToLazy : Foldable a' => a' e' -> LazyList e'
+      foldToLazy x = foldr (\e, acc => e :: acc) [] x
+      combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f)
+      combine x [] rest = rest
+      combine x (y :: ys) rest = (x, y) :: combine x ys rest
 ```
 
 ### Concat
@@ -187,10 +240,10 @@ cartProd x y =
 Lazily concatenate a LazyList of LazyLists
 
 ```idris
-export
-lazyConcat : LazyList (LazyList a) -> LazyList a
-lazyConcat [] = []
-lazyConcat (x :: xs) = x ++ lazyConcat xs
+  export
+  lazyConcat : LazyList (LazyList a) -> LazyList a
+  lazyConcat [] = []
+  lazyConcat (x :: xs) = x ++ lazyConcat xs
 ```
 
 ### Group
@@ -198,15 +251,30 @@ lazyConcat (x :: xs) = x ++ lazyConcat xs
 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)
+  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
 ```

From 5ad68cdb44291318a6bed529fcd1771116d9ca08 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Wed, 29 Jan 2025 01:13:43 -0500
Subject: [PATCH 12/19] Add unfinS to util

---
 src/Util.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/Util.md b/src/Util.md
index c2979cb..5a998c4 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -11,6 +11,7 @@ import Data.String
 import Data.List.Lazy
 import Data.List1
 import Data.Vect
+import Data.Fin
 
 %default total
 ```
@@ -137,6 +138,21 @@ Lazily generate all the permutations of a Vect
         (y, z :: ys) :: map (consSnd y) (select (z :: ys))
 ```
 
+## 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

From 3addc0aeaf403228b717abedaee094a382404f0a Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Wed, 29 Jan 2025 01:31:20 -0500
Subject: [PATCH 13/19] Add minBy and maxBy to Util

---
 src/Util.md | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 54 insertions(+), 1 deletion(-)

diff --git a/src/Util.md b/src/Util.md
index 5a998c4..9264794 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -16,6 +16,44 @@ 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
@@ -138,13 +176,28 @@ Lazily generate all the permutations of a Vect
         (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

From 22eccd177cf430827652d6e98b77851d4147efd1 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 28 Jan 2025 11:38:11 -0500
Subject: [PATCH 14/19] Year 2015 Day 13 Part 1

---
 README.md                |   6 +
 src/SUMMARY.md           |   1 +
 src/Years/Y2015.md       |   7 ++
 src/Years/Y2015/Day13.md | 241 +++++++++++++++++++++++++++++++++++++++
 4 files changed, 255 insertions(+)
 create mode 100644 src/Years/Y2015/Day13.md

diff --git a/README.md b/README.md
index 731d675..763edcc 100644
--- a/README.md
+++ b/README.md
@@ -132,7 +132,13 @@ solution.
 
     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>
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index f0b09eb..9447a3a 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -34,3 +34,4 @@
   - [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)
diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md
index 8f94f4f..79ae4e8 100644
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@@ -19,6 +19,7 @@ import Years.Y2015.Day9
 import Years.Y2015.Day10
 import Years.Y2015.Day11
 import Years.Y2015.Day12
+import Years.Y2015.Day13
 ```
 
 # Days
@@ -101,6 +102,12 @@ y2015 = MkYear 2015 [
   , day12
 ```
 
+## [Day 13](Y2015/Day13.md)
+
+```idris
+  , day13
+```
+
 ```idris
   ]
 ```
diff --git a/src/Years/Y2015/Day13.md b/src/Years/Y2015/Day13.md
new file mode 100644
index 0000000..a344473
--- /dev/null
+++ b/src/Years/Y2015/Day13.md
@@ -0,0 +1,241 @@
+# [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 -> Eff fs Changes
+parseChanges strs = do
+  changes <- traverse parseChange strs
+  let change_map = insertChanges changes empty
+  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
+  (max, arrangement) <- maxHappiness changes
+  pure (max, ())
+```
+
+```idris hide
+public export
+day13 : Day
+day13 = First 13 part1
+```
+
+## References
+
+[^1]: <https://idris2.readthedocs.io/en/latest/tutorial/modules.html#parameterised-blocks-parameters-blocks>

From f8d6e3cfcbe6904496ff1034d63efab3accd9317 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Wed, 29 Jan 2025 03:32:22 -0500
Subject: [PATCH 15/19] Year 2015 Day 13 Part 2

---
 src/Years/Y2015/Day13.md | 34 ++++++++++++++++++++++++++++------
 1 file changed, 28 insertions(+), 6 deletions(-)

diff --git a/src/Years/Y2015/Day13.md b/src/Years/Y2015/Day13.md
index a344473..e0f7f89 100644
--- a/src/Years/Y2015/Day13.md
+++ b/src/Years/Y2015/Day13.md
@@ -89,7 +89,8 @@ 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 : Has (Except String) fs => 
+  String -> Eff fs (name ** Change name)
 parseChange str = do
   changee ::: [_, direction, amount, _, _, _, _, _, _, other] 
     <- pure $ split (== ' ') str
@@ -110,10 +111,11 @@ that the conditions encoded by the auto-implict proofs in `Changes` are met.
 
 ```idris
 parseChanges : Has (Except String) fs =>
-  List String -> Eff fs Changes
-parseChanges strs = do
+  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 empty
+  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"
@@ -225,15 +227,35 @@ Notice how, since we are outside the `parameters` block, we have to provide the
 part1 : Eff (PartEff String) (Happiness, ())
 part1 = do
   input <- map lines $ askAt "input"
-  changes <- parseChanges 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 = First 13 part1
+day13 = Both 13 part1 part2
 ```
 
 ## References

From f675677a7647859c57c12e267a29552eda2dbd45 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Wed, 29 Jan 2025 03:35:21 -0500
Subject: [PATCH 16/19] Fix build-book output directory

---
 scripts/build-book | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/scripts/build-book b/scripts/build-book
index 62af9b9..fd108e3 100755
--- a/scripts/build-book
+++ b/scripts/build-book
@@ -74,9 +74,9 @@ 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;
+    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

From 5aa490acae5f233cd33dc628d9aee7a27b3ad01e Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Thu, 13 Feb 2025 22:58:29 -0500
Subject: [PATCH 17/19] Year 2015 Day 14 Part 1

---
 README.md                |   4 ++
 advent.ipkg              |   2 +-
 src/SUMMARY.md           |   1 +
 src/Years/Y2015.md       |   7 ++
 src/Years/Y2015/Day14.md | 137 +++++++++++++++++++++++++++++++++++++++
 5 files changed, 150 insertions(+), 1 deletion(-)
 create mode 100644 src/Years/Y2015/Day14.md

diff --git a/README.md b/README.md
index 763edcc..48f7b08 100644
--- a/README.md
+++ b/README.md
@@ -136,6 +136,10 @@ solution.
 
     Naive ring buffer and `parameters` blocks[^2]
 
+  - [Day 14](src/Years/Y2015/Day14.md)
+
+    Introduction to streams, infinite collections of data
+
 ## References
 
 [^1]: Idris 2 Manual:
diff --git a/advent.ipkg b/advent.ipkg
index 607e26e..d4d13fe 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -41,7 +41,7 @@ main = Main
 
 -- name of executable
 executable = "advent"
--- opts =
+opts = "--directive lazy=weakMemo"
 sourcedir = "src"
 -- builddir =
 -- outputdir =
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 9447a3a..3fad4c9 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -35,3 +35,4 @@
   - [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)
+  - [Day 14 - Introduction to Streams](Years/Y2015/Day14.md)
diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md
index 79ae4e8..d4a3b19 100644
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@@ -20,6 +20,7 @@ import Years.Y2015.Day10
 import Years.Y2015.Day11
 import Years.Y2015.Day12
 import Years.Y2015.Day13
+import Years.Y2015.Day14
 ```
 
 # Days
@@ -108,6 +109,12 @@ y2015 = MkYear 2015 [
   , day13
 ```
 
+## [Day 14](Y2015/Day14.md)
+
+```idris
+  , day14
+```
+
 ```idris
   ]
 ```
diff --git a/src/Years/Y2015/Day14.md b/src/Years/Y2015/Day14.md
new file mode 100644
index 0000000..3de7430
--- /dev/null
+++ b/src/Years/Y2015/Day14.md
@@ -0,0 +1,137 @@
+# [Year 2015 Day 14](https://adventofcode.com/2015/day/14)
+
+This day provides us an introduction to streams, infinite, lazily generated,
+collections of data.
+
+```idris hide
+module Years.Y2015.Day14
+
+import Data.Primitives.Interpolation
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+import Data.String
+import Data.List1
+import Data.Vect
+import Data.Stream
+import Decidable.Equality
+
+import Util
+```
+
+## Parsing And Datastructures
+
+Collect the aspects defining a reindeer into a record
+
+```idris
+record Reindeer where
+  constructor MkReindeer
+  name : String
+  speed : Nat
+  duration, rest : Nat
+```
+
+```idris hide
+Show Reindeer where
+  show (MkReindeer name speed duration rest) = 
+    "MkReindeer \{name} \{speed} \{duration} \{rest}"
+```
+
+This time around, since the lines describing a reindeer contain a lot of cruft,
+we'll handle the parsing by converting the input, after splitting it on space
+characters, to a `Vect`, and indexing into that `Vect`.
+
+```idris
+parseReindeer : Has (Except String) fs =>
+  (input : String) -> Eff fs Reindeer
+parseReindeer input = do
+  parts <- note "Input has wrong size: \{input}" $
+    toVect 15 . forget . split (== ' ') . trim $ input
+  let name = index 0 parts
+  speed <- note "" $
+    parsePositive $ index 3 parts
+  duration <- note "" $
+    parsePositive $ index 6 parts
+  rest <- note "" $
+    parsePositive $ index 13 parts
+  pure $ MkReindeer name speed duration rest
+```
+
+### Solver Functions
+
+A stream is an infinite analog of a list, storing an infinite collection of
+(lazily generated) values.
+
+Streams are defined like:
+
+```idris
+data Stream' : Type -> Type where
+  (::) : a -> Inf (Stream' a) -> Stream' a
+```
+
+Streams are a member of a family of concepts analogous to iterators in
+imperative languages, the different flavors of colist.
+
+Colists are the codata duals of lists, we'll dig more into to this later, but to
+provide a high level summary, where data is defined by how it is constructed,
+codata is defined by how it is destructed. While a list is defined by how you
+can cons an element `x` onto a list `xs` to produce a new list `x :: xs`, a
+colist is defined by how you can break down a colist `x :: xs` into a head `x`
+and a tail `xs`.
+
+Streams are a particular type of colist that has no empty case, breaking down a
+`Stream` will always produce an element and another stream, resulting in streams
+always being infinite in length.
+
+Destructing a `Stream` by pattern matching is semantically equivalent to calling
+the `next` method on an iterator in a language like rust, it produces the
+element at the head of a stream, and a new stream producing future elements.
+
+We will model are reindeer's future history of locations as a stream, with each
+element being the position at the time given by the index into the stream,
+generating it with a pair of mutually recursive functions. The `run` function
+adds the speed to current position to produce the next one, and the `rest`
+function doesn't modify the position whill still consuming a time step.
+
+```idris
+distances : Reindeer -> Stream Nat
+distances x = run x x.duration 0
+  where
+    run : (deer : Reindeer) -> (left : Nat) -> (position : Nat) 
+     -> Stream Nat
+    rest : (deer : Reindeer) -> (left : Nat) -> (position : Nat) 
+     -> Stream Nat
+    run deer 0 position = rest deer deer.rest position
+    run deer (S k) position = position :: run deer k (position + deer.speed)
+    rest deer 0 position = run deer deer.duration position
+    rest deer (S k) position = position :: rest deer k position
+```
+
+## Part Functions
+
+### Part 1
+
+Parse the input, generate the position `Stream`s for each reindeer, then index
+the finish position in each stream.
+
+```idris
+part1 : Eff (PartEff String) (Nat, ())
+part1 = do
+  lines <- map (lines) $ askAt "input"
+  reindeer <- traverse parseReindeer lines
+  debug $ show reindeer
+  let dists = map distances reindeer
+  let dists_end = map (index 2503) dists
+  let max = maxBy compare 0 dists_end
+  pure (max, ())
+```
+
+```idris hide
+public export
+day14 : Day 
+day14 = First 14 part1
+```

From 0fc8fa7e18d0f39c665127206fcac29cc78fb5dc Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sun, 16 Feb 2025 04:03:28 -0500
Subject: [PATCH 18/19] Add listToVect to util

---
 src/Util.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Util.md b/src/Util.md
index 9264794..7d1342e 100644
--- a/src/Util.md
+++ b/src/Util.md
@@ -192,6 +192,14 @@ Lazily generate all the permutations of a Vect
   maxBy f (x :: xs) = Foldable.maxBy f x xs
 ```
 
+### Convert a list to a vect as a sigma type
+
+```idris
+  export
+  listToVect : List a -> (n : Nat ** Vect n a)
+  listToVect xs = (length xs ** fromList xs)
+```
+
 ## Fin
 
 ```idris hide

From a282846972a69ca6623222395a07da6fff6f2e4b Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sun, 16 Feb 2025 04:03:39 -0500
Subject: [PATCH 19/19] Year 2015 Day 14 Part 2

---
 src/Years/Y2015/Day14.md | 40 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 38 insertions(+), 2 deletions(-)

diff --git a/src/Years/Y2015/Day14.md b/src/Years/Y2015/Day14.md
index 3de7430..5418617 100644
--- a/src/Years/Y2015/Day14.md
+++ b/src/Years/Y2015/Day14.md
@@ -18,6 +18,7 @@ import Data.String
 import Data.List1
 import Data.Vect
 import Data.Stream
+import Data.Zippable
 import Decidable.Equality
 
 import Util
@@ -111,6 +112,24 @@ distances x = run x x.duration 0
     rest deer (S k) position = position :: rest deer k position
 ```
 
+Carry an accumulator containing the scores for each reindeer down the stream, at
+each position, granting one point to each reindeer at the leader position after
+the end of the second.
+
+```idris
+leaderScoring : {n : _} -> Vect (S n) (Stream Nat) -> Stream (Vect (S n) Nat)
+leaderScoring xs = leaderScoring' (replicate _ 0) xs
+  where
+    leaderScoring' : {n : _} -> (acc : Vect (S n) Nat) -> Vect (S n) (Stream Nat)
+      -> Stream (Vect (S n) Nat)
+    leaderScoring' acc xs = 
+      let positions = map (head . tail) xs
+          leader_pos = maxBy compare 0 positions
+          points : Vect _ Nat = 
+            map (\x => if x == leader_pos then 1 else 0) positions
+      in acc :: leaderScoring' (zipWith (+) acc points) (map tail xs)
+```
+
 ## Part Functions
 
 ### Part 1
@@ -121,7 +140,7 @@ the finish position in each stream.
 ```idris
 part1 : Eff (PartEff String) (Nat, ())
 part1 = do
-  lines <- map (lines) $ askAt "input"
+  lines <- map lines $ askAt "input"
   reindeer <- traverse parseReindeer lines
   debug $ show reindeer
   let dists = map distances reindeer
@@ -130,8 +149,25 @@ part1 = do
   pure (max, ())
 ```
 
+Parse the input into a vect, and make sure it is not empty, then generate the
+stream with the `leaderScoring` function and index into it.
+
+```idris
+part2 : () -> Eff (PartEff String) Nat
+part2 x = do
+  lines <- map lines $ askAt "input"
+  let (len ** lines) = listToVect lines
+  case len of
+    0 => throw "No reindeer :("
+    (S k) => do
+    reindeer <- traverse parseReindeer lines
+    let dists = leaderScoring $ map distances reindeer
+    let dists_end = index 2503 dists
+    pure $ maxBy compare 0 dists_end
+```
+
 ```idris hide
 public export
 day14 : Day 
-day14 = First 14 part1
+day14 = Both 14 part1 part2
 ```