Fix build-book output directory

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>

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

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)

src/Util.md

@@ -10,10 +10,50 @@ 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
@@ -56,13 +96,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 +116,94 @@ 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))
+```
+
+### 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
@@ -166,20 +284,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 +309,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 +320,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
 ```

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

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>