Compare commits
No commits in common. "trunk" and "develop" have entirely different histories.
10
README.md
10
README.md
|
|
@ -128,17 +128,7 @@ solution.
|
|||
|
||||
Introduces refinement types
|
||||
|
||||
- [Day 12](src/Years/Y2015/Day12.md)
|
||||
|
||||
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>
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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 copy-to-dest($src) {
|
||||
sub cp-temp($src) {
|
||||
my $src-path = do given $src {
|
||||
when Str {
|
||||
$src.IO
|
||||
|
|
@ -45,16 +45,40 @@ sub copy-to-dest($src) {
|
|||
$src-path.resolve.copy: $output-path;
|
||||
}
|
||||
|
||||
# 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;
|
||||
# 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);
|
||||
}
|
||||
|
||||
# Copy our metadata files
|
||||
copy-to-dest "book.toml";
|
||||
copy-to-dest "src/SUMMARY.md";
|
||||
cp-temp "book.toml";
|
||||
cp-temp "src/README.md";
|
||||
cp-temp "src/SUMMARY.md";
|
||||
|
||||
# Katla over the source files
|
||||
for paths("src", :file(*.¬-ignored)) -> $path {
|
||||
|
|
@ -74,42 +98,7 @@ 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;
|
||||
}
|
||||
|
||||
# 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);
|
||||
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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -110,8 +110,7 @@ Provide wrappers for `rundownFirst` for evaluating it in various contexts.
|
|||
|
||||
```idris
|
||||
export
|
||||
runFirstIO : HasIO io => MonadRec io =>
|
||||
(f : Parser a) -> String -> io (Either ParseError a)
|
||||
runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a)
|
||||
runFirstIO f str = do
|
||||
Just state <- newInternalIO str
|
||||
| _ => pure . Left $ BeforeParse "Empty input"
|
||||
|
|
|
|||
|
|
@ -6,8 +6,6 @@ module Parser.JSON
|
|||
import public Parser
|
||||
import public Parser.Numbers
|
||||
|
||||
import Control.Monad.Eval
|
||||
|
||||
import Structures.Dependent.DList
|
||||
```
|
||||
|
||||
|
|
@ -57,7 +55,6 @@ data JSONValue : JSONType -> Type where
|
|||
```
|
||||
|
||||
```idris hide
|
||||
export
|
||||
Show (JSONValue t) where
|
||||
show (VObject xs) =
|
||||
let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
|
||||
|
|
@ -72,7 +69,6 @@ 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
|
||||
|
|
@ -86,96 +82,6 @@ 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
|
||||
```
|
||||
|
||||
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)
|
||||
```
|
||||
|
||||
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
|
||||
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,
|
||||
|
|
@ -262,7 +168,6 @@ object = do
|
|||
pairs = do
|
||||
first <- keyValue
|
||||
rest <- many restKeyValue
|
||||
-- TODO: headTail combinator for this
|
||||
pure $ first ::: rest
|
||||
occupiedObject : Parser (JSONValue TObject)
|
||||
occupiedObject = do
|
||||
|
|
|
|||
|
|
@ -33,5 +33,3 @@
|
|||
- [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)
|
||||
- [Day 13 - Naive Ring Buffer and parameters blocks](Years/Y2015/Day13.md)
|
||||
|
|
|
|||
223
src/Util.md
223
src/Util.md
|
|
@ -10,50 +10,10 @@ 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
|
||||
|
|
@ -96,13 +56,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
|
||||
|
|
@ -116,94 +76,16 @@ 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)
|
||||
```
|
||||
|
||||
### 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
|
||||
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)
|
||||
```
|
||||
|
||||
## Vectors
|
||||
|
|
@ -284,24 +166,20 @@ 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
|
||||
|
|
@ -309,10 +187,10 @@ Lazily take the cartesian product of two foldables
|
|||
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
|
||||
|
|
@ -320,30 +198,15 @@ Lazily concatenate a LazyList of LazyLists
|
|||
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)
|
||||
```
|
||||
|
||||
### 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
|
||||
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)
|
||||
```
|
||||
|
|
|
|||
|
|
@ -18,8 +18,6 @@ import Years.Y2015.Day8
|
|||
import Years.Y2015.Day9
|
||||
import Years.Y2015.Day10
|
||||
import Years.Y2015.Day11
|
||||
import Years.Y2015.Day12
|
||||
import Years.Y2015.Day13
|
||||
```
|
||||
|
||||
# Days
|
||||
|
|
@ -96,18 +94,6 @@ y2015 = MkYear 2015 [
|
|||
, day11
|
||||
```
|
||||
|
||||
## [Day 12](Y2015/Day12.md)
|
||||
|
||||
```idris
|
||||
, day12
|
||||
```
|
||||
|
||||
## [Day 13](Y2015/Day13.md)
|
||||
|
||||
```idris
|
||||
, day13
|
||||
```
|
||||
|
||||
```idris
|
||||
]
|
||||
```
|
||||
|
|
|
|||
|
|
@ -1,132 +0,0 @@
|
|||
# [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
|
||||
```
|
||||
|
||||
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
|
||||
|
||||
### Part 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))
|
||||
```
|
||||
|
||||
### 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 = Both 12 part1 part2
|
||||
```
|
||||
|
||||
## References
|
||||
|
||||
[^1]: <https://git.sr.ht/~thatonelutenist/Structures/tree/trunk/item/src/Structures/Dependent/DList.md>
|
||||
|
|
@ -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>
|
||||
Loading…
Reference in a new issue