diff --git a/.gitignore b/.gitignore index fbd3d96..5224155 100644 --- a/.gitignore +++ b/.gitignore @@ -4,5 +4,3 @@ inputs/ support/*.o support/advent-support tmp/ -book/ -index.html diff --git a/README.md b/README.md index 48f7b08..f40d0a7 100644 --- a/README.md +++ b/README.md @@ -1,33 +1,10 @@ # Advent 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 -Idris files. +of one single idris application, and thoroughly document the results as literate +idris files. -## Authors Note - -This entire book is a single literate code base, the source code is available at -. - -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: -. - -## Index of non-day modules +# Index of non-day modules - [Runner](src/Runner.md) @@ -49,100 +26,14 @@ solution. Extend the functionality of the effects included in the [eff](https://github.com/stefan-hoeck/idris2-eff/) library - - [Util.Digits](src/Util/Digits.md) - - 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 +# Index of years and days - 2015 - [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) - - An early hint of effectful parsing. - - [Day 3](src/Years/Y2015/Day3.md) - - Peculiarities of writing mutually recursive functions in dependently typed - languages. - - [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) - - First introduction to views and dependent pattern matching[^1]. - - [Day 6](src/Years/Y2015/Day6.md) - - Naive approach to handling the first 2d grid problem. - - [Day 7](src/Years/Y2015/Day7.md) - - Introduces dependent maps and indexed type families. - - [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] - - - [Day 14](src/Years/Y2015/Day14.md) - - Introduction to streams, infinite collections of data - -## 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]: diff --git a/advent.ipkg b/advent.ipkg index d4d13fe..1ac1a6e 100644 --- a/advent.ipkg +++ b/advent.ipkg @@ -16,32 +16,24 @@ authors = "Nathan McCarty" depends = base , contrib , structures - , tailrec , eff , elab-util - , sop , ansi , if-unsolved-implicit , c-ffi - , refined -- modules to install modules = Runner , Util , Util.Eff - , Util.Digits - , Array - , Parser - , Parser.Interface - , Parser.Numbers - , Parser.JSON + , Grid -- main file (i.e. file to load at REPL) main = Main -- name of executable executable = "advent" -opts = "--directive lazy=weakMemo" +-- opts = sourcedir = "src" -- builddir = -- outputdir = diff --git a/book.toml b/book.toml deleted file mode 100644 index a4387d0..0000000 --- a/book.toml +++ /dev/null @@ -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" diff --git a/scripts/build-book b/scripts/build-book deleted file mode 100755 index fd108e3..0000000 --- a/scripts/build-book +++ /dev/null @@ -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(*.¬-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 ; - 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/''//; - $output ~~ s:g/'
'//; - $output ~~ s:g/'\\*'/*/; - $output ~~ s:g/'\\_'/_/; - $output ~~ s:g/'\\\\'/\\/; - $output ~~ s:g/''/<\/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); -} diff --git a/src/Array.md b/src/Array.md deleted file mode 100644 index 2721297..0000000 --- a/src/Array.md +++ /dev/null @@ -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 -``` diff --git a/src/Grid.md b/src/Grid.md new file mode 100644 index 0000000..ceb6a22 --- /dev/null +++ b/src/Grid.md @@ -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 +``` diff --git a/src/Main.md b/src/Main.md index 1d0e2c1..a913135 100644 --- a/src/Main.md +++ b/src/Main.md @@ -76,7 +76,7 @@ data Error : Type where A `Show` implementation for `Error` is provided, hidden in this document for brevity. -```idris hide + ## Extract the year and day @@ -181,8 +181,8 @@ failures doing so. ## Handling the arguments and finding the input 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 -the effects list. +blackhole the logs. Afterwards, use `logHandler` to introduce the logging +`Writer` into the effects list. ```idris -- 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 -Makes use of `Logger`'s `handleLoggerIO` function to "lower" logging actions -into `IO` within the effect. +This function uses the provided `String -> IO ()` to remove the `Writer` from +the effects list by translating `tell` calls to IO actions within the effect. ```idris -- Lowers logging into IO within the effect using the given IO function diff --git a/src/Parser.md b/src/Parser.md deleted file mode 100644 index 9eacc0b..0000000 --- a/src/Parser.md +++ /dev/null @@ -1,8 +0,0 @@ -# Parsing Utilties - -```idris -module Parser - -import public Parser.Interface as Parser -import public Parser.ParserState as Parser -``` diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md deleted file mode 100644 index 53be055..0000000 --- a/src/Parser/Interface.md +++ /dev/null @@ -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 -``` diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md deleted file mode 100644 index 7baf9fa..0000000 --- a/src/Parser/JSON.md +++ /dev/null @@ -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 -``` diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md deleted file mode 100644 index e7adbf8..0000000 --- a/src/Parser/Numbers.md +++ /dev/null @@ -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") -``` diff --git a/src/Parser/ParserState.md b/src/Parser/ParserState.md deleted file mode 100644 index 1927d75..0000000 --- a/src/Parser/ParserState.md +++ /dev/null @@ -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]: diff --git a/src/README.md b/src/README.md deleted file mode 120000 index 32d46ee..0000000 --- a/src/README.md +++ /dev/null @@ -1 +0,0 @@ -../README.md \ No newline at end of file diff --git a/src/Runner.md b/src/Runner.md index 31b036e..500821b 100644 --- a/src/Runner.md +++ b/src/Runner.md @@ -22,15 +22,16 @@ import public Util.Eff # Effectful Parts 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 -type of the error value for the `Except` effect, we construct a type level -function to have a single source of truth. The `err` type can be any type with a -`Show` implementation, but that constraint will be tacked on in the next step. +the available effects are meant to be the same across both parts, only varying +in the type of the error value in the `Except` effect, I construct a type level +function to have a single source of truth for this. The `err` type can be any +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 -to pass in the input, to make the top level API a little bit cleaner. `IO` is +A `Writer` effect is provided for logging, and a `Reader` effect is provided to +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 -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. ```idris @@ -45,19 +46,19 @@ PartEff err = # The `Day` Record The `Day` type groups together an effectful `part1` computation, an optional -effectful `part2` computation, and the day number, with some type wrangling to -get the type system out of our way. +effectful `part2` computation, the day number, and does some type wrangling to +get the type system out of our way on this one. `part1` and `part2` are allowed independent output and error types, and this 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. 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 -the erased `ctx` type, which is totally opaque to the runner. The code in `Main` -will provide the value of the `ctx` type produced as part of the output of -`part1` and as the input of `part2`. +resulting from parsing, between `part1` and `part2`, and this is achieved by the +erased `ctx` type, which is totally opaque here. The runner code in `Main` will +provide the value of the `ctx` type produced as part of the output of `part1` as +the input of `part2`. ```idris ||| Model solving a single day @@ -79,9 +80,9 @@ record Day where 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 -requiring that `part2` be wrapped in a `Just` when there is one. We provide a -pair of constructors for the case where there is only a `part1`, as well as one -for when there is a `part1` and a `part2`. +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` and for where +there is a `part1` and a `part2` that handle that for us. ```idris namespace Day @@ -90,7 +91,8 @@ namespace Day ### First 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 ||| 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 -The `Both` constructor does less heavy lifting, the only thing it needs to do is -wrap `part2` in a `Just`. +The `Both` constructor does a little bit less heavy lifting, the only thing it +needs to do for us is wrap `part2` in a `Just`. ```idris ||| Constructor for a day with both parts ready to run @@ -121,17 +123,16 @@ wrap `part2` in a `Just`. ## Freshness We will be using a _Fresh List_ from the -[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build our -API defensively against duplicate days and cosmetically annoying out of order -day registration. A Fresh List structurally only allows you to prepend/cons an -element onto it when it satisfies some _freshness criteria_ relative to the -elements already contained in the list. +[structures](https://git.sr.ht/~thatonelutenist/Structures) package to build +defensiveness into the API. A Fresh List structurally only allows you to prepend +an element onto it when it satisfies some _freshness_ criteria relative to the +elements already 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 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 -the same day number. +Fresh List is sorted in ascending order and that no two `Day`s have the same day +number. ```idris ||| Freshness criteria for days @@ -149,7 +150,7 @@ FreshDay x y = x.day < y.day # The `Year` Record 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 ||| 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 in a `FreshList` in `Advent`, so we need to provide a freshness criteria for -`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 with `FreshDay`. +`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 +with `FreshDay`. ```idris ||| Freshness criteria for years @@ -186,7 +186,8 @@ FreshYear x y = x.year < y.year # The `Advent` Record 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 ||| Collect all years diff --git a/src/SUMMARY.md b/src/SUMMARY.md deleted file mode 100644 index 3fad4c9..0000000 --- a/src/SUMMARY.md +++ /dev/null @@ -1,38 +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) - - [Day 14 - Introduction to Streams](Years/Y2015/Day14.md) diff --git a/src/Util.md b/src/Util.md index 7d1342e..92b301a 100644 --- a/src/Util.md +++ b/src/Util.md @@ -9,69 +9,15 @@ module Util import Data.SortedSet import Data.String import Data.List.Lazy -import Data.List1 -import Data.Vect -import Data.Fin %default total ``` -## Foldable - -General utility functions for foldables - -```idris hide -namespace Foldable -``` - -### minBy - -```idris - ||| Get the minimum element of a collection using the provided comparison - ||| function and seed value - export - minBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a - minBy cmp acc x = - foldl - (\acc, e => - case e `cmp` acc of - LT => e - _ => acc) - acc x -``` - -```idris - ||| Get the maximum element of a collection using the provided comparison - ||| function and seed value - export - maxBy : Foldable f => (cmp : a -> a -> Ordering) -> (acc : a) -> f a -> a - maxBy cmp acc x = - foldl - (\acc, e => - case e `cmp` acc of - GT => e - _ => acc) - acc x -``` - -## Functions - -### repeatN - -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 -```idris hide + ### mapLeft @@ -85,147 +31,18 @@ Applies a function to the contents of a `Left` if the value of the given 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 -``` - -### Convert a list to a vect as a sigma type - -```idris - export - listToVect : List a -> (n : Nat ** Vect n a) - listToVect xs = (length xs ** fromList xs) -``` - -## Fin - -```idris hide -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 Define some operations for pairs of numbers, treating them roughly like vectors ### Addition and Subtraction -```idris hide + ```idris public export @@ -241,9 +58,9 @@ namespace Pair Extend `Data.SortedSet` -```idris hide + ### length @@ -259,9 +76,9 @@ Count the number of elements in a sorted set Extend `Data.String` -```idris hide + ### isSubstr @@ -292,66 +109,18 @@ off of the string at a time, checking if the needle is a prefix at each step. ### Cartesian product -```idris hide -namespace LazyList -``` - Lazily take the cartesian product of two foldables ```idris - export - cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f) - cartProd x y = - let y = foldToLazy y - in foldr (\e, acc => combine e y acc) [] x - where - foldToLazy : Foldable a' => a' e' -> LazyList e' - foldToLazy x = foldr (\e, acc => e :: acc) [] x - combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f) - combine x [] rest = rest - combine x (y :: ys) rest = (x, y) :: combine x ys rest -``` - -### 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 +export +cartProd : Foldable a => Foldable b => a e -> b f -> LazyList (e, f) +cartProd x y = + let y = foldToLazy y + in foldr (\e, acc => combine e y acc) [] x + where + foldToLazy : Foldable a' => a' e' -> LazyList e' + foldToLazy x = foldr (\e, acc => e :: acc) [] x + combine : e -> LazyList f -> LazyList (e, f) -> LazyList (e, f) + combine x [] rest = rest + combine x (y :: ys) rest = (x, y) :: combine x ys rest ``` diff --git a/src/Util/Digits.md b/src/Util/Digits.md deleted file mode 100644 index 6609c6c..0000000 --- a/src/Util/Digits.md +++ /dev/null @@ -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) -``` diff --git a/src/Util/Eff.md b/src/Util/Eff.md index 8441eb9..40517ea 100644 --- a/src/Util/Eff.md +++ b/src/Util/Eff.md @@ -6,7 +6,6 @@ Contains utility functions extending the functionality of the `eff` package. module Util.Eff import Control.Eff -import Data.Subset import Text.ANSI import System @@ -22,21 +21,12 @@ import System.File Basic enumeration describing log levels, we define some (hidden) utility 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 public export -data Level : Type where - Err : Level - Warn : Level - Info : Level - Debug : Level - Trace : Level - Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level +data Level = Err | Warn | Info | Debug | Trace | Other Nat ``` -```idris hide + Convert a `Level` into a colorized tag @@ -139,8 +129,10 @@ handleLoggerIO max_level x = else pure . ignore $ x ``` -Provide a family of effectful actions that emit log messages at the different -log levels. +Use the `WriterL "log" String` effect like a logging library. We'll provide a +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 export @@ -162,10 +154,6 @@ debug x = send $ Log Debug x export trace : Has Logger fs => Lazy String -> Eff fs () trace x = send $ Log Trace x - -export -logAt : Has Logger fs => Level -> Lazy String -> Eff fs () -logAt level x = send $ Log level x ``` ## Choose @@ -192,66 +180,3 @@ oneOfM : Has (Choose) fs => Foldable f => f (Eff fs a) -> Eff fs a 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 -``` diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index d4a3b19..d3be367 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -6,7 +6,7 @@ import Structures.Dependent.FreshList import Runner ``` -```idris hide + # Days @@ -79,42 +73,6 @@ y2015 = MkYear 2015 [ , 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 -``` - -## [Day 14](Y2015/Day14.md) - -```idris - , day14 -``` - ```idris ] ``` diff --git a/src/Years/Y2015/Day1.md b/src/Years/Y2015/Day1.md index 49369d9..cfc4950 100644 --- a/src/Years/Y2015/Day1.md +++ b/src/Years/Y2015/Day1.md @@ -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 except the effectful part computations. -```idris hide + ## Solver Functions @@ -76,8 +76,8 @@ part2 x = do pure $ findBasement 1 0 input ``` -```idris hide + diff --git a/src/Years/Y2015/Day10.md b/src/Years/Y2015/Day10.md deleted file mode 100644 index d07edf8..0000000 --- a/src/Years/Y2015/Day10.md +++ /dev/null @@ -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 -``` diff --git a/src/Years/Y2015/Day11.md b/src/Years/Y2015/Day11.md deleted file mode 100644 index 0feff8f..0000000 --- a/src/Years/Y2015/Day11.md +++ /dev/null @@ -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]: diff --git a/src/Years/Y2015/Day12.md b/src/Years/Y2015/Day12.md deleted file mode 100644 index 2829698..0000000 --- a/src/Years/Y2015/Day12.md +++ /dev/null @@ -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]: diff --git a/src/Years/Y2015/Day13.md b/src/Years/Y2015/Day13.md deleted file mode 100644 index e0f7f89..0000000 --- a/src/Years/Y2015/Day13.md +++ /dev/null @@ -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]: diff --git a/src/Years/Y2015/Day14.md b/src/Years/Y2015/Day14.md deleted file mode 100644 index 5418617..0000000 --- a/src/Years/Y2015/Day14.md +++ /dev/null @@ -1,173 +0,0 @@ -# [Year 2015 Day 14](https://adventofcode.com/2015/day/14) - -This day provides us an introduction to streams, infinite, lazily generated, -collections of data. - -```idris hide -module Years.Y2015.Day14 - -import Data.Primitives.Interpolation - -import Control.Eff - -import Runner -``` - -```idris -import Data.String -import Data.List1 -import Data.Vect -import Data.Stream -import Data.Zippable -import Decidable.Equality - -import Util -``` - -## Parsing And Datastructures - -Collect the aspects defining a reindeer into a record - -```idris -record Reindeer where - constructor MkReindeer - name : String - speed : Nat - duration, rest : Nat -``` - -```idris hide -Show Reindeer where - show (MkReindeer name speed duration rest) = - "MkReindeer \{name} \{speed} \{duration} \{rest}" -``` - -This time around, since the lines describing a reindeer contain a lot of cruft, -we'll handle the parsing by converting the input, after splitting it on space -characters, to a `Vect`, and indexing into that `Vect`. - -```idris -parseReindeer : Has (Except String) fs => - (input : String) -> Eff fs Reindeer -parseReindeer input = do - parts <- note "Input has wrong size: \{input}" $ - toVect 15 . forget . split (== ' ') . trim $ input - let name = index 0 parts - speed <- note "" $ - parsePositive $ index 3 parts - duration <- note "" $ - parsePositive $ index 6 parts - rest <- note "" $ - parsePositive $ index 13 parts - pure $ MkReindeer name speed duration rest -``` - -### Solver Functions - -A stream is an infinite analog of a list, storing an infinite collection of -(lazily generated) values. - -Streams are defined like: - -```idris -data Stream' : Type -> Type where - (::) : a -> Inf (Stream' a) -> Stream' a -``` - -Streams are a member of a family of concepts analogous to iterators in -imperative languages, the different flavors of colist. - -Colists are the codata duals of lists, we'll dig more into to this later, but to -provide a high level summary, where data is defined by how it is constructed, -codata is defined by how it is destructed. While a list is defined by how you -can cons an element `x` onto a list `xs` to produce a new list `x :: xs`, a -colist is defined by how you can break down a colist `x :: xs` into a head `x` -and a tail `xs`. - -Streams are a particular type of colist that has no empty case, breaking down a -`Stream` will always produce an element and another stream, resulting in streams -always being infinite in length. - -Destructing a `Stream` by pattern matching is semantically equivalent to calling -the `next` method on an iterator in a language like rust, it produces the -element at the head of a stream, and a new stream producing future elements. - -We will model are reindeer's future history of locations as a stream, with each -element being the position at the time given by the index into the stream, -generating it with a pair of mutually recursive functions. The `run` function -adds the speed to current position to produce the next one, and the `rest` -function doesn't modify the position whill still consuming a time step. - -```idris -distances : Reindeer -> Stream Nat -distances x = run x x.duration 0 - where - run : (deer : Reindeer) -> (left : Nat) -> (position : Nat) - -> Stream Nat - rest : (deer : Reindeer) -> (left : Nat) -> (position : Nat) - -> Stream Nat - run deer 0 position = rest deer deer.rest position - run deer (S k) position = position :: run deer k (position + deer.speed) - rest deer 0 position = run deer deer.duration position - rest deer (S k) position = position :: rest deer k position -``` - -Carry an accumulator containing the scores for each reindeer down the stream, at -each position, granting one point to each reindeer at the leader position after -the end of the second. - -```idris -leaderScoring : {n : _} -> Vect (S n) (Stream Nat) -> Stream (Vect (S n) Nat) -leaderScoring xs = leaderScoring' (replicate _ 0) xs - where - leaderScoring' : {n : _} -> (acc : Vect (S n) Nat) -> Vect (S n) (Stream Nat) - -> Stream (Vect (S n) Nat) - leaderScoring' acc xs = - let positions = map (head . tail) xs - leader_pos = maxBy compare 0 positions - points : Vect _ Nat = - map (\x => if x == leader_pos then 1 else 0) positions - in acc :: leaderScoring' (zipWith (+) acc points) (map tail xs) -``` - -## Part Functions - -### Part 1 - -Parse the input, generate the position `Stream`s for each reindeer, then index -the finish position in each stream. - -```idris -part1 : Eff (PartEff String) (Nat, ()) -part1 = do - lines <- map lines $ askAt "input" - reindeer <- traverse parseReindeer lines - debug $ show reindeer - let dists = map distances reindeer - let dists_end = map (index 2503) dists - let max = maxBy compare 0 dists_end - pure (max, ()) -``` - -Parse the input into a vect, and make sure it is not empty, then generate the -stream with the `leaderScoring` function and index into it. - -```idris -part2 : () -> Eff (PartEff String) Nat -part2 x = do - lines <- map lines $ askAt "input" - let (len ** lines) = listToVect lines - case len of - 0 => throw "No reindeer :(" - (S k) => do - reindeer <- traverse parseReindeer lines - let dists = leaderScoring $ map distances reindeer - let dists_end = index 2503 dists - pure $ maxBy compare 0 dists_end -``` - -```idris hide -public export -day14 : Day -day14 = Both 14 part1 part2 -``` diff --git a/src/Years/Y2015/Day2.md b/src/Years/Y2015/Day2.md index 9ab3ead..43ca0b1 100644 --- a/src/Years/Y2015/Day2.md +++ b/src/Years/Y2015/Day2.md @@ -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 -```idris hide + ```idris import Data.List @@ -16,9 +16,9 @@ import Data.List1 import Data.String ``` -```idris hide + ## Box structure @@ -130,8 +130,8 @@ part2 : (boxes : List Box) -> Eff (PartEff String) Integer part2 boxes = pure . sum . map totalRibbon $ boxes ``` -```idris hide + diff --git a/src/Years/Y2015/Day3.md b/src/Years/Y2015/Day3.md index daa922d..9dd7ecc 100644 --- a/src/Years/Y2015/Day3.md +++ b/src/Years/Y2015/Day3.md @@ -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 recursive functions. -```idris hide + ```idris import Data.SortedSet @@ -18,9 +18,9 @@ import Data.String import Util ``` -```idris hide + ## Parsing and data structures @@ -152,8 +152,8 @@ part2 movements = do pure . length $ locations ``` -```idris hide + diff --git a/src/Years/Y2015/Day4.md b/src/Years/Y2015/Day4.md index 78d0abe..a1fee57 100644 --- a/src/Years/Y2015/Day4.md +++ b/src/Years/Y2015/Day4.md @@ -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 `MD5` functionality. -```idris hide + ```idris import Data.String @@ -196,8 +196,8 @@ part2 seed = do pure number ``` -```idris hide + diff --git a/src/Years/Y2015/Day5.md b/src/Years/Y2015/Day5.md index d1b3ccb..d947885 100644 --- a/src/Years/Y2015/Day5.md +++ b/src/Years/Y2015/Day5.md @@ -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 [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) view, which lets us treat `String`s as if they were lazy lists or iterators. -```idris hide + ```idris import Data.String @@ -20,9 +20,9 @@ import Data.String import Util ``` -```idris hide + ## Nice Strings @@ -213,8 +213,8 @@ part2 _ = do pure x ``` -```idris hide + diff --git a/src/Years/Y2015/Day6.md b/src/Years/Y2015/Day6.md index c15596d..a2b5cd0 100644 --- a/src/Years/Y2015/Day6.md +++ b/src/Years/Y2015/Day6.md @@ -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 hide + ```idris import Util @@ -21,9 +19,9 @@ import Data.String import Data.IORef ``` -```idris hide + ## 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 ``` -```idris hide + 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 ``` -```idris hide + 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 ``` -```idris hide + ### Parsing @@ -334,8 +332,8 @@ part2 commands = do pure brightness ``` -```idris hide + diff --git a/src/Years/Y2015/Day7.md b/src/Years/Y2015/Day7.md index 9e663f6..5919288 100644 --- a/src/Years/Y2015/Day7.md +++ b/src/Years/Y2015/Day7.md @@ -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. @@ -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 outputting to a given wire is found in the input. -```idris hide + ```idris import Data.Bits @@ -31,9 +31,9 @@ import Data.SortedMap.Dependent import Decidable.Equality ``` -```idris hide + ## Parsing and data structures @@ -53,10 +53,7 @@ Input : Type Input = Either Literal 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`. +Description of a Gate, tagged in the type with the name of the output wire ```idris data Gate : Wire -> Type where @@ -252,8 +249,8 @@ part2 (circut, value) = do pure value ``` -```idris hide + diff --git a/src/Years/Y2015/Day8.md b/src/Years/Y2015/Day8.md index 621cae2..daed58e 100644 --- a/src/Years/Y2015/Day8.md +++ b/src/Years/Y2015/Day8.md @@ -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, -making use of state and non-determinism in our parsers. - -```idris hide + ```idris import Data.String import Data.Vect -import Data.List.Lazy import Data.Either ``` ## Parsing -A "Parser" is an effectful computation that has access to a list of chars as -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. +Effect alias for a parser ```idris -nextChar : Has (State (List Char)) fs => Has (Except String) fs => Eff fs Char -nextChar = do - c :: rest <- get - | [] => throw "End of input" - put rest - pure c +Parser : List (Type -> Type) +Parser = + [Choose, State (List Char), Except String] ``` -Attempt to parse a single character based on the supplied predicate, consuming -the character from the state and throwing the provided error if the predicate -does not hold over the consumed character. +Get the next character from the state, modifying it in place ```idris -char : Has (State (List Char)) fs => Has (Except String) fs => - (pred : Char -> Bool) -> (err : Char -> String) -> Eff fs Char -char pred err = do - c <- nextChar - unless (pred c) (throw $ err c) - pure c +getNext : Eff Parser Char +getNext = do + chars <- get + case chars of + [] => throw "End of Input" + (x :: xs) => do + put xs + pure x ``` -Type alias for a parser - +Parse a quote ```idris -Parser : (res : Type) -> Type -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 : Eff Parser () quote = do - _ <- char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`") - pure () + char <- getNext + 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 -normal : Parser Char -normal = - char - (\x => not $ any (== x) (the (List _) ['\\', '"'])) - (\x => "Expected normal, got `\{String.singleton x}`") +normal : Eff Parser Char +normal = do + char <- getNext + if any (char ==) (the (List _) ['\\', '"']) + then throw "Tried to parse a special character as normal \{show char}" + else pure char ``` -#### Escaped Characters - -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. +Parse a hex digit ```idris -eQuote : Parser Char -eQuote = do - _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") - char (== '"') (\x => "Expected `\"`, got `\{String.singleton x}`") +hexDigit : Eff Parser Int +hexDigit = do + char <- getNext + 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 -eSlash : Parser Char -eSlash = do - _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") - char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") +escaped : Eff Parser Char +escaped = do + escape <- getNext + 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 -fromHex : Char -> Int -fromHex c = - if ord c >= 97 - then ord c - 87 - else ord c - 48 +character : Eff Parser Char +character = oneOfM (the (List _) [escaped, normal]) ``` -Parse a character sequence `\xAB`, where `AB` are hexadecimal digits, and decode -the numerical value of `AB`, as a hexadecimal number, into its corresponding -character. +Run a parser until it runs out ```idris -eHex : Parser Char -eHex = do - _ <- char (== '\\') (\x => "Expected `\\`, got `\{String.singleton x}`") - _ <- char (== 'x') (\x => "Expected `x`, got `\{String.singleton x}`") - [x, y] <- map (map $ fromHex . toLower) . - sequence . - Vect.replicate 2 $ - (char - isHexDigit - (\x => "Expected hex digit, got `\{String.singleton x}`")) - pure . chr $ x * 0x10 + y +parseMany : Eff Parser t -> Eff Parser (List t) +parseMany x = do + Just next <- lift $ catch (\_ => pure Nothing) (map Just x) + | _ => pure [] + map (next ::) (parseMany x) ``` -Use the `oneOfM` combinator to combine our escaped character parsers into a -single character class. `oneOfM` uses the `Choice` effect to try all of the -provided parsers, conceptually in parallel, returning all of the results. +Parse any number of non-quote characters ```idris -escaped : Parser Char -escaped = oneOfM $ the (List _) [eQuote, eSlash, eHex] +characters : Eff Parser (List Char) +characters = parseMany character ``` -### Top Level Class - -Combine our `normal` and `escaped` parsers into a single parser for non-quote -characters. +Parse a quote delimited string ```idris -character : Parser Char -character = oneOfM $ the (List _) [normal, escaped] -``` - -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 +parseString : Eff Parser (List Char) +parseString = do quote - xs <- many character + xs <- characters quote - endOfInput pure xs ``` -### Running 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. +Run a parser ```idris -runParser : Has Logger fs => Parser (List Char) -> String - -> Eff fs $ Maybe String -runParser x str = do - info "Parsing: \{str}" - -- let outputs = - -- 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 +runParser : Eff Parser t -> String -> Maybe t +runParser m str = + map fst . head' . rights + . extract . runChoose {f = List} . runExcept . runState (unpack str) + $ m + ``` ## Part Functions ### 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 -part1 : Eff (PartEff String) (Int, List String) +part1 : Eff (PartEff String) (Nat, List (List Char, List Char)) part1 = do - inputs <- map lines $ askAt "input" - outputs <- traverse (runParser string) inputs - Just outputs <- pure $ sequence outputs - | _ => throw "Some strings failed to parse" - let difference = - sum $ zipWith (\x, y => strLength x - strLength y) inputs outputs - pure (difference, inputs) + inputs <- map (lines . trim) $ askAt "input" + let outputs = map (map pack . runParser parseString) inputs + let pairs = zip inputs outputs + let debug_out = joinBy "\n" . map show $ pairs + putStrLn debug_out + ?part1_rhs_1 ``` -### Part 2 - -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 + diff --git a/src/Years/Y2015/Day9.md b/src/Years/Y2015/Day9.md deleted file mode 100644 index d30a9b0..0000000 --- a/src/Years/Y2015/Day9.md +++ /dev/null @@ -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 -```