Idris/advent
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: Idris:f675677a7647859c57c12e267a29552eda2dbd45
Branches Tags
Idris:trunk
Idris:develop
Idris:wat
..
compare: Idris:c632ab023dec68d9206f8a7dd1e18b73ef99b315
Branches Tags
Idris:trunk
Idris:develop
Idris:wat

No commits in common. "f675677a7647859c57c12e267a29552eda2dbd45" and "c632ab023dec68d9206f8a7dd1e18b73ef99b315" have entirely different histories.
f675677a76 ... c632ab023d

6 changed files with 46 additions and 460 deletions
Show stats Expand all files Collapse all files

6
README.md
View file

@ -132,13 +132,7 @@ solution.
New Parser Effect stack and DLists New Parser Effect stack and DLists
- [Day 13](src/Years/Y2015/Day13.md)
Naive ring buffer and `parameters` blocks[^2]
## References ## References
[^1]: Idris 2 Manual: [^1]: Idris 2 Manual:
[Views and the "with" rule](https://idris2.readthedocs.io/en/latest/tutorial/views.html#views-and-the-with-rule) [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>

2
scripts/build-book
View file

@ -74,7 +74,7 @@ rm_rf "book";
cp $tempdir.add("book"), "book", :r; cp $tempdir.add("book"), "book", :r;
if $upload { if $upload {
my $rsync = run 'rsync', '-avzh', $tempdir.add("book/").Str, my $rsync = run 'rsync', '-avzh', $tempdir.add("book").Str,
'ubuntu@static.stranger.systems:/var/www/static.stranger.systems/idris-by-contrived-example'; 'ubuntu@static.stranger.systems:/var/www/static.stranger.systems/idris-by-contrived-example';
die "rsync went bad" unless $rsync; die "rsync went bad" unless $rsync;
} }

1
src/SUMMARY.md
View file

@ -34,4 +34,3 @@
- [Day 10 - Digits View](Years/Y2015/Day10.md) - [Day 10 - Digits View](Years/Y2015/Day10.md)
- [Day 11 - Refinement Types](Years/Y2015/Day11.md) - [Day 11 - Refinement Types](Years/Y2015/Day11.md)
- [Day 12 - Custom Parser Effect and DLists](Years/Y2015/Day12.md) - [Day 12 - Custom Parser Effect and DLists](Years/Y2015/Day12.md)
- [Day 13 - Naive Ring Buffer and parameters blocks](Years/Y2015/Day13.md)

175
src/Util.md
View file

@ -10,50 +10,10 @@ import Data.SortedSet
import Data.String import Data.String
import Data.List.Lazy import Data.List.Lazy
import Data.List1 import Data.List1
import Data.Vect
import Data.Fin
%default total %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 ## Functions
### repeatN ### repeatN
@ -96,10 +56,10 @@ namespace List
Returns `True` if the list contains the given value Returns `True` if the list contains the given value
```idris ```idris
export export
contains : Eq a => a -> List a -> Bool contains : Eq a => a -> List a -> Bool
contains x [] = False contains x [] = False
contains x (y :: xs) = contains x (y :: xs) =
if x == y if x == y
then True then True
else contains x xs else contains x xs
@ -116,9 +76,9 @@ rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]
``` ```
```idris ```idris
export export
rotations : List a -> List (List a) rotations : List a -> List (List a)
rotations xs = rotations' (length xs) xs [] rotations xs = rotations' (length xs) xs []
where where
rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a) rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a)
rotations' 0 xs acc = acc rotations' 0 xs acc = acc
@ -128,84 +88,6 @@ rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]]
in rotations' k next (next :: acc) 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 ## Vectors
Define some operations for pairs of numbers, treating them roughly like vectors Define some operations for pairs of numbers, treating them roughly like vectors
@ -284,16 +166,12 @@ off of the string at a time, checking if the needle is a prefix at each step.
### Cartesian product ### Cartesian product
```idris hide
namespace LazyList
```
Lazily take the cartesian product of two foldables Lazily take the cartesian product of two foldables
```idris ```idris
export export
cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f) cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f)
cartProd x y = cartProd x y =
let y = foldToLazy y let y = foldToLazy y
in foldr (\e, acc => combine e y acc) [] x in foldr (\e, acc => combine e y acc) [] x
where where
@ -309,10 +187,10 @@ Lazily take the cartesian product of two foldables
Lazily concatenate a LazyList of LazyLists Lazily concatenate a LazyList of LazyLists
```idris ```idris
export export
lazyConcat : LazyList (LazyList a) -> LazyList a lazyConcat : LazyList (LazyList a) -> LazyList a
lazyConcat [] = [] lazyConcat [] = []
lazyConcat (x :: xs) = x ++ lazyConcat xs lazyConcat (x :: xs) = x ++ lazyConcat xs
``` ```
### Group ### Group
@ -320,30 +198,15 @@ Lazily concatenate a LazyList of LazyLists
Lazily group a LazyList Lazily group a LazyList
```idris ```idris
export export
lazyGroup : Eq a => LazyList a -> LazyList (List1 a) lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
lazyGroup [] = [] lazyGroup [] = []
lazyGroup (x :: xs) = lazyGroup' xs x (x ::: []) lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
where where
lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) -> LazyList (List1 a)
-> LazyList (List1 a)
lazyGroup' [] current acc = [acc] lazyGroup' [] current acc = [acc]
lazyGroup' (y :: ys) current acc@(head ::: tail) = lazyGroup' (y :: ys) current acc@(head ::: tail) =
if y == current if y == current
then lazyGroup' ys current (head ::: (y :: tail)) then lazyGroup' ys current (head ::: (y :: tail))
else acc :: lazyGroup (y :: ys) 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
```

7
src/Years/Y2015.md
View file

@ -19,7 +19,6 @@ import Years.Y2015.Day9
import Years.Y2015.Day10 import Years.Y2015.Day10
import Years.Y2015.Day11 import Years.Y2015.Day11
import Years.Y2015.Day12 import Years.Y2015.Day12
import Years.Y2015.Day13
``` ```
# Days # Days
@ -102,12 +101,6 @@ y2015 = MkYear 2015 [
, day12 , day12
``` ```
## [Day 13](Y2015/Day13.md)
```idris
, day13
```
```idris ```idris
] ]
``` ```

263
src/Years/Y2015/Day13.md
View file

@ -1,263 +0,0 @@
# [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>