README.md

@@ -136,10 +136,6 @@ 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:

advent.ipkg

@@ -41,7 +41,7 @@ main = Main
 
 -- name of executable
 executable = "advent"
-opts = "--directive lazy=weakMemo"
+-- opts =
 sourcedir = "src"
 -- builddir =
 -- outputdir =

src/SUMMARY.md

@@ -35,4 +35,3 @@
   - [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)

src/Util.md

@@ -192,14 +192,6 @@ 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

src/Years/Y2015.md

@@ -20,7 +20,6 @@ import Years.Y2015.Day10
 import Years.Y2015.Day11
 import Years.Y2015.Day12
 import Years.Y2015.Day13
-import Years.Y2015.Day14
 ```
 
 # Days
@@ -109,12 +108,6 @@ y2015 = MkYear 2015 [
   , day13
 ```
 
-## [Day 14](Y2015/Day14.md)
-
-```idris
-  , day14
-```
-
 ```idris
   ]
 ```

src/Years/Y2015/Day14.md

@@ -1,173 +0,0 @@
-# [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 Data.Zippable
-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
-```
-
-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
-
-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, ())
-```
-
-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 = Both 14 part1 part2
-```