From 5aa490acae5f233cd33dc628d9aee7a27b3ad01e Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 13 Feb 2025 22:58:29 -0500 Subject: [PATCH 1/3] 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 Date: Sun, 16 Feb 2025 04:03:28 -0500 Subject: [PATCH 2/3] 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 Date: Sun, 16 Feb 2025 04:03:39 -0500 Subject: [PATCH 3/3] 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 ```