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

Compare commits

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

2 commits
trunk ... wat

Author SHA1 Message Date
Nathan McCarty 9721602598 wat 2025-01-14 21:51:33 -05:00
Nathan McCarty 62510c6755 Day 8 template 2025-01-14 16:02:52 -05:00
33 changed files with 600 additions and 4150 deletions
Show stats Expand all files Collapse all files

2
.gitignore vendored
View file

@ -4,5 +4,3 @@ inputs/
support/*.o support/*.o
support/advent-support support/advent-support
tmp/ tmp/
book/
index.html

113
README.md
View file

@ -1,33 +1,10 @@
# Advent # Advent
The goal of this project is to get all 500 currently available stars in the form The goal of this project is to get all 500 currently available stars in the form
of one single Idris application, and thoroughly document the results as literate of one single idris application, and thoroughly document the results as literate
Idris files. idris files.
## Authors Note # Index of non-day modules
This entire book is a single literate code base, the source code is available at
<https://git.stranger.systems/Idris/advent>.
The solutions contained in this project are intended to be read in sequential
order, though can reasonably be read in any order if you have a good level of
familiarity with more advanced functional programming topics.
The solutions will involve progressively more advanced topics as day and year
number increase, though I try not to introduce too much within the scope of any
one day.
Suggestions and other feedback are highly welcome, please reach out to me via
any platform you know me on, or send an email to the
[~thatonelutenist/public-inbox](https://lists.sr.ht/~thatonelutenist/public-inbox)
mailing list on source hut.
While this project is intended to read more like a book, while it is still a
work in progress, you can follow its development as a psuedo-blog by subscribing
to the rss feed for the repository in your feed reader:
<https://git.stranger.systems/Idris/advent.rss>.
## Index of non-day modules
- [Runner](src/Runner.md) - [Runner](src/Runner.md)
@ -49,96 +26,14 @@ solution.
Extend the functionality of the effects included in the Extend the functionality of the effects included in the
[eff](https://github.com/stefan-hoeck/idris2-eff/) library [eff](https://github.com/stefan-hoeck/idris2-eff/) library
- [Util.Digits](src/Util/Digits.md) # Index of years and days
Provide views that enable recursively pattern matching numbers as lists of
digits, in both ascending and descending order of significance.
- [Array](src/Array.md)
Provider wrappers over the standard library `IOArray` type to make them more
ergonomic to use.
- [Parser](src/Parser.md)
Effectful parser mini-library
- [Interface](src/Parser/Interface.md)
Effectful parser API
- [ParserState](src/Parser/ParserState.md)
Internal state of a parser
- [Numbers](src/Parser/Numbers.md)
Parsers for numerical values in multiple bases
- [JSON](src/Parser/JSON.md)
JSON Parser
## Index of years and days
- 2015 - 2015
- [Day 1](src/Years/Y2015/Day1.md) - [Day 1](src/Years/Y2015/Day1.md)
Warm up problem, breaks in our new runner and not much else interesting.
- [Day 2](src/Years/Y2015/Day2.md) - [Day 2](src/Years/Y2015/Day2.md)
An early hint of effectful parsing.
- [Day 3](src/Years/Y2015/Day3.md) - [Day 3](src/Years/Y2015/Day3.md)
Peculiarities of writing mutually recursive functions in dependently typed
languages.
- [Day 4](src/Years/Y2015/Day4.md) - [Day 4](src/Years/Y2015/Day4.md)
Basic FFI to openssl to steal its MD5 function for Idris's use.
- [Day 5](src/Years/Y2015/Day5.md) - [Day 5](src/Years/Y2015/Day5.md)
First introduction to views and dependent pattern matching[^1].
- [Day 6](src/Years/Y2015/Day6.md) - [Day 6](src/Years/Y2015/Day6.md)
Naive approach to handling the first 2d grid problem.
- [Day 7](src/Years/Y2015/Day7.md) - [Day 7](src/Years/Y2015/Day7.md)
Introduces dependent maps and indexed type families.
- [Day 8](src/Years/Y2015/Day8.md) - [Day 8](src/Years/Y2015/Day8.md)
Proper effectful parsers and non-determinism in effect stacks.
- [Day 9](src/Years/Y2015/Day9.md)
Naive approach to handling the first graph traversal problem.
- [Day 10](src/Years/Y2015/Day10.md)
Introduce our `Digits`, dependent pattern matching on integers as lists of
digits.
- [Day 11](src/Years/Y2015/Day11.md)
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>

10
advent.ipkg
View file

@ -16,25 +16,17 @@ authors = "Nathan McCarty"
depends = base depends = base
, contrib , contrib
, structures , structures
, tailrec
, eff , eff
, elab-util , elab-util
, sop
, ansi , ansi
, if-unsolved-implicit , if-unsolved-implicit
, c-ffi , c-ffi
, refined
-- modules to install -- modules to install
modules = Runner modules = Runner
, Util , Util
, Util.Eff , Util.Eff
, Util.Digits , Grid
, Array
, Parser
, Parser.Interface
, Parser.Numbers
, Parser.JSON
-- main file (i.e. file to load at REPL) -- main file (i.e. file to load at REPL)
main = Main main = Main

13
book.toml
View file

@ -1,13 +0,0 @@
[book]
authors = ["Nathan McCarty"]
language = "en"
multilingual = false
src = "src"
title = "Idris 2 by Highly Contrived Example"
[build]
create-missing = false
# use-default-preprocessors = false
[output.html]
preferred-dark-theme = "ayu"

115
scripts/build-book
View file

@ -1,115 +0,0 @@
#!/usr/bin/env raku
use File::Temp;
use Shell::Command;
use paths;
unit sub MAIN(Bool :$upload);
my $tempdir = tempdir.IO;
my $ttc-number = dir('build/ttc').first.basename;
my $ttc = "build/ttc/$ttc-number".IO;
# Filenames to ignore while processing source files
my Str:D @ignored = ["README.md", "SUMMARY.md"];
# Check to see if a filename is ignored
sub not-ignored($path) {
for @ignored -> $ignored {
return False if $path.ends-with: $ignored;
}
return True;
}
# 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) {
my $src-path = do given $src {
when Str {
$src.IO
}
when IO::Path {
$src
}
default {
die "Invalid source $src, {$src.WHAT}"
}
}
my $output-path = $tempdir.add($src-path.relative).IO;
# Create the parent directory if needed
if !$output-path.parent.d {
$output-path.parent.mkdir;
}
# Copy the file
$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;
# Copy our metadata files
copy-to-dest "book.toml";
copy-to-dest "src/SUMMARY.md";
# Katla over the source files
for paths("src", :file(*.&not-ignored)) -> $path {
my $ttc-path = $ttc.add($path.IO.relative: "src").extension: "ttm";
katla $path.IO.relative, $ttc-path.relative;
}
# Build the book
indir $tempdir, {
my $mdbook = run <mdbook build>;
die "Ooops" unless $mdbook;
}
# Copy it over
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);
}

537
src/Array.md
View file

@ -1,537 +0,0 @@
# Array Wrappers
```idris
module Array
import Data.IOArray
import Data.Vect
import Data.List.Lazy
import Data.Fin
import Data.Iterable
import Decidable.Equality
import Control.WellFounded
```
```idris hide
import System
```
```idris
%default total
%hide Prelude.Types.elem
```
Provide some wrappers over the standard library IO arrays, using plenty of
unsafe operations along the way.
## Internal Utility Functions
Unsafely unwrap a `Maybe`, making the assumption that it is a `Just`.
```idris
%unsafe
unwrapUnsafe : Maybe a -> a
unwrapUnsafe x = assert_total $ unwrapUnsafe' x
where
partial
unwrapUnsafe' : Maybe a -> a
unwrapUnsafe' (Just x) = x
```
Insert an element into an `IOArray` at the index described by the given `Fin`.
```idris
insertPair : IOArray e -> (e, Fin n) -> IO ()
insertPair arr (elem, idx) = do
let idx : Int = cast . finToInteger $ idx
_ <- writeArray arr idx elem
pure ()
```
### Tail safe monadic recursion with lazy lists
Generate all of the fins of a given size, lazily.
```idris
allFins : (n : Nat) -> LazyList (Fin n)
allFins 0 = []
allFins (S k) = FZ :: map FS (allFins k)
```
LazyLists have a size
```idris
Sized (LazyList e) where
size [] = 0
size (x :: xs) = S (size xs)
```
Convert a `Vect` to a `LazyList`
```idris
vectLazy : Vect n e -> LazyList e
vectLazy [] = []
vectLazy (x :: xs) = x :: vectLazy xs
```
LazyLists are iterable
```idris
refl : {k : Nat} -> LTE k k
refl = reflexive {x = k}
Iterable (LazyList a) a where
iterM accum done ini seed =
trSized seed ini $
\case Nil => pure . Done . done
h :: t => map (Cont t refl) . accum h
```
## Immutable arrays
```idris hide
namespace Immutable
```
Immutable arrays created from vectors that provide constant time indexing and
slicing operations.
As an invariant of the the type, every "slot" in the inner `IOArray` must always
be a `Just`, unsafe operations are performed that depend on that.
```idris
||| An immutable array of length `n`
export
data IArray : Nat -> Type -> Type where
MkIArray : (size : Nat) -> (offset : Int) -> (inner : IOArray e)
-> IArray size e
%name IArray xs, ys, zs
```
### Basic Interface
Indexing operation
```idris
export
index : (idx : Fin n) -> IArray n e -> e
index idx (MkIArray size offset inner) = unsafePerformIO index'
where
index' : IO e
index' = do
-- Convert the index to an Int for use in the IO array
let idx : Int = cast . finToInteger $ idx
map unwrapUnsafe $ readArray inner (idx + offset)
```
Getting the length of an `IArray`, as well as a proof of correctness for the
length function
```idris
export
length : IArray n e -> Nat
length (MkIArray n _ inner) = n
export
lengthCorrect : (array : IArray n e) -> length array = n
lengthCorrect (MkIArray n _ inner) = Refl
```
Basic conversion operations
```idris
export
fromVect : {n : Nat} -> Vect n e -> IArray n e
fromVect xs = unsafePerformIO fromVect'
where
fromVect' : IO $ IArray n e
fromVect' = do
let pairs = zip (vectLazy xs) (allFins n)
array <- newArray (cast n)
forM_ (insertPair array) pairs
pure $ MkIArray n 0 array
export
replicate : (n : Nat) -> e -> IArray n e
replicate n x = unsafePerformIO replicate'
where
insertR : IOArray e -> Fin n -> IO ()
insertR arr idx = do
let idx : Int = cast . finToInteger $ idx
_ <- writeArray arr idx x
pure ()
replicate' : IO $ IArray n e
replicate' = do
array <- newArray (cast n)
forM_ (insertR array) (Array.allFins n)
pure $ MkIArray n 0 array
export
toVect : IArray n e -> Vect n e
toVect xs =
let xs' : IArray (length xs) e = rewrite lengthCorrect xs in xs
values : Vect _ e = map (flip index $ xs') (allFins _)
in rewrite sym $ lengthCorrect xs in values
arrayToList : IArray n e -> List e
arrayToList xs =
let xs' : IArray (length xs) e = rewrite lengthCorrect xs in xs
in map (flip index $ xs') (allFins (length xs))
```
Unsafely create an array from a lazy list of values, for internal use only. Will
cause crashes if the provided `LazyList` isn't the right length.
```idris
%unsafe
unsafeFromLazy : {n : Nat} -> LazyList e -> IO (IArray n e)
unsafeFromLazy xs = do
array <- newArray (cast n)
let pairs = zip xs (allFins n)
forM_ (insertPair array) pairs
pure $ MkIArray _ 0 array
```
Typical drop and take operations, implemented in constant time
```idris
-- TODO: Minimize whatever compiler bug is requiring us to use this
newOffset : Nat -> Int -> Int
newOffset k i = cast k + i
export
drop : (n : Nat) -> IArray (n + m) e -> IArray m e
drop n xs@(MkIArray _ offset inner) =
believe_me $ MkIArray (length xs `minus` n) (newOffset n offset) inner
export
drop' : (n : Nat) -> IArray l e -> IArray (minus l n) e
drop' n (MkIArray l offset inner) =
if n >= l
then believe_me $ fromVect [] {e}
else MkIArray (l `minus` n) (newOffset n offset) inner
export
take : (n : Nat) -> IArray (n + m) e -> IArray n e
take n (MkIArray _ offset inner) = MkIArray n offset inner
```
A view for pattern matching on `IArray`s as if they were lists
```idris
namespace View
public export
data AsList : IArray n e -> Type where
Nil : {0 tail : IArray 0 e} -> AsList tail
(::) : {0 xs : IArray (S n) e} -> {rest : IArray n e}
-> (head : e) -> (tail : Lazy (AsList rest)) -> AsList xs
public export
asList : (xs : IArray n e) -> AsList xs
asList (MkIArray 0 offset inner) = []
asList xs@(MkIArray (S k) offset inner) =
let head = 0 `index` xs
rest = drop 1 xs
in head :: (asList rest)
```
Convert to a `LazyList` using our view
```idris
export
toLazy : IArray n e -> LazyList e
toLazy xs with (asList xs)
toLazy xs | [] = []
toLazy xs | (head :: tail) =
head :: toLazy _ | tail
```
Typical filtering and finding interface
```idris
-- Don't know if this one is really worth optimizing
export
filter : (e -> Bool) -> IArray n e -> (p : Nat ** IArray p e)
filter f xs =
let (_ ** ps) = filter f (toVect xs)
in (_ ** fromVect ps)
export
find : (e -> Bool) -> IArray n e -> Maybe e
find f xs with (asList xs)
find f xs | [] = Nothing
find f xs | (head :: tail) =
if f head
then Just head
else find f _ | tail
export
findIndex : (e -> Bool) -> IArray n e -> Maybe (Fin n)
findIndex f xs =
let indexed = zip (toLazy xs) (allFins (length xs))
in findIndex' f indexed
where
findIndex' : (e -> Bool) -> LazyList (e, Fin (length xs)) -> Maybe (Fin n)
findIndex' f [] = Nothing
findIndex' f ((e, idx) :: ys) =
if f e
then rewrite sym $ lengthCorrect xs in Just idx
else findIndex' f ys
export
findIndices : (e -> Bool) -> IArray n e -> List (Fin n)
findIndices f xs@(MkIArray n _ _) =
let pairs = zip (toLazy xs) (allFins n)
in toList . map snd . filter (f . fst) $ pairs
```
### Interface Implementations
Provide a `Foldable` implementation by performing indexing within the context of
`unsafePerformIO`.
```idris
export
Foldable (IArray n) where
foldl f acc_val (MkIArray n offset inner) = unsafePerformIO $ foldl'
where
liftF : Fin n -> acc -> IO acc
liftF idx acc_val = do
let idx : Int = cast . finToInteger $ idx
val <- map unwrapUnsafe $ readArray inner (idx + offset)
pure $ f acc_val val
foldl' : IO acc
foldl' = iterM liftF id acc_val (Array.allFins n)
foldr f acc_val (MkIArray n offset inner) = unsafePerformIO $ foldr'
where
liftF : Fin n -> acc -> IO acc
liftF idx acc_val = do
let idx : Int = cast . finToInteger $ idx
val <- map unwrapUnsafe $ readArray inner (idx + offset)
pure $ f val acc_val
foldr' : IO acc
-- TODO: Make a lazy reverse allFins function so we aren't instantiating
-- the full index list here
foldr' = iterM liftF id acc_val (reverse $ List.allFins n)
toList = arrayToList
```
Provide implementations of `Eq`, `Ord`, and `DecEq` in terms of our `AsList`
view. The `DecEq` implementation requires use of unsafe `believe_me`, as arrays
are primitive types the compiler has no insight into the structure of.
```idris
export
Eq e => Eq (IArray n e) where
xs == ys = (toLazy xs) == (toLazy ys)
export
Ord e => Ord (IArray n e) where
compare xs ys = compare (toLazy xs) (toLazy ys)
-- TODO : Optimize IArray DecEq
decEq' : DecEq e => {m : Nat} -> (xs, ys : IArray m e) -> Dec (xs = ys)
decEq' xs ys with (asList xs, asList ys)
decEq' xs ys | ([], []) = believe_me $ the (xs = xs) Refl
decEq' xs ys | ((h_x :: t_x), (h_y :: t_y)) =
case decEq h_x h_y of
Yes prf =>
believe_me $ decEq' _ _ | (t_x, t_y)
No contra => believe_me contra
export
DecEq e => DecEq (IArray n e) where
decEq xs@(MkIArray n _ _) ys = decEq' xs ys
```
Provide `Functor`, `Applicative`, `Monad`, and `Traverseable` implementations by
building a new array in an `IO` context
```idris
map' : (f : a -> b) -> IArray n a -> IO (IArray n b)
map' f xs@(MkIArray n _ _) = do
array <- newArray (cast n)
let pairs = zip (map f . toLazy $ xs) (Array.allFins n)
forM_ (insertPair array) pairs
pure $ MkIArray n 0 array
export
Functor (IArray k) where
map f xs = unsafePerformIO $ map' f xs
apply' : {n : Nat} -> IArray n (a -> b) -> IArray n a -> IO (IArray n b)
apply' fs xs = do
array <- newArray (cast n)
let applied = map (\(f, x) => f x) $ zip (toLazy fs) (toLazy xs)
let pairs = zip applied (allFins n)
forM_ (insertPair array) pairs
pure $ MkIArray n 0 array
-- Applicative requires the length of the array to be available at runtime at
-- the type level for `replicate`
export
{k : Nat} -> Applicative (IArray k) where
pure = replicate _
fs <*> xs = unsafePerformIO $ apply' fs xs
-- Like `Vect`'s `join`, this takes the diagonal elements
export
{k : Nat} -> Monad (IArray k) where
join xs =
let lazys = join' . map toLazy $ toLazy xs
in assert_total $ unsafePerformIO $ unsafeFromLazy lazys
where
covering
join' : LazyList (LazyList a) -> LazyList a
join' [] = []
join' ([] :: y) = []
join' ((x :: _) :: xs) =
x :: join' (map (drop 1) xs)
-- join xs = fromVect . join . map toVect . toVect $ xs
-- TODO: Maybe take another pass at optimizing this?
export
Traversable (IArray k) where
traverse fun xs@(MkIArray k _ _) =
map (unsafePerformIO . unsafeFromLazy . fromList)
. Prelude.traverse fun
. toList
$ xs
```
Provide a `Show` implementation in terms of our `AsList` view through the
`asLazy` wrapper.
```idris
export
Show e => Show (IArray n e) where
show xs =
let elements = map show $ toLazy xs
in case elements of
[] => "[]"
(x :: xs) => "[\{join' xs x}]"
where
join' : LazyList String -> (acc : String) -> String
join' [] acc = acc
join' (x :: []) acc = "\{acc}, \{x}"
join' (x :: (y :: xs)) acc =
join' (y :: xs) "\{acc}, \{x}"
```
Provide a `Zippable` implementation by roundtripping through a `Vect`. This
isn't the most efficient, but this provides a workable starter implementation.
```idris
export
Zippable (IArray k) where
zipWith f xs@(MkIArray k _ _) ys =
unsafePerformIO . unsafeFromLazy $ zipWith f (toLazy xs) (toLazy ys)
zipWith3 f xs@(MkIArray k _ _) ys zs =
unsafePerformIO . unsafeFromLazy $ zipWith3 f (toLazy xs) (toLazy ys) (toLazy zs)
unzipWith f xs@(MkIArray k _ _) =
let (xs, ys) = unzipWith f (toLazy xs)
in (unsafePerformIO . unsafeFromLazy $ xs,
unsafePerformIO . unsafeFromLazy $ ys)
unzipWith3 f xs@(MkIArray k _ _) =
let (xs, ys, zs) = unzipWith3 f (toLazy xs)
in (unsafePerformIO . unsafeFromLazy $ xs,
unsafePerformIO . unsafeFromLazy $ ys,
unsafePerformIO . unsafeFromLazy $ zs)
```
Provide `Semigroup` and `Monoid` implementations, matching those for `Vect`, in
terms of our other interfaces.
```idris
export
Semigroup a => Semigroup (IArray k a) where
xs <+> ys = zipWith (<+>) xs ys
-- Monoid requires the length argument to be available at runtime for
-- `replicate` to work
export
{k : Nat} -> Monoid a => Monoid (IArray k a) where
neutral = replicate _ neutral
```
## Unit tests
### IArray
```idris
-- @@test IArray RoundTrip
iRoundTrip : IO Bool
iRoundTrip = do
let test_vect : Vect _ Nat = [1, 2, 3, 4, 5]
putStrLn "test_vect: \{show test_vect}"
let xs = fromVect test_vect
putStrLn "xs: \{show xs}"
let round_tripped = toVect xs
putStrLn "round_tripped: \{show round_tripped}"
pure $ test_vect == round_tripped
-- @@test IArray drop/take
iDropTake : IO Bool
iDropTake = do
let test = fromVect [1, 2, 3, 4, 5]
putStrLn "test: \{show test}"
let dropped = drop 2 test
putStrLn "dropped: \{show dropped}"
let taked = take 3 test
putStrLn "taked: \{show taked}"
pure $ (toVect dropped) == [3, 4, 5] && (toVect taked) == [1, 2, 3]
-- @@test IArray toLazy
iLazy : IO Bool
iLazy = do
let test_vect : Vect _ Nat = [1, 2, 3, 4, 5]
let test_array = fromVect test_vect
putStrLn "test_array: \{show test_array}"
let output_lazy = toLazy test_array
putStrLn "output_lazy: \{show output_lazy}"
pure $ vectLazy test_vect == output_lazy
-- @@test IArray foldl/foldr
iFold : IO Bool
iFold = do
let test = fromVect [1, 2, 3, 4, 5]
putStrLn "test: \{show test}"
let foldl_test = foldl (flip (::)) [] test
putStrLn "foldl_test: \{show foldl_test}"
let foldr_test = foldr (::) [] test
putStrLn "foldr_test: \{show foldr_test}"
pure $ foldl_test == [5, 4, 3, 2, 1] && foldr_test == [1, 2, 3, 4, 5]
-- @@test IArray functor
iFunctor : IO Bool
iFunctor = do
let test = fromVect [1, 2, 3, 4, 5]
putStrLn "test: \{show test}"
let output = map (+ 1) test
putStrLn "output: \{show output}"
pure $ toVect output == [2, 3, 4, 5, 6]
-- @@test IArray show
iShow : IO Bool
iShow = do
let test = fromVect [1, 2, 3, 4, 5]
putStrLn "test: \{show test}"
let empty : IArray _ Nat = fromVect []
putStrLn "empty: \{show empty}"
let singleton = fromVect [1]
putStrLn "singleton: \{show singleton}"
pure $
show test == "[1, 2, 3, 4, 5]"
&& show empty == "[]"
&& show singleton == "[1]"
-- @@test IArray monad
iMonad : IO Bool
iMonad = do
let test_vect : Vect 3 (Vect 3 Nat) = [[1, 2, 3], [4, 5, 6], [7, 8 ,9]]
let test_array = fromVect $ map fromVect test_vect
let vect_out = join test_vect
let array_out = join test_array
putStrLn "vect: \{show vect_out} array: \{show array_out}"
pure $ toVect array_out == vect_out
```

371
src/Grid.md Normal file
View file

@ -0,0 +1,371 @@
# 2D Grid utilities
Types and utilities for dealing with a 2D grid of things
We base our `Grid` type on `Data.Seq.Sized` from `contrib`, a finger tree based
collection that tracks its size in its type, since it provides somewhat
efficient random access and updates.
```idris
module Grid
import Data.Seq.Sized
import Data.Fin
import Data.Fin.Extra
import Data.List.Lazy
import Data.Zippable
import Data.Vect
import Data.String
import Decidable.Equality
%default total
```
## Coordinates
A coordinate is a pair of numbers both less than their respective bounds.
Since `Grid`s will always be non-empty in the contexts we will be using them in,
this type alias adds one to each of the bounds to ensure non-emptyness
```idris
public export
Coord : (rows, cols : Nat) -> Type
Coord rows cols = (Fin (S rows), Fin (S cols))
```
### Coordinate utility functions
Lazily generate all the coordinates for a given pair of bounds
Uses an internal helper function to generate a lazy list of all the fins of a
given bound in ascending order (`all`), and another to convert a lazy list of
`Fin` into a lazy list of pairs of `Fin`s.
The totality checker likes to go in the descending direction, since then it can
reason about values getting structurally "smaller", so it has issues with `all'`
moving in the ascending direction. We know this function is total because the
`acc < last` check will always eventually be triggered, since `Fin`s only have a
finite number of values.
We pull out an `assert_smaller` to tell Idris that the argument to the recursive
call is getting structurally smaller, which while not strictly correct, does
convey to the compiler that we are getting closer to our recursive base case and
that the function is thus total.
```idris
export
allCords : {rows, cols : Nat} -> LazyList (Coord rows cols)
allCords = concat . map row $ all
where
all : {n : Nat} -> LazyList (Fin (S n))
all = FZ :: all' FZ
where
all' : {n : Nat} -> (acc : Fin (S n)) -> LazyList (Fin (S n))
all' acc =
if acc < last
then finS acc :: all' (assert_smaller acc (finS acc))
else []
row : Fin (S rows) -> LazyList (Coord rows cols)
row r = map (\c => (r, c)) all
```
Add a given vector to a coordinate, returning `Nothing` if we go off the ends of
the bounds in the process.
To keep this function simple and reasonably efficient, we perform the arithmetic
in integer space, using `integerToFin` to fallably convert back to `Fin` space,
making use of the `Maybe` monad to keep the code clean.
```idris
export
step : {rows, cols : Nat} -> (input : Coord rows cols) -> (direction : (Integer, Integer))
-> Maybe (Coord rows cols)
step (row, col) (d_row, d_col) = do
let (row, col) = (finToInteger row, finToInteger col)
row <- integerToFin (row + d_row) (S rows)
col <- integerToFin (col + d_col) (S cols)
pure (row, col)
```
## Grid
A grid is a `Seq` of `Seq`s with the given size bounds.
The inner `Seq`s are kept opaque to maintain flexability in the implementation
```idris
export
record Grid (rows, cols : Nat) (e : Type) where
constructor MkGrid
grid : Seq (S rows) (Seq (S cols) e)
%name Grid grid, grid2, grid3
```
### Constructors
Construct a `Grid` by filling every slot with identical copies of the provided
element
```idris
export
replicate : {rows, cols : Nat} -> (seed : e) -> Grid rows cols e
replicate seed =
let row = replicate (S cols) seed
grid = replicate (S rows) row
in MkGrid grid
```
Attempt to construct a `Grid` from a Foldable of Foldables. Will return
`Nothing` if either the rows are of heterogeneous size, or if either the rows or
columns are empty. Requires that the outer Foldable also be Traversable.
We make heavy use of the `Maybe` monad to keep the code clean here.
```idris
export
fromFoldable : Traversable a => Foldable a => Foldable b => a (b e) ->
Maybe (rows : Nat ** cols : Nat ** Grid rows cols e)
fromFoldable xs = do
-- First collect the number of rows from the outer foldable
let (S rows) = foldl (\acc, e => acc + 1) 0 xs
| _ => Nothing -- Return Nothing if there are no rows
-- Get the number of columns in the largest row in the inner foldable
let (S cols) = foldl (\acco, eo => max acco (foldl (\acci, ei => acci +1) 0 eo)) 0 xs
| _ => Nothing -- Return Nothing if all the rows are empty
-- Convert the rows by traversing our foldToSeq function over the outer foldable
xs <- traverse (foldToSeq (S cols)) xs
-- Reuse our foldToSeq helper function to convert the outer foldable
xs <- foldToSeq (S rows) xs
-- wrap it up and return
pure (rows ** cols ** MkGrid xs)
where
-- Convert each row to a seq using an intermediate list
foldToSeq : Foldable c => (n : Nat) -> c f -> Maybe (Seq n f)
foldToSeq n x =
let list = toList x
-- Check to see if the list is of the correct length, then rewrite the
-- output type to match if that's the case, otherwise return Nothing
in case decEq (length list) n of
Yes Refl => Just $ fromList list
No _ => Nothing
```
Construct a `Grid` from a non-empty `Vect` of non-empty `Vect`s. To keep the
function simple, we require that both the row and column dimension are known to
be non-zero before calling this constructor.
```idris
export
fromVect : Vect (S rows) (Vect (S cols) e) -> Grid rows cols e
fromVect xs = MkGrid . fromVect . map fromVect $ xs
```
Construct `Grid` containing the coordinate of the location in each location
```idris
export
coordinateGrid : {rows, cols : Nat} -> Grid rows cols (Coord rows cols)
coordinateGrid =
let row = fromVect $ allFins (S cols)
grid = zip (fromVect $ allFins (S rows)) (replicate _ row)
grid = map (\(x, xs) => map (x,) xs) grid
in MkGrid grid
```
### Accessors and Mutators
Get the value at a specific index in the grid
```idris
export
index : Coord rows cols -> Grid rows cols e -> e
index (row, col) grid =
index' (index' grid.grid row) col
```
Replace the value at a specific index in the grid
```idris
export
replaceAt : Coord rows cols -> e -> Grid rows cols e -> Grid rows cols e
replaceAt (row, col) x (MkGrid grid) =
let r = index' grid row
r = update (finToNat col) x r @{elemSmallerThanBound col}
grid = update (finToNat row) r grid @{elemSmallerThanBound row}
in MkGrid grid
```
Update the value at a specific index in the grid
```idris
export
updateAt : Coord rows cols -> (e -> e) -> Grid rows cols e -> Grid rows cols e
updateAt (row, col) f (MkGrid grid) =
let r = index' grid row
r = adjust f (finToNat col) r @{elemSmallerThanBound col}
grid = update (finToNat row) r grid @{elemSmallerThanBound row}
in MkGrid grid
```
Lazily provide all the values in the grid as a flat collection
```idris
export
flat : {rows, cols : Nat} -> Grid rows cols e -> LazyList e
flat (MkGrid grid) =
let grid = seqToLazy . map (seqToLazy {n = S cols}) $ grid
grid = grid []
in foldrLazy (\a, acc => a acc) [] grid
where
seqToLazy : {n : Nat} -> (seq : Seq n a) -> (rest : LazyList a) -> LazyList a
seqToLazy {n = 0} seq rest = rest
seqToLazy {n = (S k)} seq rest =
let (head, tail) = viewl seq
in head :: seqToLazy tail rest
```
### Interface Implementations
#### Show
```idris
export
{rows, cols : Nat} -> Show e => Show (Grid rows cols e) where
show (MkGrid grid) =
show . toVect . map toVect $ grid
```
#### Eq/Ord
```idris
export
Eq e => Eq (Grid rows cols e) where
(MkGrid grid_x) == (MkGrid grid_y) = grid_x == grid_y
export
Ord e => Ord (Grid rows cols e) where
compare (MkGrid grid_x) (MkGrid grid_y) = compare grid_x grid_y
```
#### Functor
```idris
export
Functor (Grid rows cols) where
map f (MkGrid grid) =
MkGrid . map (map f) $ grid
```
#### Foldable
Cheeze it a little and use our `flat` function internally here.
Also, `null` can statically return false, as `Grid` is structurally non-empty
```idris
export
{rows, cols : Nat} -> Foldable (Grid rows cols) where
foldr f acc grid = foldr f acc (flat grid)
foldl f acc grid = foldl f acc (flat grid)
null _ = False
toList grid = toList (flat grid)
```
#### Applicative
```idris
export
{rows, cols : Nat} -> Applicative (Grid rows cols) where
pure a = replicate a
(MkGrid f) <*> (MkGrid grid) =
MkGrid . map (\(a,b) => a <*> b) . zip f $ grid
```
#### Traversable
```idris
export
{rows, cols : Nat} -> Traversable (Grid rows cols) where
traverse f (MkGrid grid) =
map MkGrid . traverse (traverse f) $ grid
```
#### Zippable
```idris
export
Zippable (Grid rows cols) where
zipWith f (MkGrid grid_x) (MkGrid grid_y) =
let xs = zip grid_x grid_y
in MkGrid . map (\(a,b) => zipWith f a b) $ xs
unzipWith f (MkGrid grid) =
let (xs, ys) = unzip . map (unzipWith f) $ grid
in (MkGrid xs, MkGrid ys)
zipWith3 f (MkGrid as) (MkGrid bs) (MkGrid cs) =
let xs = zip3 as bs cs
in MkGrid . map (\(a, b, c) => zipWith3 f a b c) $ xs
unzipWith3 f (MkGrid grid) =
let (a, b, c) = unzip3 . map (unzipWith3 f) $ grid
in (MkGrid a, MkGrid b, MkGrid c)
```
### Extra
Extensions of the above functionality
#### Indexing
Convert this grid to one with both the index of the location and the element in
each location
```idris
export
indexed : {rows, cols : Nat} -> Grid rows cols e -> Grid rows cols (Coord rows cols, e)
indexed grid = zip coordinateGrid grid
```
Same as `flat` above, but indexed
```idris
export
flatIndexed : {rows, cols : Nat} -> Grid rows cols e -> LazyList (Coord rows cols, e)
flatIndexed = flat . indexed
```
#### String functionality
Attempts to convert a string, with newline delimited rows, to a grid of
characters
```idris
export
stringToGrid : String -> Maybe (rows : Nat ** cols : Nat ** Grid rows cols Char)
stringToGrid = fromFoldable . map (unpack . trim) . lines . trim
```
Converts a grid of chars to a string, delimiting the rows with newlines
```idris
export
gridToString : Grid rows cols Char -> String
gridToString (MkGrid grid) = unlines . toList . map (pack . toList) $ grid
```
#### Conversion
Convert a grid to a vect of vects
```idris
export
toVects : {rows, cols : Nat} -> Grid rows cols e -> Vect (S rows) (Vect (S cols) e)
toVects (MkGrid grid) = toVect . map toVect $ grid
```
Convert a grid to a list of lists
```idris
export
toLists : Grid rows cols e -> List (List e)
toLists (MkGrid grid) = toList . map toList $ grid
```

12
src/Main.md
View file

@ -76,7 +76,7 @@ data Error : Type where
A `Show` implementation for `Error` is provided, hidden in this document for A `Show` implementation for `Error` is provided, hidden in this document for
brevity. brevity.
```idris hide <!-- idris
Show Error where Show Error where
show (OptionsError errs) = show (OptionsError errs) =
let errs = unlines . map (" " ++) . lines . joinBy "\n" $ errs let errs = unlines . map (" " ++) . lines . joinBy "\n" $ errs
@ -98,7 +98,7 @@ Show Error where
show (SolveError year day part err) = show (SolveError year day part err) =
let err = unlines . map (" " ++) . lines . show $ err let err = unlines . map (" " ++) . lines . show $ err
in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
``` -->
## Extract the year and day ## Extract the year and day
@ -181,8 +181,8 @@ failures doing so.
## Handling the arguments and finding the input ## Handling the arguments and finding the input
Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise
blackhole the logs. Afterwards, use `logHandler` to introduce the `Logger` into blackhole the logs. Afterwards, use `logHandler` to introduce the logging
the effects list. `Writer` into the effects list.
```idris ```idris
-- If the verbose flag is set, hook up the logging writer to stderr -- If the verbose flag is set, hook up the logging writer to stderr
@ -259,8 +259,8 @@ a `SolveError`, then print out the result, then return, closing out the program.
### Lower logging into the IO component of the effect ### Lower logging into the IO component of the effect
Makes use of `Logger`'s `handleLoggerIO` function to "lower" logging actions This function uses the provided `String -> IO ()` to remove the `Writer` from
into `IO` within the effect. the effects list by translating `tell` calls to IO actions within the effect.
```idris ```idris
-- Lowers logging into IO within the effect using the given IO function -- Lowers logging into IO within the effect using the given IO function

8
src/Parser.md
View file

@ -1,8 +0,0 @@
# Parsing Utilties
```idris
module Parser
import public Parser.Interface as Parser
import public Parser.ParserState as Parser
```

333
src/Parser/Interface.md
View file

@ -1,333 +0,0 @@
# The interface of a `Parser`
```idris
module Parser.Interface
import public Data.List1
import public Parser.ParserState
import public Control.Eff
export infixr 4 >|
export infixr 5 >&
```
## Parser Errors
Combine the parser state at time of error with an error message.
```idris
public export
data ParseError : Type where
-- TODO: Rename this constructor
MkParseError : (state : ParserInternal Id) -> (message : String) -> ParseError
BeforeParse : (message : String) -> ParseError
NestedErrors : (state : ParserInternal Id) -> (message : String)
-> (rest : List ParseError) -> ParseError
```
```idris hide
export
Show ParseError where
show (MkParseError state message) =
let (line, col) = positionPair state
(line, col) = (show line, show col)
position = show state.position.index
in "Error at line \{line}, column \{col} (\{position}): \{message}"
show (BeforeParse message) =
"Error before parsing: \{message}"
show (NestedErrors state message rest) =
let rest = assert_total $joinBy "\n" . map ((" " ++) . show) $ rest
(line, col) = positionPair state
(line, col) = (show line, show col)
position = show state.position.index
first = "Error at line \{line}, column \{col} (\{position}): \{message}"
in "\{first}\n\{rest}"
```
## Type Alias
```idris
public export
Parser : Type -> Type
Parser a = Eff [ParserState, Except ParseError] a
```
## Error Generation
Provide a few effectful actions to generate an error from an error message, and
either return it or throw it.
```idris
export
parseError : Has ParserState fs => (message : String) -> Eff fs ParseError
parseError message = do
state <- save
pure $ MkParseError state message
export
throwParseError : Has ParserState fs => Has (Except ParseError) fs =>
(message : String) -> Eff fs a
throwParseError message = do
err <- parseError message
throw err
export
guardMaybe : Has ParserState fs => Has (Except ParseError) fs =>
(message : String) -> Eff fs (Maybe a) -> Eff fs a
guardMaybe message x = do
Just x <- x
| _ => throwParseError message
pure x
export
replaceError : (message : String) -> Parser (a -> Parser b)
replaceError message = do
state <- save
pure (\_ => throw $ MkParseError state message)
```
## Running a parser
We will use the phrasing "rundown" to refer to running all the effects in the
parser effect stack except `ParserState`, which is left in the effect stack to
facilitate handling in the context of another monad or effect stack, since it
benefits from mutability.
Rundown a parser, accepting the first returning parse, which may be failing or
succeding, and automatically generating a "no valid parses" message in the event
no paths in the `Choice` effect produce a returning parse.
```idris
export
rundownFirst : (f : Parser a) -> Eff [ParserState] (Either ParseError a)
rundownFirst f =
runExcept f
```
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 str = do
Just state <- newInternalIO str
| _ => pure . Left $ BeforeParse "Empty input"
runEff (rundownFirst f) [handleParserStateIO state]
export
runFirstIODebug : (f : Parser a) -> String -> IO (Either ParseError a)
runFirstIODebug f str = do
Just state <- newInternalIO str
| _ => pure . Left $ BeforeParse "Empty input"
runEff (rundownFirst f) [handleParserStateIODebug state]
export
runFirst : (f : Parser a) -> String -> Eff fs (Either ParseError a)
runFirst f str = do
Just state <- pure $ newInternal str
| _ => pure . Left $ BeforeParse "Empty input"
(result, _) <- lift . runParserState state . rundownFirst $ f
pure result
export
runFirst' : (f : Parser a) -> String -> Either ParseError a
runFirst' f str = extract $ runFirst f str {fs = []}
```
## Utility functionality
### Parser combinators
Try to run a computation in the context of the `Parser` effect stack, if it
fails (via `Except`), reset the state and resort to the supplied callback
Also supply a version specialized to ignore the error value, returning `Just a`
if the parse succeeds, and `Nothing` if it fails.
```idris
export
try : (f : Parser a) -> (err : ParseError -> Parser a) -> Parser a
try f err = do
starting_state <- save
result <- lift . runExcept $ f
case result of
Left error => do
load starting_state
err error
Right result => pure result
export
tryMaybe : (f : Parser a) -> Parser (Maybe a)
tryMaybe f = try (map Just f) (\_ => pure Nothing)
export
tryEither : (f : Parser a) -> Parser (Either ParseError a)
tryEither f = try (map Right f) (pure . Left)
```
Attempt to parse one of the given input parsers, in the provided order, invoking
the provided error action on failure.
The state will not be modified when an input parser fails
```idris
export
oneOfE : (err : String) -> List (Parser a) -> Parser a
oneOfE err xs = do
start <- save
oneOfE' err start [] xs
where
oneOfE' : (err : String) -> (start : ParserInternal Id)
-> (errs : List ParseError) -> List (Parser a) -> Parser a
oneOfE' err start errs [] = do
throw $ NestedErrors start err (reverse errs)
oneOfE' err start errs (x :: xs) = do
x <- tryEither x
case x of
Right val => pure val
Left error => oneOfE' err start (error :: errs) xs
```
Attempt to parse 0+ of an item
```idris
export
many : (f : Parser a) -> Parser (List a)
many f = do
Just next <- tryMaybe f
| _ => pure []
map (next ::) $ many f
```
Attempt to parse 1+ of an item, invoking the supplied error action on failure
```idris
export
atLeastOne : (err : ParseError -> Parser (List1 a)) -> (f : Parser a)
-> Parser (List1 a)
atLeastOne err f = do
Right next <- tryEither f
| Left e => err e
map (next :::) $ many f
```
Lift a parser producing a `List` or `List1` of `Char` into a parser producing a
`String`
```idris
-- TODO: Rename these
export
liftString : Parser (List Char) -> Parser String
liftString x = do
xs <- x
pure $ pack xs
export
liftString' : Parser (List1 Char) -> Parser String
liftString' x = liftString $ map forget x
```
Attempt to parse a specified character
```idris
export
charExact : Char -> Parser Char
charExact c = do
result <- charExact' c
case result of
GotChar char => pure char
GotError err => throwParseError "Got \{show err} Expected \{show c}"
EndOfInput => throwParseError "End of input"
```
Attempt to parse one of a list of chars
```idris
export
theseChars : List Char -> Parser Char
theseChars cs = do
pnote "Parsing one of: \{show cs}"
result <- charPredicate (\x => any (== x) cs)
case result of
GotChar char => pure char
GotError err => throwParseError "Got \{show err} Expected one of \{show cs}"
EndOfInput => throwParseError "End of input"
```
Attempt to parse an exact string
```idris
export
exactString : String -> Parser String
exactString str with (asList str)
exactString "" | [] = do
pnote "Parsing the empty string"
pure ""
exactString input@(strCons c str) | (c :: x) = do
pnote "Parsing exact string \{show input}"
GotChar next <- charPredicate (== c)
| GotError err => throwParseError "Got \{show err} expected \{show c}"
| EndOfInput => throwParseError "End of input"
rest <- exactString str | x
pure input
```
Wrap a parser in delimiter characters, discarding the value of the delimiters
```idris
export
delimited : (before, after : Char) -> Parser a -> Parser a
delimited before after x = do
pnote "Parsing delimited by \{show before} \{show after}"
starting_state <- save
_ <- charExact before
Right val <- tryEither x
| Left err => do
load starting_state
throw err
Just _ <- tryMaybe $ charExact after
| _ => do
load starting_state
throw $ MkParseError starting_state "Unmatched delimiter \{show before}"
pure val
```
Consume any number of characters of the provided character class and discard the
result. Also a version for doing so on both sides of a provided parser
```idris
export
nom : Parser Char -> Parser ()
nom x = do
pnote "Nomming"
_ <- many x
pure ()
export
surround : (around : Parser Char) -> (item : Parser a) -> Parser a
surround around item = do
pnote "Surrounding"
nom around
val <- item
nom around
pure val
```
### Composition of boolean functions
```idris
||| Return true if both of the predicates evaluate to true
public export
(>&) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool)
(>&) a b x = a x && b x
```
```idris
||| Return true if either of the predicates evaulates to true
public export
(>|) : (a : e -> Bool) -> (b : e -> Bool) -> (e -> Bool)
(>|) a b x = a x || b x
```

380
src/Parser/JSON.md
View file

@ -1,380 +0,0 @@
# JSON Parser
```idris
module Parser.JSON
import public Parser
import public Parser.Numbers
import Control.Monad.Eval
import Structures.Dependent.DList
```
```idris hide
import System
import Derive.Prelude
import Generics.Derive
%hide Generics.Derive.Eq
%hide Generics.Derive.Ord
%hide Generics.Derive.Show
%language ElabReflection
```
## JSON components
Types a JSON value is allowed to have
```idris
public export
data JSONType : Type where
TObject : JSONType
TArray : JSONType
TString : JSONType
TNumber : JSONType
TBool : JSONType
TNull : JSONType
%runElab derive "JSONType" [Generic, Meta, Eq, Ord, Show, DecEq]
%name JSONType type, type2, type3
```
A JSON value indexed by its type
```idris
public export
data JSONValue : JSONType -> Type where
VObject : {types : List JSONType}
-> DList JSONType (\t => (String, JSONValue t)) types -> JSONValue TObject
VArray : {types : List JSONType}
-> DList JSONType JSONValue types -> JSONValue TArray
VString : (s : String) -> JSONValue TString
VNumber : (d : Double) -> JSONValue TNumber
VBool : (b : Bool) -> JSONValue TBool
VNull : JSONValue TNull
%name JSONValue value, value2, value3
```
```idris hide
export
Show (JSONValue t) where
show (VObject xs) =
let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs
in assert_total $ "{\{joinBy "," xs}}"
show (VArray xs) =
let xs = dMap (\_,e => show e) xs
in assert_total $ "[\{joinBy "," xs}]"
show (VString s) = "\"\{s}\""
show (VNumber d) = show d
show (VBool False) = "false"
show (VBool True) = "true"
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
(VArray xs) == (VArray ys) =
assert_total $ xs $== ys
(VString s) == (VString str) = s == str
(VNumber d) == (VNumber dbl) = d == dbl
(VBool b) == (VBool x) = b == x
VNull == VNull = True
%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,
we will use the more modern style of declaring all our types ahead of our
definitions.
```idris
export
object : Parser (JSONValue TObject)
export
array : Parser (JSONValue TArray)
export
string : Parser (JSONValue TString)
export
number : Parser (JSONValue TNumber)
export
bool : Parser (JSONValue TBool)
export
null : Parser (JSONValue TNull)
```
Define a `whitespace` character class based on the json specifications
```idris
whitespace : Parser Char
whitespace = do
pnote "Whitespace character"
theseChars [' ', '\n', '\r', '\t']
```
Convenience function
```idris
dpairize : {t : JSONType} ->
Parser (JSONValue t) -> Parser (t' : JSONType ** JSONValue t')
dpairize x = do
x <- x
pure (_ ** x)
```
Top level json value parser
```idris
export
value : Parser (t : JSONType ** JSONValue t)
value = do
pnote "JSON Value"
surround whitespace $ oneOfE
"Expected JSON Value"
[
dpairize object
, dpairize array
, dpairize string
, dpairize number
, dpairize bool
, dpairize null
]
```
Now go through our json value types
```idris
object = do
pnote "JSON Object"
oneOfE
"Expected Object"
[emptyObject, occupiedObject]
where
emptyObject : Parser (JSONValue TObject)
emptyObject = do
delimited '{' '}' (nom whitespace)
pure $ VObject Nil
keyValue : Parser (t : JSONType ** (String, JSONValue t))
keyValue = do
VString key <- surround whitespace string
_ <- charExact ':'
(typ ** val) <- value
pure (typ ** (key, val))
restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
restKeyValue = do
_ <- charExact ','
keyValue
pairs : Parser (List1 (t : JSONType ** (String, JSONValue t)))
pairs = do
first <- keyValue
rest <- many restKeyValue
-- TODO: headTail combinator for this
pure $ first ::: rest
occupiedObject : Parser (JSONValue TObject)
occupiedObject = do
val <- delimited '{' '}' pairs
let (types ** xs) = DList.fromList (forget val)
pure $ VObject xs
```
```idris
array = do
pnote "JSON Array"
oneOfE
"Expected Array"
[emptyArray, occupiedArray]
where
emptyArray : Parser (JSONValue TArray)
emptyArray = do
delimited '[' ']' (nom whitespace)
pure $ VArray Nil
restValue : Parser (t : JSONType ** JSONValue t)
restValue = do
_ <- charExact ','
value
values : Parser (List1 (t : JSONType ** JSONValue t))
values = do
first <- value
rest <- many restValue
pure $ first ::: rest
occupiedArray : Parser (JSONValue TArray)
occupiedArray = do
xs <- delimited '[' ']' values
let (types ** xs) = DList.fromList (forget xs)
pure $ VArray xs
```
```idris
string = do
pnote "JSON String"
str <- liftString $ delimited '"' '"' (many stringCharacter)
pure $ VString str
where
-- TODO: Handle control characters properly
stringCharacter : Parser Char
stringCharacter = do
result <- charPredicate (not . (== '"'))
case result of
GotChar char => pure char
GotError err =>
throwParseError "Expected string character, got \{show err}"
EndOfInput => throwParseError "Unexpected end of input"
```
```idris
number = do
pnote "JSON Number"
d <- double
pure $ VNumber d
```
```idris
bool = do
pnote "JSON Bool"
oneOfE
"Expected Bool"
[true, false]
where
true : Parser (JSONValue TBool)
true = do
_ <- exactString "true"
pure $ VBool True
false : Parser (JSONValue TBool)
false = do
_ <- exactString "false"
pure $ VBool False
```
```idris
null = do
pnote "JSON null"
_ <- exactString "null"
pure VNull
```
## Unit tests
Quick smoke test
```idris
-- @@test JSON Quick Smoke
quickSmoke : IO Bool
quickSmoke = do
let input = "{\"string\":\"string\",\"number\":5,\"true\":true,\"false\":false,\"null\":null,\"array\":[1,2,3]}"
putStrLn input
Right (type ** parsed) <- runFirstIODebug value input
| Left err => do
printLn err
pure False
putStrLn "Input: \{input}\nOutput: \{show type} -> \{show parsed}"
let reference_object =
VObject [
("string", VString "string")
, ("number", VNumber 5.0)
, ("true", VBool True)
, ("false", VBool False)
, ("null", VNull)
, ("array", VArray [
VNumber 1.0
, VNumber 2.0
, VNumber 3.0
])
]
case type of
TObject => pure $ parsed == reference_object
_ => pure False
```

257
src/Parser/Numbers.md
View file

@ -1,257 +0,0 @@
# Numerical Parsers
```idris
module Parser.Numbers
import public Parser
import Data.Vect
import Control.Eff
```
```idris hide
import System
```
## Base Abstraction
```idris
public export
record Base where
constructor MkBase
base : Nat
digits : Vect base Char
%name Base b
export
hasDigit : Base -> Char -> Bool
hasDigit (MkBase base digits) c = any (== c) digits
export
digitValue : Base -> Char -> Maybe Nat
digitValue (MkBase base digits) c = digitValue' digits 0
where
digitValue' : Vect n Char -> (idx : Nat) -> Maybe Nat
digitValue' [] idx = Nothing
digitValue' (x :: xs) idx =
if x == c
then Just idx
else digitValue' xs (S idx)
public export
base10 : Base
base10 = MkBase 10
['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']
public export
hex : Base
hex = MkBase 16
['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f']
```
## Parsers
### Nat
```idris
export
nat : Base -> Parser Nat
nat b = do
error <- replaceError "Expected digit"
(first ::: rest) <- atLeastOne error parseDigit
pure $ foldl (\acc, e => 10 * acc + e) first rest
where
parseDigit : Parser Nat
parseDigit = do
GotChar char <- charPredicate (hasDigit b)
| GotError e => throwParseError "\{show e} is not a digit"
| EndOfInput => throwParseError "End Of Input"
case digitValue b char of
Nothing =>
throwParseError "Failed to parse as base \{show b.base}: \{show char}"
Just x => pure x
export
natBase10 : Parser Nat
natBase10 = nat base10
```
### Integer
```idris
export
integer : Base -> Parser Integer
integer b = do
negative <- map isJust . tryMaybe $ charExact '-'
value <- map natToInteger $ nat b
if negative
then pure $ negate value
else pure $ value
export
integerBase10 : Parser Integer
integerBase10 = integer base10
```
### Double
```idris
-- TODO: Replicate `parseDouble` logic and make this base-generic
export
double : Parser Double
double = do
starting_state <- save
integer <- integer
fraction <- tryMaybe fraction
exponent <- tryMaybe exponent
let str = case (fraction, exponent) of
(Nothing, Nothing) =>
integer
(Nothing, (Just exponent)) =>
"\{integer}e\{exponent}"
((Just fraction), Nothing) =>
"\{integer}.\{fraction}"
((Just fraction), (Just exponent)) =>
"\{integer}.\{fraction}e\{exponent}"
Just out <- pure $ parseDouble str
| _ =>
throw $ MkParseError starting_state "Std failed to parse as double: \{str}"
pure out
where
parseDigit : Parser Char
parseDigit = do
GotChar char <- charPredicate (hasDigit base10)
| GotError e => throwParseError "\{show e} is not a digit"
| EndOfInput => throwParseError "End Of Input"
pure char
integer : Parser String
integer = do
sign <- tryMaybe $ charExact '-'
error <- replaceError "Expected digit"
digits <- map forget $ atLeastOne error parseDigit
case sign of
Nothing => pure $ pack digits
Just x => pure $ pack (x :: digits)
fraction : Parser String
fraction = do
decimal <- charExact '.'
error <- replaceError "Expected digit"
digits <- map forget $ atLeastOne error parseDigit
pure $ pack digits
exponent : Parser String
exponent = do
e <- theseChars ['e', 'E']
sign <- theseChars ['+', '-']
error <- replaceError "Expected digit"
digits <- map forget $ atLeastOne error parseDigit
pure . pack $ sign :: digits
```
## Unit tests
Test roundtripping a value through the provided parser
```idris
roundtrip : Eq a => Show a => a -> (p : Parser a) -> IO Bool
roundtrip x p = do
let string = show x
putStrLn "Roundtripping \{string}"
Just state <- newInternalIO string
| _ => do
putStrLn "Failed to produce parser for \{string}"
pure False
Right result <- runEff (rundownFirst p) [handleParserStateIO state] {m = IO}
| Left err => do
printLn err
pure False
putStrLn "Input: \{string} Output: \{show result}"
pure $ x == result
```
Do some roundtrip tests with the nat parser
```idris
-- @@test Nat round trip
natRoundTrip : IO Bool
natRoundTrip = pure $
!(roundtrip 0 natBase10)
&& !(roundtrip 1 natBase10)
&& !(roundtrip 100 natBase10)
&& !(roundtrip 1234 natBase10)
&& !(roundtrip 1234567890 natBase10)
&& !(roundtrip 1234567890000 natBase10)
&& !(roundtrip 12345678901234567890 natBase10)
```
```idris
-- @@test Integer round trip
integerRoundTrip : IO Bool
integerRoundTrip = pure $
!(roundtrip 0 integerBase10)
&& !(roundtrip 1 integerBase10)
&& !(roundtrip 100 integerBase10)
&& !(roundtrip 1234 integerBase10)
&& !(roundtrip 1234567890 integerBase10)
&& !(roundtrip 1234567890000 integerBase10)
&& !(roundtrip 12345678901234567890 integerBase10)
&& !(roundtrip (-1) integerBase10)
&& !(roundtrip (-100) integerBase10)
&& !(roundtrip (-1234) integerBase10)
&& !(roundtrip (-1234567890) integerBase10)
&& !(roundtrip (-1234567890000) integerBase10)
&& !(roundtrip (-12345678901234567890) integerBase10)
```
Compare our parsing of a double to the standard library's
```idris
compareDouble : String -> IO Bool
compareDouble string = do
Just state <- newInternalIO string
| _ => do
putStrLn "Failed to produce parser for \{string}"
pure False
Right result <-
runEff (rundownFirst double) [handleParserStateIO state] {m = IO}
| Left err => do
printLn err
pure False
putStrLn "Input: \{string} Output: \{show result}"
Just double' <- pure $ parseDouble string
| _ => do
printLn "Std failed to parse as double: \{string}"
pure False
pure $ result == double'
```
```idris
-- @@test Double Std Comparison
doubleRoundTrip : IO Bool
doubleRoundTrip = pure $
!(compareDouble "0")
&& !(compareDouble "1")
&& !(compareDouble "100")
&& !(compareDouble "1234")
&& !(compareDouble "1234567890")
&& !(compareDouble "1234567890000")
&& !(compareDouble "12345678901234567890")
&& !(compareDouble "-1")
&& !(compareDouble "-100")
&& !(compareDouble "-1234")
&& !(compareDouble "-1234567890")
&& !(compareDouble "-1234567890000")
&& !(compareDouble "-12345678901234567890")
&& !(compareDouble "0.0")
&& !(compareDouble "1.0")
&& !(compareDouble "-1.0")
&& !(compareDouble "-0.0")
&& !(compareDouble "-0.0")
&& !(compareDouble "0.1234")
&& !(compareDouble "0.01234")
&& !(compareDouble "-0.1234")
&& !(compareDouble "-0.01234")
&& !(compareDouble "1.234e+5")
&& !(compareDouble "1.234e-5")
&& !(compareDouble "-1.234e+5")
&& !(compareDouble "-1.234e-5")
```

369
src/Parser/ParserState.md
View file

@ -1,369 +0,0 @@
# Parser State
An effectful description of the text a parser consumes
```idris
module Parser.ParserState
import public Data.String
import public Data.DPair
import public Data.Refined
import public Data.Refined.Int64
import public Data.SortedMap
import public Data.IORef
import Data.Primitives.Interpolation
import System.File
import public Control.Eff
```
## Barbie Basics
Barbies are types that can "change their clothes", in Idris, this manifests as a
type indexed by a type-level function that affects the types of the fields.
Since we know our usage here is going to be quite simple, and not even really
making use of dependently typed fun, we are going to implement all the barbie
functionality we need by hand, but if you feel like barbies might be a good fit
for your problem, or you simply want to learn more, please check out a library
like `barbies`[^1]
```idris
public export
Id : Type -> Type
Id x = x
```
## Internal State of a Parser
Type alias for our refined `Int64`s
```idris
public export
0 IsIndex : (length : Int64) -> Int64 -> Type
IsIndex length = From 0 && LessThan length
public export
record Index (length : Int64) where
constructor MkIndex
index : Int64
{auto 0 prf : IsIndex length index}
```
```idris hide
export
Eq (Index i) where
x == y = x.index == y.index
export
Ord (Index i) where
compare x y = compare x.index y.index
export
Show (Index i) where
show (MkIndex index) = show index
```
Stores the location we are currently at in the string, and metadata about it for
providing good error messages. Parsing an empty input isn't very interesting, so
we exclude inputs of length zero, since that will make other things easier.
```idris
||| State representing a parser's position in the text
public export
record ParserInternal (f : Type -> Type) where
constructor MkInternal
-- IDEA: Maybe go full barbie and have this be a field, so that we can, say,
-- read directly from a file instead of from an already loaded string using the
-- same parser
||| The input string
input : String
||| The length of the input string
length : Int64
{auto 0 len_prf : length = cast (strLength input)}
||| A sorted set containing the positions of the start of each line
line_starts : SortedMap (Index length) Nat
||| The position of the next character to read in the input
position : f (Index length)
||| True if we have hit the end of input
end_of_input : f Bool
%name ParserInternal pi, pj, pk
```
### ParserInternal Methods
Construct a `ParserInternal` from an input string. Will fail if the input is
empty, because then we can't index it.
```idris
export
newInternal : (input : String) -> Maybe (ParserInternal Id)
newInternal input =
-- Check if we have at least one character in the input
case refine0 0 {p = IsIndex (cast (strLength input))} of
Nothing => Nothing
Just (Element position _) => Just $
MkInternal input
(cast (strLength input))
(mkStarts' input (MkIndex position))
(MkIndex position)
False
where
partial
mkStarts :
(str : String) -> (acc : List (Index (cast (strLength str)), Nat))
-> (idx : Index (cast (strLength str))) -> (count : Nat) -> (next : Bool)
-> List (Index (cast (strLength str)), Nat)
mkStarts str acc idx count True =
mkStarts str ((idx, count) :: acc) idx (S count) False
mkStarts str acc idx count False =
case refine0 (idx.index + 1) {p = IsIndex (cast (strLength str))} of
Nothing => acc
Just (Element next _) =>
if strIndex str (cast idx.index) == '\n'
then mkStarts str acc (MkIndex next) count True
else mkStarts str acc (MkIndex next) count False
mkStarts' : (str : String) -> (start : Index (cast (strLength str)))
-> SortedMap (Index (cast (strLength str))) Nat
mkStarts' str start =
let
pairs = assert_total $
mkStarts str [] start 0 True
in fromList pairs
```
Get the current line and column number
```idris
||| Returns the current position of the parser cursor in, zero indexed, (line,
||| column) form
export
positionPair : (pi : ParserInternal Id) -> (Nat, Nat)
positionPair pi =
case lookup pi.position pi.line_starts of
Just line => (line, 0)
Nothing =>
case lookupBetween pi.position pi.line_starts of
-- There will always be at least one line start, and we would have hit
-- the previous case if we were at the start of the first one, so if
-- there isn't a before, we can return a nonsense value safely
(Nothing, _) => (0, 0)
(Just (start, linum), after) =>
-- Our index will always be after the start of the line, for previously
-- mentioned reasons, so this cast is safe
let col = cast {to = Nat} $ pi.position.index - start.index
in (linum, col)
```
```idris hide
export
Show (ParserInternal Id) where
show pi =
let (line, col) = positionPair pi
current = assert_total $ strIndex pi.input (cast pi.position.index)
pos = pi.position.index
eof = show pi.end_of_input
in "Position: \{pos}(\{line}, \{col}}) Value: \{show current} EoF: \{eof}"
```
### More Barbie Functionality
Provide the barbie analogs of `map` and `traverse` for our `ParserInternal`
type, allowing us to change the type the values in a `ParserInternal` by mapping
over those values.
```idris
export
bmap : ({0 a : Type} -> f a -> g a) -> ParserInternal f -> ParserInternal g
-- bmap f = bmap_ (\_ => f)
bmap fun (MkInternal input length line_starts position end_of_input) =
let position' = fun position
end_of_input' = fun end_of_input
in MkInternal input length line_starts position' end_of_input'
export
btraverse : Applicative e => ({0 a : Type} -> f a -> e (g a))
-> ParserInternal f -> e (ParserInternal g)
btraverse fun (MkInternal input length line_starts position end_of_input) =
let pures = (MkInternal input length line_starts)
in [| pures (fun position) (fun end_of_input)|]
```
## Three way result
```idris
||| Three way result returned from attempting to parse a single char
public export
data ParseCharResult : Type where
GotChar : (char : Char) -> ParseCharResult
GotError : (err : Char) -> ParseCharResult
EndOfInput : ParseCharResult
```
## The Effect Type
```idris
export
data ParserState : Type -> Type where
Save : ParserState (ParserInternal Id)
Load : (ParserInternal Id) -> ParserState ()
-- TODO: Maybe add a ParseString that parses a string of characters as a
-- string using efficent slicing?
ParseChar : (predicate : Char -> Bool) -> ParserState ParseCharResult
ParseExactChar : (char : Char) -> ParserState ParseCharResult
ParseEoF : ParserState Bool
Note : Lazy String -> ParserState ()
```
```idris hide
Show (ParserState t) where
show Save = "Saving state"
show (Load pi) = "Loading state \{show pi}"
show (ParseChar predicate) = "Parsing char"
show (ParseExactChar char) = "Parsing char \{show char}"
show ParseEoF = "Parsing EoF"
show (Note _) = "Note"
```
### Actions
```idris
||| Return the current state, for potential later reloading
export
save : Has ParserState fs => Eff fs (ParserInternal Id)
save = send Save
||| Reset to the provided state
export
load : Has ParserState fs => ParserInternal Id -> Eff fs ()
load pi = send $ Load pi
||| Attempt to parse a char, checking to see if it complies with the supplied
||| predicate, updates the state if parsing succeeds, does not alter it in an
||| error condition.
export
charPredicate : Has ParserState fs => (predicate : Char -> Bool)
-> Eff fs ParseCharResult
charPredicate predicate = send $ ParseChar predicate
||| Parse a char by exact value
export
charExact' : Has ParserState fs => (chr : Char) -> Eff fs ParseCharResult
charExact' chr = send $ ParseExactChar chr
||| "Parse" the end of input, returning `True` if the parser state is currently
||| at the end of the input
export
parseEoF : Has ParserState fs => Eff fs Bool
parseEoF = send ParseEoF
||| Make a note to be output when running with a debug handler
export
pnote : Has ParserState fs => Lazy String -> Eff fs ()
pnote x = send $ Note x
```
## Handling a ParserState
### IO Context
```idris
export
handleParserStateIO : HasIO io =>
IORef (ParserInternal IORef) -> ParserState t -> io t
handleParserStateIO pi Save = do
pi <- readIORef pi
btraverse readIORef pi
handleParserStateIO pi (Load pj) = do
pj <- btraverse newIORef pj
writeIORef pi pj
handleParserStateIO pi (ParseChar predicate) = do
pi <- readIORef pi
False <- readIORef pi.end_of_input
| _ => pure EndOfInput
position <- readIORef pi.position
let char = assert_total $ strIndex pi.input (cast position.index)
True <- pure $ predicate char
| _ => pure $ GotError char
-- Our refinement type on the position forces us to check that the length is
-- in bounds after incrementing it, if its out of bounds, set the end_of_input
-- flag
case refine0 (position.index + 1) {p = IsIndex pi.length} of
Nothing => do
writeIORef pi.end_of_input True
pure $ GotChar char
Just (Element next _) => do
writeIORef pi.position $ MkIndex next
pure $ GotChar char
handleParserStateIO pi (ParseExactChar chr) = do
-- TODO: do this directly?
handleParserStateIO pi (ParseChar (== chr))
handleParserStateIO pi ParseEoF = do
pi <- readIORef pi
readIORef pi.end_of_input
-- We ignore notes in non-debug mode
handleParserStateIO pi (Note _) = pure ()
export
newInternalIO : HasIO io => String -> io $ Maybe (IORef (ParserInternal IORef))
newInternalIO str = do
Just internal <- pure $ newInternal str
| _ => pure Nothing
internal <- btraverse newIORef internal
map Just $ newIORef internal
```
Wrapper with debugging output
```idris
export
handleParserStateIODebug : HasIO io =>
IORef (ParserInternal IORef) -> ParserState t -> io t
handleParserStateIODebug x (Note note) = do
state <- readIORef x
state <- btraverse readIORef state
_ <- fPutStrLn stderr "Note \{note} -> \{show state}"
pure ()
handleParserStateIODebug x y = do
state <- readIORef x
state <- btraverse readIORef state
_ <- fPutStrLn stderr "\{show y} -> \{show state}"
handleParserStateIO x y
```
### State context
```idris
unPS : ParserInternal Id -> ParserState a -> (a, ParserInternal Id)
unPS pi Save = (pi, pi)
unPS pi (Load pj) = ((), pi)
unPS pi (ParseChar predicate) =
if pi.end_of_input
then (EndOfInput, pi)
else let
char = assert_total $ strIndex pi.input (cast pi.position.index)
in if predicate char
then case refine0 (pi.position.index + 1) {p = IsIndex pi.length} of
Nothing =>
(GotChar char, {end_of_input := True} pi)
Just (Element next _) =>
(GotChar char, {position := MkIndex next} pi)
else (GotError char, pi)
unPS pi (ParseExactChar chr) = unPS pi (ParseChar (== chr))
unPS pi ParseEoF = (pi.end_of_input, pi)
unPS pi (Note _) = ((), pi)
export
runParserState : Has ParserState fs =>
(s : ParserInternal Id) -> Eff fs t
-> Eff (fs - ParserState) (t, ParserInternal Id)
runParserState s =
handleRelayS s (\x, y => pure (y, x)) $ \s2,ps,f =>
let (a, st) = unPS s2 ps
in f st a
```
## Footnotes
[^1]: <https://github.com/stefan-hoeck/idris2-barbies>

1
src/README.md
View file

@ -1 +0,0 @@
../README.md

69
src/Runner.md
View file

@ -22,15 +22,16 @@ import public Util.Eff
# Effectful Parts # Effectful Parts
The solution to each part of a day is run as an effectful computation, and as The solution to each part of a day is run as an effectful computation, and as
the effect stack is meant to be the same across both parts, only varying in the the available effects are meant to be the same across both parts, only varying
type of the error value for the `Except` effect, we construct a type level in the type of the error value in the `Except` effect, I construct a type level
function to have a single source of truth. The `err` type can be any type with a function to have a single source of truth for this. The `err` type can be any
`Show` implementation, but that constraint will be tacked on in the next step. type with a `Show` implementation, but that constraint will be tacked on in the
next step.
The `Logger` effect is provided for logging, and a `Reader` effect is provided A `Writer` effect is provided for logging, and a `Reader` effect is provided to
to pass in the input, to make the top level API a little bit cleaner. `IO` is pass in the input, just to make the top level API a little bit cleaner. `IO` is
also provided, even though the part solutions themselves shouldn't really be also provided, even though the part solutions themselves shouldn't really be
doing any IO, this will come in handy if a part needs `IO` for performance doing any IO, this may come in handy if a part needs `IO` for performance
reasons. reasons.
```idris ```idris
@ -45,19 +46,19 @@ PartEff err =
# The `Day` Record # The `Day` Record
The `Day` type groups together an effectful `part1` computation, an optional The `Day` type groups together an effectful `part1` computation, an optional
effectful `part2` computation, and the day number, with some type wrangling to effectful `part2` computation, the day number, and does some type wrangling to
get the type system out of our way. get the type system out of our way on this one.
`part1` and `part2` are allowed independent output and error types, and this `part1` and `part2` are allowed independent output and error types, and this
record captures `Show` implementations for those output and error types so that record captures `Show` implementations for those output and error types so that
we can display them in `Main`, where the `Day` is consumed, without having to we can display them in `Main` where the `Day` is consumed without having to
actually know what the types are. actually know what the types are.
It is often useful to pass a bit of context, such as the data structures It is often useful to pass a bit of context, such as the data structures
resulting from parsing, between `part1` and `part2`. This is achieved through resulting from parsing, between `part1` and `part2`, and this is achieved by the
the erased `ctx` type, which is totally opaque to the runner. The code in `Main` erased `ctx` type, which is totally opaque here. The runner code in `Main` will
will provide the value of the `ctx` type produced as part of the output of provide the value of the `ctx` type produced as part of the output of `part1` as
`part1` and as the input of `part2`. the input of `part2`.
```idris ```idris
||| Model solving a single day ||| Model solving a single day
@ -79,9 +80,9 @@ record Day where
The default `MkDay` constructor is slightly cumbersome to use, always requiring The default `MkDay` constructor is slightly cumbersome to use, always requiring
_something_ for the `part2` slot, even if there isn't a part 2 yet, and _something_ for the `part2` slot, even if there isn't a part 2 yet, and
requiring that `part2` be wrapped in a `Just` when there is one. We provide a requiring that `part2` be wrapped in a `Just` when there is one, so we provide a
pair of constructors for the case where there is only a `part1`, as well as one pair of constructors for the case where there is only a `part1` and for where
for when there is a `part1` and a `part2`. there is a `part1` and a `part2` that handle that for us.
```idris ```idris
namespace Day namespace Day
@ -90,7 +91,8 @@ namespace Day
### First ### First
The `First` constructor only accepts a `part1`, it does the work of filling in The `First` constructor only accepts a `part1`, it does the work of filling in
`part2` with `Nothing` and setting all of `part2`'s type arguments to `()`. `part2` with `Nothing` and setting all of `part2`'s type arguments to `()` for
us.'
```idris ```idris
||| Constructor for a day with only part one ready to run ||| Constructor for a day with only part one ready to run
@ -104,8 +106,8 @@ The `First` constructor only accepts a `part1`, it does the work of filling in
### Both ### Both
The `Both` constructor does less heavy lifting, the only thing it needs to do is The `Both` constructor does a little bit less heavy lifting, the only thing it
wrap `part2` in a `Just`. needs to do for us is wrap `part2` in a `Just`.
```idris ```idris
||| Constructor for a day with both parts ready to run ||| Constructor for a day with both parts ready to run
@ -121,17 +123,16 @@ wrap `part2` in a `Just`.
## Freshness ## Freshness
We will be using a _Fresh List_ from the We will be using a _Fresh List_ from the
[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build our [structures](https://git.sr.ht/~thatonelutenist/Structures) package to build
API defensively against duplicate days and cosmetically annoying out of order defensiveness into the API. A Fresh List structurally only allows you to prepend
day registration. A Fresh List structurally only allows you to prepend/cons an an element onto it when it satisfies some _freshness_ criteria relative to the
element onto it when it satisfies some _freshness criteria_ relative to the elements already in the list.
elements already contained in the list.
We compare the day numbers of the two `Day`s using the less-than(`<`) Here, we compare the day numbers of the two `Day`s using the less-than
relationship. Since we are operating on the start of the list when this relationship. Since we are operating on the start of the list when this
comparison takes place, this enforces, through type checking, that the resulting comparison takes place, this enforces, through type checking, that the resulting
Fresh List of `Day`s is sorted in ascending order and that no two `Day`s have Fresh List is sorted in ascending order and that no two `Day`s have the same day
the same day number. number.
```idris ```idris
||| Freshness criteria for days ||| Freshness criteria for days
@ -149,7 +150,7 @@ FreshDay x y = x.day < y.day
# The `Year` Record # The `Year` Record
The `Year` record collects a number of `Day`s into a single Fresh List for the The `Year` record collects a number of `Day`s into a single Fresh List for the
year, also containing the year number for this collection. year, and is mostly just a simple container.
```idris ```idris
||| Collect all the days in a given year ||| Collect all the days in a given year
@ -165,10 +166,9 @@ record Year where
Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored Much like `Day`s are stored in a `FreshList` in `Year`, `Year`s will be stored
in a `FreshList` in `Advent`, so we need to provide a freshness criteria for in a `FreshList` in `Advent`, so we need to provide a freshness criteria for
`Year` as well. `Year` as well. We do so by applying the less-than relationship against the year
number of the two `Years`, for the same reasons and with the same results as
We do so by applying the less-than relationship against the year number of the with `FreshDay`.
two `Years`, for the same reasons and with the same results as with `FreshDay`.
```idris ```idris
||| Freshness criteria for years ||| Freshness criteria for years
@ -186,7 +186,8 @@ FreshYear x y = x.year < y.year
# The `Advent` Record # The `Advent` Record
The `Advent` record collects a number of `Year`s in much the same way that The `Advent` record collects a number of `Year`s in much the same way that
`Year` collects a number of days. `Year` collects a number of days, sorting the `Year`s in a `FreshList` to
provide API defensiveness.
```idris ```idris
||| Collect all years ||| Collect all years

37
src/SUMMARY.md
View file

@ -1,37 +0,0 @@
# Summary
[README](README.md)
# Running the code
- [Runner - Divide Code Into Years and Days](Runner.md)
- [Main - Select a Day and Year to Run](Main.md)
# Utility Mini-Library
- [Util - Extend Standard Types](Util.md)
- [Util.Eff - Effects and Effect Accessories](Util/Eff.md)
- [Util.Digits - Pattern Matching Integers as Lists of Digits](Util/Eff.md)
- [Array - Arrays With Constant Time Indexing and Slicing](Array.md)
- [Parser - Recursive Descent Parsing, With Effects](Parser.md)
- [Interface - Core Parsing Functionality](Parser/Interface.md)
- [ParserState - Custom Effect for Parser Internal State](Parser/ParserState.md)
- [Numbers - Parsers for Numerical Values](Parser/Numbers.md)
- [JSON - A JSON Parser](Parser/JSON.md)
# Problems
- [2015](Years/Y2015.md)
- [Day 1 - Warmup](Years/Y2015/Day1.md)
- [Day 2 - Early Effectful Parsing](Years/Y2015/Day2.md)
- [Day 3 - Mutually Recursive Functions](Years/Y2015/Day3.md)
- [Day 4 - Basic FFI](Years/Y2015/Day4.md)
- [Day 5 - Views and Dependent Pattern Matching](Years/Y2015/Day5.md)
- [Day 6 - Naive 2D Grid](Years/Y2015/Day6.md)
- [Day 7 - Dependent Maps and Indexed Type Familes](Years/Y2015/Day7.md)
- [Day 8 - Proper Effectful Parsers](Years/Y2015/Day8.md)
- [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)

239
src/Util.md
View file

@ -9,69 +9,15 @@ module Util
import Data.SortedSet import Data.SortedSet
import Data.String import Data.String
import Data.List.Lazy import Data.List.Lazy
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
### repeatN
Recursively applies `f` to `seed` N times
```idris
export
repeatN : (times : Nat) -> (f : a -> a) -> (seed : a) -> a
repeatN 0 f seed = seed
repeatN (S times') f seed = repeatN times' f (f seed)
```
## Either ## Either
```idris hide <!-- idris
namespace Either namespace Either
``` -->
### mapLeft ### mapLeft
@ -85,139 +31,18 @@ Applies a function to the contents of a `Left` if the value of the given
mapLeft f (Right x) = Right x mapLeft f (Right x) = Right x
``` ```
## List
```idris hide
namespace List
```
### contains
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
```
### rotations
Provides all the 'rotations' of a list.
Example:
```
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
```
## 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
### Addition and Subtraction ### Addition and Subtraction
```idris hide <!-- idris
export infixl 8 >+< export infixl 8 >+<
export infixl 8 >-< export infixl 8 >-<
namespace Pair namespace Pair
``` -->
```idris ```idris
public export public export
@ -233,9 +58,9 @@ namespace Pair
Extend `Data.SortedSet` Extend `Data.SortedSet`
```idris hide <!-- idris
namespace Set namespace Set
``` -->
### length ### length
@ -251,9 +76,9 @@ Count the number of elements in a sorted set
Extend `Data.String` Extend `Data.String`
```idris hide <!-- idris
namespace String namespace String
``` -->
### isSubstr ### isSubstr
@ -284,10 +109,6 @@ 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
@ -303,47 +124,3 @@ Lazily take the cartesian product of two foldables
combine x [] rest = rest combine x [] rest = rest
combine x (y :: ys) rest = (x, y) :: combine x ys rest combine x (y :: ys) rest = (x, y) :: combine x ys rest
``` ```
### Concat
Lazily concatenate a LazyList of LazyLists
```idris
export
lazyConcat : LazyList (LazyList a) -> LazyList a
lazyConcat [] = []
lazyConcat (x :: xs) = x ++ lazyConcat xs
```
### Group
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
```

192
src/Util/Digits.md
View file

@ -1,192 +0,0 @@
# Viewing Integers as lists of digits
```idris
module Util.Digits
import Data.Monoid.Exponentiation
```
```idris hide
import System
%default total
```
This module provides views and associated functionality for treating `Integers`
as if they were lists of numbers.
Since `Integer` is a primitive type, that Idris can't directly reason about the
structure of, we need to use some `believe_me`s, a hideously unsafe operation
that completely bypasses the type checker, somewhere along the line. For
teaching purposes, we'll do it here, but please consider a library like
[prim](https://github.com/stefan-hoeck/idris2-prim) if you find yourself needing
to prove properties about primitive types.
```idris hide
-- This mutual block isn't strictly required, but is useful for literate purposes
mutual
```
## Primitive functionality
Take the integer log base 10 of an `Integer`
```idris
log10 : Integer -> Nat
log10 i = assert_total $ log10' i 0
where
covering
log10' : Integer -> (acc : Nat) -> Nat
log10' i acc =
if i > 0
then log10' (i `div` 10) (S acc)
else acc
```
## Ascending Order
View an integer as a list of digits, ordered from least significant digit to
most significant digit.
For a clarifying example:
```idris hide
-- @@test Ascending Digits Example
ascendingExample : IO Bool
ascendingExample = do
putStrLn "Expecting: \{show [5, 4, 3, 2, 1]}"
putStrLn "Got: \{show . ascList $ ascending 12345}"
pure $
```
```idris
ascList (ascending 12345) == [5, 4, 3, 2, 1]
```
The view itself, storing the current digit, and the rest of the number, both as
a raw integer and by a recursive `Ascending`. Acts as a proof that the number
can be reproduced by multiplying the rest by 10 and then adding the current
digit.
```idris
||| A view of an integer as a list of digits in order of ascending signifigance
public export
data Ascending : Integer -> Type where
||| Indicates that the number was negative
NegAsc : (rec : Lazy (Ascending (negate i))) -> Ascending i
||| Indicates we have already seen all the digits of a number
End : Ascending 0
||| A digit and all the preceeding ones
Next : (digit : Integer)
-> (rest : Integer)
-> (rec : Lazy (Ascending rest))
-> Ascending (rest * 10 + digit)
%name Ascending as, bs, cs
```
Generate an `Ascending` from an integer.
```idris
||| Covering function for `Ascending`
export
ascending : (i : Integer) -> Ascending i
ascending i =
if i < 0 then NegAsc (ascending (assert_smaller i $ negate i)) else
let digit = i `mod` 10
rest = i `div` 10
in if rest == 0
then believe_me $ Next digit rest (believe_me End)
else believe_me $ Next digit rest (ascending (assert_smaller i rest))
```
Convert an `Ascending` to a list
```idris
export
ascList : {i : Integer} -> Ascending i -> List Integer
ascList as = reverse $ ascList' i as []
where
ascList' : (j : Integer) -> Ascending j -> (acc : List Integer)
-> List Integer
ascList' k (NegAsc rec) acc = ascList' (negate k) rec acc
ascList' 0 End acc = acc
ascList' ((rest * 10) + digit) (Next digit rest rec) acc =
ascList' rest rec (digit :: acc)
```
## Descending Order
View an integer as a list of digits, ordered from most significant digit to
least significant digit.
For a clarifying example:
```idris hide
-- @@test Descending Digits Example
descendingExample : IO Bool
descendingExample = do
putStrLn "Expecting: \{show [1, 2, 3, 4, 5]}"
putStrLn "Got: \{show . decList $ descending 12345}"
pure $
```
```idris
decList (descending 12345) == [1, 2, 3, 4, 5]
```
The view itself, storing the current digit, and the rest of the number, both as
a raw integer and by a recursive `Ascending`. Acts as a proof that the number
can be reproduced by appending the current digit to the rest of the number.
```idris
||| A view of an integer as a list of digits in order of descending
||| signifigance
public export
data Descending : Integer -> Type where
||| Indicates that the number was negative
NegDec : (rec : Lazy (Descending (negate i))) -> Descending i
||| Indicates we have already seen all the digits of a number
Start : Descending 0
||| A digit and all the preceeding ones
Prev : (magnitude : Nat)
-> (digit : Integer)
-> (rest : Integer)
-> (rec : Lazy (Descending rest))
-> Descending ((digit * 10 ^ magnitude) + rest)
%name Descending ds, es, fs
```
Generate a `Descending` from an `Integer`
```idris
export
descending : (i : Integer) -> Descending i
descending i =
if i < 0 then NegDec (descending (assert_smaller i $ negate i)) else
let magnitude = log10 i
in if magnitude == 0
then believe_me $ Prev 0 0 0 Start
else descending' magnitude i
where
descending' : (magnitude : Nat) -> (j : Integer) -> Descending j
descending' 0 j = believe_me Start
descending' magnitude@(S m) j =
let digit = j `div` 10 ^ m
rest = j - digit * 10 ^ m
in believe_me $ Prev m digit rest (descending' m rest)
```
Convert a `Descending` to a list
```idris
export
decList : {i : Integer} -> Descending i -> List Integer
decList ds = reverse $ decList' ds []
where
decList' : {i : Integer} -> Descending i -> (acc : List Integer) ->
List Integer
decList' (NegDec rec) acc = decList' rec acc
decList' Start acc = acc
decList' (Prev magnitude digit rest rec) acc =
decList' rec (digit :: acc)
```

91
src/Util/Eff.md
View file

@ -6,7 +6,6 @@ Contains utility functions extending the functionality of the `eff` package.
module Util.Eff module Util.Eff
import Control.Eff import Control.Eff
import Data.Subset
import Text.ANSI import Text.ANSI
import System import System
@ -22,21 +21,12 @@ import System.File
Basic enumeration describing log levels, we define some (hidden) utility Basic enumeration describing log levels, we define some (hidden) utility
functions for working with these. functions for working with these.
The `Other n` log level is restricted to `n` greater than 4, to prevent
ambiguity between custom log levels and predefined log levels.
```idris ```idris
public export public export
data Level : Type where data Level = Err | Warn | Info | Debug | Trace | Other Nat
Err : Level
Warn : Level
Info : Level
Debug : Level
Trace : Level
Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level
``` ```
```idris hide <!-- idris
export export
levelToNat : Level -> Nat levelToNat : Level -> Nat
levelToNat Err = 0 levelToNat Err = 0
@ -53,7 +43,7 @@ natToLevel 1 = Warn
natToLevel 2 = Info natToLevel 2 = Info
natToLevel 3 = Debug natToLevel 3 = Debug
natToLevel 4 = Trace natToLevel 4 = Trace
natToLevel (S (S (S (S (S k))))) = Other (5 + k) natToLevel k = Other k
export export
Eq Level where Eq Level where
@ -67,7 +57,7 @@ export infixl 8 >+
export export
(>+) : Level -> Nat -> Level (>+) : Level -> Nat -> Level
(>+) x k = natToLevel (k + levelToNat x) (>+) x k = natToLevel (k + levelToNat x)
``` -->
Convert a `Level` into a colorized tag Convert a `Level` into a colorized tag
@ -139,8 +129,10 @@ handleLoggerIO max_level x =
else pure . ignore $ x else pure . ignore $ x
``` ```
Provide a family of effectful actions that emit log messages at the different Use the `WriterL "log" String` effect like a logging library. We'll provide a
log levels. few "log levels" as verbs for the effect, but no filtering is done, when logging
is enabled, all logs are always displayed, however the log level is indicated
with a colored tag.
```idris ```idris
export export
@ -162,10 +154,6 @@ debug x = send $ Log Debug x
export export
trace : Has Logger fs => Lazy String -> Eff fs () trace : Has Logger fs => Lazy String -> Eff fs ()
trace x = send $ Log Trace x trace x = send $ Log Trace x
export
logAt : Has Logger fs => Level -> Lazy String -> Eff fs ()
logAt level x = send $ Log level x
``` ```
## Choose ## Choose
@ -192,66 +180,3 @@ oneOfM : Has (Choose) fs => Foldable f =>
f (Eff fs a) -> Eff fs a f (Eff fs a) -> Eff fs a
oneOfM x = foldl alt empty x oneOfM x = foldl alt empty x
``` ```
## Subset
Reorder the first two elements of the first argument of a subset
```idris
public export
subsetReorderLeft : Subset (x :: g :: xs) ys -> Subset (g :: x :: xs) ys
subsetReorderLeft (e :: (e' :: subset)) = e' :: e :: subset
```
Add the same element to both arguments of a subset
```idris
public export
subsetConsBoth : {0 xs, ys : List a} -> {0 g : a} -> Subset xs ys
-> Subset (g :: xs) (g :: ys)
subsetConsBoth {xs = []} {ys = ys} [] = [Z]
subsetConsBoth {xs = (x :: xs)} {ys} (e :: subset) =
let rest = S e :: subsetConsBoth subset {g}
in subsetReorderLeft rest
```
A list is always a subset of itself
```idris
public export
subsetReflexive : {xs : List a} -> Subset xs xs
subsetReflexive {xs = []} = []
subsetReflexive {xs = (x :: xs)} =
let rest = subsetReflexive {xs}
in subsetConsBoth rest
```
If `xs` is a subset of `ys`, then it is also a subset of `ys + g`
```idris
public export
subsetConsRight : {0 g: _} -> {0 xs, ys: _} -> Subset xs ys -> Subset xs (g :: ys)
subsetConsRight {xs = []} {ys = ys} [] = []
subsetConsRight {xs = (x :: xs)} {ys} (e :: subset) =
S e :: subsetConsRight subset {g}
```
`xs` is always a subset of `xs + g`
```idris
public export
trivialSubset : {0 g : a} -> {xs : List a} -> Subset xs (g :: xs)
trivialSubset = subsetConsRight subsetReflexive
```
`fs - f` is always a subset of `f`
```idris
public export
minusLemma : {fs : List a} -> {0 x : a} -> {auto prf : Has x fs}
-> Subset (fs - x) fs
minusLemma {fs = (_ :: vs)} {prf = Z} = trivialSubset
minusLemma {fs = (w :: vs)} {prf = (S y)} =
let rest = minusLemma {fs = vs} {prf = y}
in subsetConsBoth rest
```

39
src/Years/Y2015.md
View file

@ -6,7 +6,7 @@ import Structures.Dependent.FreshList
import Runner import Runner
``` ```
```idris hide <!-- idris
import Years.Y2015.Day1 import Years.Y2015.Day1
import Years.Y2015.Day2 import Years.Y2015.Day2
import Years.Y2015.Day3 import Years.Y2015.Day3
@ -15,12 +15,7 @@ import Years.Y2015.Day5
import Years.Y2015.Day6 import Years.Y2015.Day6
import Years.Y2015.Day7 import Years.Y2015.Day7
import Years.Y2015.Day8 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 # Days
@ -78,36 +73,6 @@ y2015 = MkYear 2015 [
, day8 , day8
``` ```
## [Day 9](Y2015/Day9.md)
```idris
, day9
```
## [Day 10](Y2015/Day10.md)
```idris
, day10
```
## [Day 11](Y2015/Day11.md)
```idris
, day11
```
## [Day 12](Y2015/Day12.md)
```idris
, day12
```
## [Day 13](Y2015/Day13.md)
```idris
, day13
```
```idris ```idris
] ]
``` ```

10
src/Years/Y2015/Day1.md
View file

@ -1,9 +1,9 @@
# [Year 2015 Day 1](https://adventofcode.com/2015/day/1) # Year 2015 Day 1
Pretty simple, basic warmup problem, nothing really novel is on display here Pretty simple, basic warmup problem, nothing really novel is on display here
except the effectful part computations. except the effectful part computations.
```idris hide <!-- idris
module Years.Y2015.Day1 module Years.Y2015.Day1
import Control.Eff import Control.Eff
@ -11,7 +11,7 @@ import Control.Eff
import Runner import Runner
%default total %default total
``` -->
## Solver Functions ## Solver Functions
@ -76,8 +76,8 @@ part2 x = do
pure $ findBasement 1 0 input pure $ findBasement 1 0 input
``` ```
```idris hide <!-- idris
public export public export
day1 : Day day1 : Day
day1 = Both 1 part1 part2 day1 = Both 1 part1 part2
``` -->

125
src/Years/Y2015/Day10.md
View file

@ -1,125 +0,0 @@
# [Year 2015 Day 10](https://adventofcode.com/2015/day/10)
This day doesn't really add anything new, but we will show off our new views for
viewing integers as lists of digits.
```idris hide
module Years.Y2015.Day10
import Control.Eff
import Runner
```
```idris
import Data.String
import Data.List1
import Data.List.Lazy
import Data.Monoid.Exponentiation
import Data.Nat.Views
import Util
import Util.Digits
```
```idris hide
%default total
```
# Solver Functions
Produce a lazy lists of the digits of a number, in descending order of
significance. This effectively translates our new
[`Descending`](../../Util/Digits.md#descending-order) view to a `LazyList`.
```idris
lazyDigits : Integer -> LazyList Integer
lazyDigits i with (descending i)
lazyDigits i | (NegDec rec) = lazyDigits _ | rec
lazyDigits 0 | Start = []
lazyDigits ((digit * (10 ^ magnitude)) + rest) | (Prev _ digit rest rec) =
digit :: lazyDigits _ | rec
```
Apply the look-and-say rule to list of digits. We operate in the list-of-digits
space for efficiency, this number will grow into the millions of digits, and
Idris is currently lacking some needed primitive operations to perform this
operation in `Integer` space reasonably efficiently. A `LazyList` is used here
to avoid having to actually instantiate the entirety of these reasonably large
lists.
```idris
lookAndSay : LazyList Integer -> LazyList Integer
lookAndSay digits =
-- Flatten the list once more
lazyConcat
-- Convert the produced numbers into lists of their digits
. map lazyDigits
-- re-flatten our list
. lazyConcat
-- Count the number of occurrences of each digit and emit [occurances, digit]
. map (\xs@(head ::: tail) =>
(the (LazyList _) [natToInteger $ length xs, head]))
-- Group identical digits
. lazyGroup
$ digits
```
Apply the look-and-say rule to an integer, for repl testing
```idris
lookAndSay' : Integer -> Integer
lookAndSay' i =
let digits = lazyDigits i
res = lookAndSay digits
in unDigits res 0
where
unDigits : LazyList Integer -> (acc : Integer) -> Integer
unDigits [] acc = acc
unDigits (x :: xs) acc = unDigits xs (acc * 10 + x)
```
Repeatedly apply `lookAndSay` to a seed value, with logging
```idris
repeatLogged : Has Logger fs =>
(count : Nat) -> (seed : LazyList Integer) -> Eff fs $ LazyList Integer
repeatLogged 0 seed = pure seed
repeatLogged (S k) seed = do
trace "Remaining iterations: \{show (S k)} digits: \{show . count (const True) $ seed}"
repeatLogged k (lookAndSay seed)
```
# Part Functions
## Part 1
Parse our input, convert it into a list of digits, then run our `lookAndSay`
function on it 40 times, and count the output digits.
```idris
part1 : Eff (PartEff String) (Nat, LazyList Integer)
part1 = do
input <- askAt "input" >>= (note "Invalid input" . parsePositive)
let input = lazyDigits input
info "Input: \{show input}"
output <- repeatLogged 40 input
pure (count (const True) output, output)
```
## Part 2
Same thing, but 10 more times
```idris
part2 : (digits : LazyList Integer) -> Eff (PartEff String) Nat
part2 digits = do
output <- repeatLogged 10 digits
pure $ count (const True) output
```
```idris hide
public export
day10 : Day
day10 = Both 10 part1 part2
```

238
src/Years/Y2015/Day11.md
View file

@ -1,238 +0,0 @@
# [Year 2015 Day 11](https://adventofcode.com/2015/day/11)
This day provides a gentle introduction to refinement types, types which augment
other types with a predicate that must hold for all the values of the refined
type, which allow easily defining types as subsets of other types based on some
property of the acceptable elements.
While refinement types are quite easy to implement in Idris, and we easily could
implement the one we need for today's task as a throw away data structure just
for this module, we will be using the `refined`[^1] library's implementation for
the sake of getting on with it.
```idris hide
module Years.Y2015.Day11
import Control.Eff
import Runner
```
```idris
import Data.Vect
import Data.String
import Data.Refined.Char
import Util
```
## Data Structures and Parsing
Provide a predicate which establishes that a char is a lowercase alphabetic
character, the only type of character that passwords are allowed to contain. We
use the `FromTo` predicate from the `refined`[^1] library to restrict chars to
within the range from `a` to `z`.
This predicate has multiplicity 0, a full discussion of multiplicites and linear
types is out of scope for today, but put simply this enforces that a value of
this predicate type can be "used" at most 0 times, having the effect of erasing
the value at runtime, making this more or less a zero-cost abstraction.
```idris
0 IsPasswordChar : Char -> Type
IsPasswordChar = FromTo 'a' 'z'
```
Combine a `Char` with its corresponding `IsPasswordChar` predicate into a
combined "refined" type, whose elements are the subset of `Char`s that are
lowercase alphabetic characters.
```idris
record PasswordChar where
constructor MkPC
char : Char
{auto 0 prf : IsPasswordChar char}
%name PasswordChar pc
```
```idris hide
Show PasswordChar where
show (MkPC char) = singleton char
Eq PasswordChar where
x == y = x.char == y.char
```
A function to fallible convert `Char`s into refined `PasswordChar`s, this will
return `Just` if the `Char` satisfies the predicate, and `Nothing` otherwise,
aligning with the type-level guarantees of the `PasswordChar` type.
```idris
refineChar : Char -> Maybe PasswordChar
refineChar c = map fromSubset $ refine0 c
where
fromSubset : Subset Char IsPasswordChar -> PasswordChar
fromSubset (Element char prf) = MkPC char
```
Convenience function returning `a` as a `PasswordChar`
```idris
lowest : PasswordChar
lowest = MkPC 'a'
```
"Increment" a `PasswordChar`, changing it to the next letter (`a` becomes `b`,
`b` becomes `c`, so on), returning nothing if we go past `z`, corresponding to a
carry.
We do this by converting the internal `Char` to an integer, adding one to it,
then converting back to a `Char`. This low-level conversion loses the refinement
context, forcing us to call `refineChar` on the new value to bring it back into
the refined type, providing us type-level assurance that this function will
return `Nothing` if an overflow occurs.
```idris
incriment : PasswordChar -> Maybe PasswordChar
incriment (MkPC char) =
let next = chr $ ord char + 1
in refineChar next
```
A `Password` is a `Vect` of 8 `PasswordChar`s. This `Vect` is sorted in reverse
order compared to the `String` it corresponds to, with the right-most letter
first, to make implementing the `incrimentPassword` function a little easier and
cleaner.
We also provide conversion to/from a `String`
```idris
Password : Type
Password = Vect 8 PasswordChar
parsePassword : Has (Except String) fs => String -> Eff fs Password
parsePassword str = do
cs <- note "Password has incorrect number of characters: \{str}"
. toVect 8 . reverse . unpack $ str
cs <- note "Password contained invalid characters: \{str}"
$ traverse refineChar cs
pure cs
passwordToString : Password -> String
passwordToString = pack . toList . reverse . map char
```
Define a function to increment a `Password`, this function will "roll over",
producing `aaaaaaaa` if provided `zzzzzzzz`.
```idris
incrimentPassword : Vect n PasswordChar -> Vect n PasswordChar
incrimentPassword [] = []
incrimentPassword (x :: xs) =
case incriment x of
Nothing => lowest :: incrimentPassword xs
Just x => x :: xs
```
### Password validity
A password must contain a run of at least 3 incrementing characters, check this
by converting the `PasswordChar`s to their integer representations. Remember
that our `Password` `Vect` is backwards compared to the string representation.
```idris
incrimentingChars : Vect n PasswordChar -> Bool
incrimentingChars (z :: next@(y :: (x :: xs))) =
let [x, y, z] : Vect _ Int = map (ord . char) [x, y, z]
in if y == x + 1 && z == y + 1
then True
else incrimentingChars next
incrimentingChars _ = False
```
A password may not contain `i`, `o`, or `l`
```idris
noInvalidChars : Vect n PasswordChar -> Bool
noInvalidChars = not . (any (flip contains $ ['i', 'o', 'l'])) . map char
```
A password contains at least two different non-overlapping pairs.
We check this by pattern matching our password two characters at a time,
consuming both characters if a matched pair is found, and tacking on the `Char`
the list is composed of to an accumulator list as we go. This list is then
reduced to only its unique elements (it's `nub`), and checking to see if it's
length is at least 2.
```idris
containsPairs : Vect n PasswordChar -> Bool
containsPairs xs = length (nub $ pairs (reverse xs) []) >= 2
where
pairs : Vect m PasswordChar -> (acc : List Char) -> List Char
pairs [] acc = acc
pairs (x :: []) acc = acc
pairs (x :: (y :: xs)) acc =
if x == y
-- If there is a pair, consume it to prevent detecting overlapping pairs
then pairs xs (x.char :: acc)
-- If there isn't a pair, only consume one character
else pairs (y :: xs) acc
```
Combine our password criteria into one function
```idris
passwordCriteria : Vect n PasswordChar -> Bool
passwordCriteria xs = incrimentingChars xs && noInvalidChars xs && containsPairs xs
```
### Find the next password
Find the next password based on a criteria function
```idris
findNextPassword :
(f : Vect n PasswordChar -> Bool) -> (password : Vect n PasswordChar)
-> Vect n PasswordChar
findNextPassword f password =
let next = incrimentPassword password
in if f next
then next
else findNextPassword f next
```
## Part Functions
### Part 1
```idris
part1 : Eff (PartEff String) (String, Password)
part1 = do
input <- map trim $ askAt "input"
password <- parsePassword input
info "Starting password: \{show password} -> \{passwordToString password}"
let next_password = findNextPassword passwordCriteria password
pure (passwordToString next_password, next_password)
```
### Part 2
```idris
part2 : Password -> Eff (PartEff String) String
part2 password = do
info
"Second starting password: \{show password} -> \{passwordToString password}"
let next_password = findNextPassword passwordCriteria password
pure $ passwordToString next_password
```
```idris hide
public export
day11 : Day
day11 = Both 11 part1 part2
```
## References
[^1]: <https://github.com/stefan-hoeck/idris2-refined/>

132
src/Years/Y2015/Day12.md
View file

@ -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>

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>

14
src/Years/Y2015/Day2.md
View file

@ -1,14 +1,14 @@
# [Year 2015 Day 2](https://adventofcode.com/2015/day/2) # Year 2015 Day 2
This day provides us our first little taste of effectful parsing This day provides us our first little taste of effectful parsing
```idris hide <!-- idris
module Years.Y2015.Day2 module Years.Y2015.Day2
import Control.Eff import Control.Eff
import Runner import Runner
``` -->
```idris ```idris
import Data.List import Data.List
@ -16,9 +16,9 @@ import Data.List1
import Data.String import Data.String
``` ```
```idris hide <!-- idris
%default total %default total
``` -->
## Box structure ## Box structure
@ -130,8 +130,8 @@ part2 : (boxes : List Box) -> Eff (PartEff String) Integer
part2 boxes = pure . sum . map totalRibbon $ boxes part2 boxes = pure . sum . map totalRibbon $ boxes
``` ```
```idris hide <!-- idris
public export public export
day2 : Day day2 : Day
day2 = Both 2 part1 part2 day2 = Both 2 part1 part2
``` -->

14
src/Years/Y2015/Day3.md
View file

@ -1,15 +1,15 @@
# [Year 2015 Day 3](https://adventofcode.com/2015/day/3) # Year 2015 Day 3
This day provides a gentle introduction to `mutual` blocks and mutually This day provides a gentle introduction to `mutual` blocks and mutually
recursive functions. recursive functions.
```idris hide <!-- idris
module Years.Y2015.Day3 module Years.Y2015.Day3
import Control.Eff import Control.Eff
import Runner import Runner
``` -->
```idris ```idris
import Data.SortedSet import Data.SortedSet
@ -18,9 +18,9 @@ import Data.String
import Util import Util
``` ```
```idris hide <!-- idris
%default total %default total
``` -->
## Parsing and data structures ## Parsing and data structures
@ -152,8 +152,8 @@ part2 movements = do
pure . length $ locations pure . length $ locations
``` ```
```idris hide <!-- idris
public export public export
day3 : Day day3 : Day
day3 = Both 3 part1 part2 day3 = Both 3 part1 part2
``` -->

10
src/Years/Y2015/Day4.md
View file

@ -1,15 +1,15 @@
# [Year 2015 Day 4](https://adventofcode.com/2015/day/4) # Year 2015 Day 4
This day introduces us to a little bit of FFI, linking to openssl to use it's This day introduces us to a little bit of FFI, linking to openssl to use it's
`MD5` functionality. `MD5` functionality.
```idris hide <!-- idris
module Years.Y2015.Day4 module Years.Y2015.Day4
import Control.Eff import Control.Eff
import Runner import Runner
``` -->
```idris ```idris
import Data.String import Data.String
@ -196,8 +196,8 @@ part2 seed = do
pure number pure number
``` ```
```idris hide <!-- idris
public export public export
day4 : Day day4 : Day
day4 = Both 4 part1 part2 day4 = Both 4 part1 part2
``` -->

14
src/Years/Y2015/Day5.md
View file

@ -1,4 +1,4 @@
# [Year 2015 Day 5](https://adventofcode.com/2015/day/5) # Year 2015 Day 5
This day provides a nice chance to introduce This day provides a nice chance to introduce
[views](https://idris2.readthedocs.io/en/latest/tutorial/views.html), [views](https://idris2.readthedocs.io/en/latest/tutorial/views.html),
@ -6,13 +6,13 @@ specifically `String`'s
[`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList) [`AsList`](https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.String.html#Data.String.AsList)
view, which lets us treat `String`s as if they were lazy lists or iterators. view, which lets us treat `String`s as if they were lazy lists or iterators.
```idris hide <!-- idris
module Years.Y2015.Day5 module Years.Y2015.Day5
import Control.Eff import Control.Eff
import Runner import Runner
``` -->
```idris ```idris
import Data.String import Data.String
@ -20,9 +20,9 @@ import Data.String
import Util import Util
``` ```
```idris hide <!-- idris
%default total %default total
``` -->
## Nice Strings ## Nice Strings
@ -213,8 +213,8 @@ part2 _ = do
pure x pure x
``` ```
```idris hide <!-- idris
public export public export
day5 : Day day5 : Day
day5 = Both 5 part1 part2 day5 = Both 5 part1 part2
``` -->

28
src/Years/Y2015/Day6.md
View file

@ -1,14 +1,12 @@
# [Year 2015 Day 6](https://adventofcode.com/2015/day/6) # Year 2015 Day 6
Introduction to the advent of code classic 2d grid problem. <!-- idris
```idris hide
module Years.Y2015.Day6 module Years.Y2015.Day6
import Control.Eff import Control.Eff
import Runner import Runner
``` -->
```idris ```idris
import Util import Util
@ -21,9 +19,9 @@ import Data.String
import Data.IORef import Data.IORef
``` ```
```idris hide <!-- idris
%default total %default total
``` -->
## Parsing and data structures ## Parsing and data structures
@ -75,12 +73,12 @@ The three types of action that can be performed on a light.
data Action = On | Off | Toggle data Action = On | Off | Toggle
``` ```
```idris hide <!-- idris
Show Action where Show Action where
show On = "on" show On = "on"
show Off = "off" show Off = "off"
show Toggle = "toggle" show Toggle = "toggle"
``` -->
The range of coordinates that a command affects The range of coordinates that a command affects
@ -90,11 +88,11 @@ record Range (rows, cols : Nat) where
top_left, bottom_right : Coord rows cols top_left, bottom_right : Coord rows cols
``` ```
```idris hide <!-- idris
Show (Range rows cols) where Show (Range rows cols) where
show (MkRange top_left bottom_right) = show (MkRange top_left bottom_right) =
"\{show top_left} -> \{show bottom_right}" "\{show top_left} -> \{show bottom_right}"
``` -->
Helper function to extract a range of values from our Grid. Helper function to extract a range of values from our Grid.
@ -119,11 +117,11 @@ record Command (rows, cols : Nat) where
range : Range rows cols range : Range rows cols
``` ```
```idris hide <!-- idris
Show (Command rows cols) where Show (Command rows cols) where
show (MkCmd action range) = show (MkCmd action range) =
"{\{show action}: \{show range}}" "{\{show action}: \{show range}}"
``` -->
### Parsing ### Parsing
@ -334,8 +332,8 @@ part2 commands = do
pure brightness pure brightness
``` ```
```idris hide <!-- idris
public export public export
day6 : Day day6 : Day
day6 = Both 6 part1 part2 day6 = Both 6 part1 part2
``` -->

19
src/Years/Y2015/Day7.md
View file

@ -1,4 +1,4 @@
# [Year 2015 Day 7](https://adventofcode.com/2015/day/7) # Year 2015 Day 7
This day provides us a gentle introduction to dependent maps. This day provides us a gentle introduction to dependent maps.
@ -13,13 +13,13 @@ Ensuring that the input contains only one gate outputting for each wire is done
through throwing a runtime error in the parsing function if a second gate through throwing a runtime error in the parsing function if a second gate
outputting to a given wire is found in the input. outputting to a given wire is found in the input.
```idris hide <!-- idris
module Years.Y2015.Day7 module Years.Y2015.Day7
import Control.Eff import Control.Eff
import Runner import Runner
``` -->
```idris ```idris
import Data.Bits import Data.Bits
@ -31,9 +31,9 @@ import Data.SortedMap.Dependent
import Decidable.Equality import Decidable.Equality
``` ```
```idris hide <!-- idris
%default total %default total
``` -->
## Parsing and data structures ## Parsing and data structures
@ -53,10 +53,7 @@ Input : Type
Input = Either Literal Wire Input = Either Literal Wire
``` ```
Description of a Gate, tagged in the type with the name of the output wire. Description of a Gate, tagged in the type with the name of the output wire
This creates what is referred to as an "indexed type family", in this case a
family of `Gate` types indexed by values of type `Wire`.
```idris ```idris
data Gate : Wire -> Type where data Gate : Wire -> Type where
@ -252,8 +249,8 @@ part2 (circut, value) = do
pure value pure value
``` ```
```idris hide <!-- idris
public export covering public export covering
day7 : Day day7 : Day
day7 = Both 7 part1 part2 day7 = Both 7 part1 part2
``` -->

377
src/Years/Y2015/Day8.md
View file

@ -1,9 +1,6 @@
# [Year 2015 Day 8](https://adventofcode.com/2015/day/8) # Year 2015 Day 8
This day provides a more in depth introduction to writing effectful parsers, <!-- idris
making use of state and non-determinism in our parsers.
```idris hide
module Years.Y2015.Day8 module Years.Y2015.Day8
import Control.Eff import Control.Eff
@ -11,341 +8,169 @@ import Control.Eff
import Data.Primitives.Interpolation import Data.Primitives.Interpolation
import Runner import Runner
``` -->
```idris ```idris
import Data.String import Data.String
import Data.Vect import Data.Vect
import Data.List.Lazy
import Data.Either import Data.Either
``` ```
## Parsing ## Parsing
A "Parser" is an effectful computation that has access to a list of chars as Effect alias for a parser
state, can throw exceptions of type `String`, and has non-determinism through
the `Choose` effect, which consumes some of the state to potentially return a
value.
### Basic operations
Get the next character out of the parser state, updating the state to consume
that character.
```idris ```idris
nextChar : Has (State (List Char)) fs => Has (Except String) fs => Eff fs Char Parser : List (Type -> Type)
nextChar = do Parser =
c :: rest <- get [Choose, State (List Char), Except String]
| [] => throw "End of input"
put rest
pure c
``` ```
Attempt to parse a single character based on the supplied predicate, consuming Get the next character from the state, modifying it in place
the character from the state and throwing the provided error if the predicate
does not hold over the consumed character.
```idris ```idris
char : Has (State (List Char)) fs => Has (Except String) fs => getNext : Eff Parser Char
(pred : Char -> Bool) -> (err : Char -> String) -> Eff fs Char getNext = do
char pred err = do chars <- get
c <- nextChar case chars of
unless (pred c) (throw $ err c) [] => throw "End of Input"
pure c (x :: xs) => do
put xs
pure x
``` ```
Type alias for a parser Parse a quote
```idris ```idris
Parser : (res : Type) -> Type quote : Eff Parser ()
Parser res = Eff [State (List Char), Except String, Choose, Logger] res
```
Parse 0+ of a thing, speculatively attempting to apply the given parser. In the
event the supplied parser fails, catch the error, unwind changes to the state,
and return an empty list, otherwise append the parsed element to the head of the
returned list and recurse.
The rewinding of the state on failure _could_ be handled implicitly by the
effect stack if `Except` was structured a bit differently, but that's a topic
for another day.
```idris
many : (f : Parser t) -> Parser (List t)
many f = do
state <- get
Just x <- lift $ catch (\ _ => pure Nothing) (map Just f)
| Nothing => do
put state
pure []
map (x ::) $ many f
```
"Parse" the end of the input, returning a unit if we are at the end of input,
throwing an error otherwise.
```idris
endOfInput : Parser ()
endOfInput = do
[] <- get
| xs => throw "Expected end of input, state non empty: `\{pack xs}`"
pure ()
```
### Character Classes
Parse a single `"`, throwing an error if the current character is anything else.
Returns a unit since there is only one possible character this parses, and this
avoids us having to discard the character later in our `string` parser.
```idris
quote : Parser ()
quote = do quote = do
_ <- char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`") char <- getNext
pure () if char == '"'
then pure ()
else throw "Expected quote, found: \{show char}"
``` ```
Parse any character except `\` or `"` Parse a char that's not a quote or an escape character
```idris ```idris
normal : Parser Char normal : Eff Parser Char
normal = normal = do
char char <- getNext
(\x => not $ any (== x) (the (List _) ['\\', '"'])) if any (char ==) (the (List _) ['\\', '"'])
(\x => "Expected normal, got `\{String.singleton x}`") then throw "Tried to parse a special character as normal \{show char}"
else pure char
``` ```
#### Escaped Characters Parse a hex digit
Parse the character sequence `\"`, returning just the `"`. Despite the fact that
can only return one possible character, like `quote` above, we return the parsed
character, as we intend to provide all the escaped character parsers to the
`oneOfM` combinator later.
```idris ```idris
eQuote : Parser Char hexDigit : Eff Parser Int
eQuote = do hexDigit = do
_ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") char <- getNext
char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`") case toLower char of
'0' => pure 0x0
'1' => pure 0x1
'2' => pure 0x2
'3' => pure 0x3
'4' => pure 0x4
'5' => pure 0x5
'6' => pure 0x6
'7' => pure 0x7
'8' => pure 0x8
'9' => pure 0x9
'a' => pure 0xa
'b' => pure 0xb
'c' => pure 0xc
'd' => pure 0xd
'e' => pure 0xe
'f' => pure 0xf
_ => throw "Invalid hex digit: \{show char}"
``` ```
Parse the character sequence `\\`, returning just the second `\`. Parse an escaped character
```idris ```idris
eSlash : Parser Char escaped : Eff Parser Char
eSlash = do escaped = do
_ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") escape <- getNext
char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") if escape == '\\'
then do
first <- getNext
case first of
'\\' => pure '\\'
'"' => pure '"'
'x' => do
[x, y] : Vect _ Int <- sequence [hexDigit, hexDigit]
-- Fails to compile
-- pure . chr $ x * 0x10 + y
-- Compiles
pure . (const 'a') $ x * 0x10 + y
_ => throw "Invalid Escape Character: \{show first}"
else throw "Tried to parse non escape as escape \{show escape}"
``` ```
Convert a lowercase hexadecimal digit to its numerical value. Parse any non-quote character
```idris ```idris
fromHex : Char -> Int character : Eff Parser Char
fromHex c = character = oneOfM (the (List _) [escaped, normal])
if ord c >= 97
then ord c - 87
else ord c - 48
``` ```
Parse a character sequence `\xAB`, where `AB` are hexadecimal digits, and decode Run a parser until it runs out
the numerical value of `AB`, as a hexadecimal number, into its corresponding
character.
```idris ```idris
eHex : Parser Char parseMany : Eff Parser t -> Eff Parser (List t)
eHex = do parseMany x = do
_ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") Just next <- lift $ catch (\_ => pure Nothing) (map Just x)
_ <- char (== 'x') (\x => "Expected `x`, got `\{String.singleton x}`") | _ => pure []
[x, y] <- map (map $ fromHex . toLower) . map (next ::) (parseMany x)
sequence .
Vect.replicate 2 $
(char
isHexDigit
(\x => "Expected hex digit, got `\{String.singleton x}`"))
pure . chr $ x * 0x10 + y
``` ```
Use the `oneOfM` combinator to combine our escaped character parsers into a Parse any number of non-quote characters
single character class. `oneOfM` uses the `Choice` effect to try all of the
provided parsers, conceptually in parallel, returning all of the results.
```idris ```idris
escaped : Parser Char characters : Eff Parser (List Char)
escaped = oneOfM $ the (List _) [eQuote, eSlash, eHex] characters = parseMany character
``` ```
### Top Level Class Parse a quote delimited string
Combine our `normal` and `escaped` parsers into a single parser for non-quote
characters.
```idris ```idris
character : Parser Char parseString : Eff Parser (List Char)
character = oneOfM $ the (List _) [normal, escaped] parseString = do
```
Parse a string literal by describing its layout as a quote (`"`), followed by
any number of characters, then another quote, followed by the end of input.
Return the characters between the outer quotes.
```idris
string : Parser (List Char)
string = do
quote quote
xs <- many character xs <- characters
quote quote
endOfInput
pure xs pure xs
``` ```
### Running a parser Run a parser
Run a parser, with some debug logging, by peeling the parsing effects of of the
type. The order is important here, remember that function composition "runs"
right to left.
We peel the state off the type first, so that we can get implicit "rewinding" of
the state inside of our combinators, like `oneOfM`.
For a full understanding of what's going on here, we need to see how the type
signature changes as we peel effects off the type, you can uncomment the
commented lines, and comment out the rest of the function, modifying the
`let output =` line to follow along yourself, though the types you get may look
a little different due to idris evaluating type alaises like `Eff` for you, I am
keeping them in aliased forms, and excluding `Logger`, which doesn't impact the
semantic of parsing, to keep the examples concise:
- `runstate (unpack str) $ x`
This produces a value with type
`Eff [Except String, Choose] (List Char, List Char)`. In this tuple of values,
the first element is the actual output of the parser, and the second element
is the state after the parser has run.
- `runExcept . runState (unpack str) $ x`
This produces a value with type
`Eff [Choose] (Either String (List Char, List Char))`. This corresponds to a
computation that either returns our tuple of output and state from before, or
an error. Important to note here is that, in the error case, we only return a
`String` (our error type), our state is discarded.
- `runChoose {f = LazyList} . runExcept . runState (unpack str) $ x`
The `Choose` effect, works with any type that implements the `Alternative`
interface, and the choice of type impacts the semantics. A full discussion of
this is beyond the scope for today, but we chose to "run" `Choose` with
`LazyList`, which effectively gives us an iterator over all the possible
parsings of our input text.
This produces a value with type
`Eff [] (LazyList (Either String (List Char, List Char)))`. When we hit an
application of `Choose`, like `oneOfM`, all possibilities will be tried and
each one will be added to our output `LazyList`. Because this is a `LazyList`,
and not a `List`, only values we actually inspect are generated, allowing
parsing to terminate after the first successful parse without having to
generate the rest of the list.
Note that we have an independent possible state value for each slot in the
list, this speaks to this effect stack, when run in this order, providing a
sort of branching behavior for states, allowing different branches in the
`Choose` effect to modify their state without impacting the state of other
branches.
From there, we run our `lazyRights` helper function over the outputs `LazyList`
to discard parsing paths that result in an error, extract the first element of
each tuple, get the head of the list, if one still exists, and use `pack` to
convert the contents of the resulting `Maybe (List Char)` to a string. Then a
little bit of debug logging, and return the output.
```idris ```idris
runParser : Has Logger fs => Parser (List Char) -> String runParser : Eff Parser t -> String -> Maybe t
-> Eff fs $ Maybe String runParser m str =
runParser x str = do map fst . head' . rights
info "Parsing: \{str}" . extract . runChoose {f = List} . runExcept . runState (unpack str)
-- let outputs = $ m
-- runChoose {f = LazyList} . runExcept . runState (unpack str) $ x
-- ?parser_types
outputs <-
lift . runChoose {f = LazyList} . runExcept . runState (unpack str) $ x
let output = map pack . head' . map fst . lazyRights $ outputs
case output of
Nothing =>
debug "Failed: \{show outputs}"
Just y => do
debug "Got: \{y}"
trace "\{show outputs}"
pure output
where
lazyRights : LazyList (Either a b) -> LazyList b
lazyRights [] = []
lazyRights (Left _ :: xs) = lazyRights xs
lazyRights (Right x :: xs) = x :: lazyRights xs
```
## Escaping characters
This is much more boring the the parsing, we just do simple recursive pattern
matching on the characters of the provided string, escaping `"` and `\`, and
surround the resulting string with quotes.
```idris
escape : String -> String
escape str = "\"\{pack . escape' . unpack $ str}\""
where
escape' : List Char -> List Char
escape' [] = []
escape' ('"' :: xs) = '\\' :: '"' :: escape' xs
escape' ('\\' :: xs) = '\\' :: '\\' :: escape' xs
escape' (x :: xs) = x :: escape' xs
``` ```
## Part Functions ## Part Functions
### Part 1 ### Part 1
Convert the inputs into a list of lines, traverse our parser over it, deal with
possible failures by sequencing the `List (Maybe String)` into a
`Maybe (List String)`, and the compute the difference in character counts.
```idris ```idris
part1 : Eff (PartEff String) (Int, List String) part1 : Eff (PartEff String) (Nat, List (List Char, List Char))
part1 = do part1 = do
inputs <- map lines $ askAt "input" inputs <- map (lines . trim) $ askAt "input"
outputs <- traverse (runParser string) inputs let outputs = map (map pack . runParser parseString) inputs
Just outputs <- pure $ sequence outputs let pairs = zip inputs outputs
| _ => throw "Some strings failed to parse" let debug_out = joinBy "\n" . map show $ pairs
let difference = putStrLn debug_out
sum $ zipWith (\x, y => strLength x - strLength y) inputs outputs ?part1_rhs_1
pure (difference, inputs)
``` ```
### Part 2 <!-- idris
Map our character escaping function over our input string and compute the
difference in character counts.
Make a little stop along the way to ensure that escape -> parse round trips
without changing the content of the string.
```idris
part2 : List String -> Eff (PartEff String) Int
part2 inputs = do
let outputs = map escape inputs
Just reversed_outputs <- map sequence . traverse (runParser string) $ outputs
| _ => throw "Reversing escaping of the inputs failed"
unless (all id $ zipWith (==) inputs reversed_outputs) $ do
debug . delay . joinBy "\n" . map show . filter (\(x, y, z) => x /= z) $
zip3 inputs outputs reversed_outputs
throw "Parsed outputs were not identical to inputs"
let difference =
sum $ zipWith (\x, y => strLength y - strLength x) inputs outputs
pure difference
```
```idris hide
public export public export
day8 : Day day8 : Day
day8 = Both 8 part1 part2 day8 = First 8 part1
``` -->

294
src/Years/Y2015/Day9.md
View file

@ -1,294 +0,0 @@
# [Year 2015 Day 9](https://adventofcode.com/2015/day/9)
This day provides our first example of a graph traversal problem. We'll use a
`Choose` based effectful breath first search to identify all the possible paths
meeting the problem criteria, and then figure out the length in a separate step.
This isn't a particularly efficient solution, but its good enough for this small
problem size.
```idris hide
module Years.Y2015.Day9
import Control.Eff
import Runner
```
```idris
import Data.String
import Data.List1
import Data.Vect
import Data.List.Lazy
import Data.SortedMap
import Data.SortedSet
import Util
```
## Parsing and data structures
### Parsing
Define a location pair as a collection of two locations and a distance between
them (as this graph is undirected), as well as some type aliases, a `contains`
method to test if a pair covers a given location, and implement `Foldable` for
the type to get access to the standard library utility methods.
`DistanceMap` serves as a slightly fancy adjacency list for our graph
representation. We'll load this into a `Reader` effect to avoid having to pass
it around as an explicit argument to every function later on once it's been
computed.
```idris
Location : Type
Location = String
Distance : Type
Distance = Integer
record LocationPair (l : Type) where
constructor MkLP
locations : Vect 2 l
distance : Integer
%name LocationPair lp, mp, np, op
contains : Eq l => l -> LocationPair l -> Bool
contains x lp =
case find (== x) lp.locations of
Nothing => False
Just _ => True
Foldable LocationPair where
foldl f acc lp = foldl f acc lp.locations
foldr f acc lp = foldr f acc lp.locations
toList lp = toList lp.locations
LP : Type
LP = LocationPair Location
DistanceMap : Type
DistanceMap = SortedMap Location (List LP)
```
```idris hide
Show l => Show (LocationPair l) where
show (MkLP [x, y] distance) = "\{show x} <-> \{show y}: \{show distance}"
```
Perform simple, pattern matching based parsing of a location pair.
```idris
parseLocationPair : Has (Except String) fs =>
String -> Eff fs LP
parseLocationPair str = do
from ::: ["to", to, "=", dist] <- pure $ split (== ' ') str
| _ => throw "Badly formatted input string: \{str}"
dist <- note "Bad distance: \{dist}" $ parsePositive dist
pure $ MkLP [from, to] dist
```
Convert a list of pairs to a `DistanceMap`, a mapping from a location to all the
location pairs that cover it. To keep this function readable, we do this inside
an inner function with the `State DistanceMap` effect.
Since the inner function is recursive, instead of extracting the result after
running the state effect, we lift it into an unconstrained `fs` so we can borrow
the stack-saftey from our runner's top level `runEff`.
```idris
pairsToMap : List LP -> Eff fs DistanceMap
pairsToMap lps = do
(_, out) <- lift . runState empty $ insertPairs lps
pure out
where
insertLoc : LP -> (loc : Fin 2) -> Eff [State DistanceMap] ()
insertLoc lp loc = do
let loc = (index loc lp.locations)
list <- map (lookup loc) get
case list of
Nothing => modify $ insert loc [lp]
Just xs => modify $ insert loc (lp :: xs)
insertPair : LP -> Eff [State DistanceMap] ()
insertPair lp = traverse_ (insertLoc lp) (the (List _) [0, 1])
insertPairs : List LP -> Eff [State DistanceMap] ()
insertPairs lps = traverse_ insertPair lps
```
## Solver functions
Generate all the possible paths originating from `current` with length `depth`,
which is set to the number of locations in the calling function to provide the
"visits each node once" property.
The `path` argument accumulates the path taken by this particular branch of the
breadth first search. It is accumulated in reverse order, but this doesn't
really matter as this graph is undirected.
We use the `Choose` effect to explore every possible link connecting to the
current node, after filtering the possible links for ones that satisfy the
problem constraints.
```idris
paths : Has (Reader DistanceMap) fs => Has Choose fs => Has Logger fs =>
(path : List Location)
-> (depth : Nat)
-> (current : Location)
-> Eff fs (List Location)
paths path 0 current = empty
paths path 1 current =
if contains current path
then empty
else pure $ current :: path
paths path (S depth') current = do
debug "Paths from \{current} at \{show (S depth')} having visited \{show path}"
-- If we are in the path list, we have revisited this node, bail
False <- pure $ contains current path
| _ => empty
-- Update our path list to contain ourself
let path = current :: path
-- Find our next possible steps, bailing out if there are none
Just nexts <- map (lookup current) ask
| _ => do empty
-- Convert it to a list of locations
let nexts = concat . map toList $ nexts
-- Filter out any that are already in the path, this would be covered by the
-- check at the start of this function, but this cleans up the logs
let nexts = filter (not . (flip contains) path) nexts
-- Select our next node
next <- oneOf nexts
paths path depth' next
```
Calculate all the possible paths that satisfy the problem constraints.
As a minor optimization, we only explore the paths leading out of a single
arbitrary location to start with, and then take advantage of a symmetry of the
problem, collecting all the "rotations" of each output path to cheaply calculate
all the paths that take all the same steps as our "seed" path, but have
different starting and ending locations.
```idris
allPaths :
Has (Reader DistanceMap) fs => Has Logger fs => Has (Except String) fs =>
Eff fs $ SortedSet (List Location)
allPaths = do
locs <- map keys ask
first <- note "No locations" $ head' locs
paths <- lift . runChoose {f = LazyList} $
paths [] (length locs) first {fs = [Choose, Reader _, Logger]}
pure $ buildSet paths empty
where
insertPaths : List (List Location) -> (acc : SortedSet (List Location))
-> SortedSet (List Location)
insertPaths [] acc = acc
insertPaths (x :: xs) acc = insertPaths xs (insert x acc)
buildSet : LazyList (List Location) -> (acc : SortedSet (List Location))
-> SortedSet (List Location)
buildSet [] acc = acc
buildSet (x :: xs) acc =
let rots = rotations x
in buildSet xs (insertPaths rots acc)
```
Calculate the length of a path by recursively destructuring the list and looking
up each pair of locations in our `DistanceMap`.
```idris
pathLen : Has (Reader DistanceMap) fs => Has (Except String) fs =>
(path : List Location) -> Eff fs Integer
pathLen [] = pure 0
pathLen (x :: []) = pure 0
pathLen (x :: (y :: xs)) = do
lps <- map (lookup x) ask >>= note "Not found in distance map: \{x}"
lp <- note "Pair not found \{x} \{y}" $
find (\l => contains x l && contains y l) lps
map (lp.distance +) $ pathLen (y :: xs)
```
Calculate the shortest path from a list of paths by recursively comparing
lengths.
```idris
shortestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
(paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
shortestPath paths = do
shortest paths Nothing
where
shortest : List (a, Integer) -> (acc : Maybe (a, Integer))
-> Eff fs (a, Integer)
shortest [] acc = note "No paths" acc
shortest (x :: xs) acc =
case acc of
Nothing => shortest xs (Just x)
Just y =>
if (snd x) < (snd y)
then shortest xs (Just x)
else shortest xs (Just y)
```
Calculate the longest path from a list of paths by recursively comparing
lengths.
```idris
longestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
(paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
longestPath paths = do
longest paths Nothing
where
longest : List (a, Integer) -> (acc : Maybe (a, Integer))
-> Eff fs (a, Integer)
longest [] acc = note "No paths" acc
longest (x :: xs) acc =
case acc of
Nothing => longest xs (Just x)
Just y =>
if (snd x) > (snd y)
then longest xs (Just x)
else longest xs (Just y)
```
## Part Functions
### Part 1
Parse our locations, turn them into a `DistanceMap`, load that into our reader,
generate our paths, then find the one with the shortest length.
```idris
part1 :
Eff (PartEff String) (Integer, (DistanceMap, List (List Location, Integer)))
part1 = do
locations <- map lines (askAt "input") >>= traverse parseLocationPair
info "Locations: \{show locations}"
distance_map <- pairsToMap locations
info "Distance map: \{show distance_map}"
runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do
paths <- map Prelude.toList allPaths
trace "Paths: \{show paths}"
info "Found \{show $ length paths} paths"
distances <- traverse pathLen paths
let pairs = zip paths distances
(path, len) <- shortestPath pairs
info "Shortest Path: \{show path} \{show len}"
pure (len, (distance_map, pairs))
```
### Part 2
Feed the locations back into a longest path function
```idris
part2 : (DistanceMap, List (List Location, Integer))
-> Eff (PartEff String) Integer
part2 (distance_map, pairs) = do
runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do
(path, len) <- longestPath pairs
info "Longest Path: \{show path} \{show len}"
pure len
```
```idris hide
public export
day9 : Day
day9 = Both 9 part1 part2
```