diff --git a/README.md b/README.md index 731d675..1598931 100644 --- a/README.md +++ b/README.md @@ -128,10 +128,6 @@ solution. Introduces refinement types - - [Day 12](src/Years/Y2015/Day12.md) - - New Parser Effect stack and DLists - ## References [^1]: Idris 2 Manual: diff --git a/book.toml b/book.toml index a4387d0..4ad1625 100644 --- a/book.toml +++ b/book.toml @@ -7,7 +7,7 @@ title = "Idris 2 by Highly Contrived Example" [build] create-missing = false -# use-default-preprocessors = false +use-default-preprocessors = false [output.html] preferred-dark-theme = "ayu" diff --git a/scripts/build-book b/scripts/build-book index 62af9b9..8513e4d 100755 --- a/scripts/build-book +++ b/scripts/build-book @@ -23,7 +23,7 @@ sub not-ignored($path) { # Copy a file from the current directory to the temporary directory, preserving # realtive path. Resolves symlinks in source, but does not reflect symlink # resoultion in the output path -sub copy-to-dest($src) { +sub cp-temp($src) { my $src-path = do given $src { when Str { $src.IO @@ -45,16 +45,40 @@ sub copy-to-dest($src) { $src-path.resolve.copy: $output-path; } -# Special handling for our readme file, we need to butcher up it's links -my $readme-contents = 'README.md'.IO.slurp; -$readme-contents ~~ s:g/'src/'//; -my $readme-dest = $tempdir.add('src/README.md'); -$readme-dest.parent.mkdir; -$readme-dest.spurt: $readme-contents; +# Invoke katla on a source file, streaming its output to the temporary directory +sub katla($src, $ttc-src) { + # Run katla and collect the output + my $katla = run 'katla', 'markdown', $src, $ttc-src, :out; + my $output = $katla.out.slurp(:close); + # TODO: Post process them to set themeing correctly + $output ~~ s:g/''//; + $output ~~ s:g/'
'//; + $output ~~ s:g/'\\*'/*/; + $output ~~ s:g/'\\_'/_/; + $output ~~ s:g/'\\\\'/\\/; + $output ~~ s:g/''/<\/code><\/pre>/; + $output ~~ s:g/'class="IdrisKeyword"'/class="hljs-keyword"/; + $output ~~ s:g/'class="IdrisModule"'/class="hljs-symbol hljs-emphasis"/; + $output ~~ s:g/'class="IdrisComment"'/class="hljs-comment"/; + $output ~~ s:g/'class="IdrisFunction"'/class="hljs-symbol"/; + $output ~~ s:g/'class="IdrisBound"'/class="hljs-name"/; + $output ~~ s:g/'class="IdrisData"'/class="hljs-title"/; + $output ~~ s:g/'class="IdrisType"'/class="hljs-type"/; + $output ~~ s:g/'class="IdrisNamespace"'/class="hljs-symbol hljs-emphasis"/; + + # Spurt the output to the temporary directory + my $output-path = $tempdir.add: $src; + if !$output-path.parent.d { + $output-path.parent.mkdir; + } + $output-path.spurt($output); +} # Copy our metadata files -copy-to-dest "book.toml"; -copy-to-dest "src/SUMMARY.md"; +cp-temp "book.toml"; +cp-temp "src/README.md"; +cp-temp "src/SUMMARY.md"; # Katla over the source files for paths("src", :file(*.¬-ignored)) -> $path { @@ -78,38 +102,3 @@ if $upload { '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/Parser/Interface.md b/src/Parser/Interface.md index 53be055..79583cf 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -110,8 +110,7 @@ Provide wrappers for `rundownFirst` for evaluating it in various contexts. ```idris export -runFirstIO : HasIO io => MonadRec io => - (f : Parser a) -> String -> io (Either ParseError a) +runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a) runFirstIO f str = do Just state <- newInternalIO str | _ => pure . Left $ BeforeParse "Empty input" diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 7baf9fa..6602210 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -6,8 +6,6 @@ module Parser.JSON import public Parser import public Parser.Numbers -import Control.Monad.Eval - import Structures.Dependent.DList ``` @@ -57,7 +55,6 @@ data JSONValue : JSONType -> Type where ``` ```idris hide -export Show (JSONValue t) where show (VObject xs) = let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs @@ -72,7 +69,6 @@ Show (JSONValue t) where show VNull = "null" -- TODO: Deal with keys potentially having different orders in different objects -export Eq (JSONValue t) where (VObject xs) == (VObject ys) = assert_total $ xs $== ys @@ -86,96 +82,6 @@ Eq (JSONValue t) where %hide Language.Reflection.TT.WithFC.value ``` -### JSON Functions - -`foldl` Analog for consuming a JSON structure by values. Ignores the keys in -objects. - -```idris -export -dFoldL : {t : JSONType} - -> (acc -> (type : JSONType) -> (val : JSONValue type) -> acc) - -> acc -> JSONValue t -> acc -dFoldL f acc' (VObject xs) = - let recur : acc -> (v : JSONType) -> (String, JSONValue v) -> acc - recur acc' v (key, value) = dFoldL f acc' value - in DList.dFoldL recur acc' xs -dFoldL f acc' (VArray xs) = - let recur : acc -> (v : JSONType) -> JSONValue v -> acc - recur acc' v value = dFoldL f acc' value - in DList.dFoldL recur acc' xs -dFoldL f acc (VString s) = f acc _ (VString s) -dFoldL f acc (VNumber d) = f acc _ (VNumber d) -dFoldL f acc (VBool b) = f acc _ (VBool b) -dFoldL f acc VNull = f acc _ VNull -``` - -Look up a property in an object - -```idris -export -getProperty : (prop : String) -> (object : JSONValue TObject) - -> Maybe (type : JSONType ** JSONValue type) -getProperty prop (VObject xs) = - case dFind (\_, (key, _) => key == prop) xs of - Nothing => Nothing - Just (type ** (_, val)) => Just (type ** val) -``` - -Return the values from an object. - -```idris -export -getValues : (object : JSONValue TObject) - -> (types : List JSONType ** DList JSONType JSONValue types) -getValues (VObject xs) = - dMap' (\t, (k, v) => (t ** v)) xs -``` - -Recursively apply a filter to a JSON structure. - -```idris -export -dFilter : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) - -> {t : JSONType} -> JSONValue t -> Maybe (JSONValue t) -dFilter f value = eval $ dFilter' f value - where - dFilter' : (f : (type : JSONType) -> (val : JSONValue type) -> Bool) - -> {t : JSONType} -> JSONValue t -> Eval $ Maybe (JSONValue t) - dFilter' f (VObject xs) = do - True <- pure $ f _ (VObject xs) - | _ => pure Nothing - let xs = toList xs - xs : List (Maybe (x : JSONType ** (String, JSONValue x))) <- - traverse - (\(t ** (k, v)) => do - Just v <- dFilter' f v - | _ => pure Nothing - pure $ Just (t ** (k, v))) - xs - let (_ ** xs) : (t : List JSONType ** DList _ _ t) = - fromList $ catMaybes xs - pure . Just $ VObject xs - dFilter' f (VArray xs) = do - True <- pure $ f _ (VArray xs) - | _ => pure Nothing - let xs = toList xs - xs : List (Maybe (x : JSONType ** JSONValue x)) <- - traverse - (\(t ** v) => do - Just v <- dFilter' f v - | _ => pure Nothing - pure $ Just (t ** v)) - xs - let (_ ** xs) : (t : List JSONType ** DList _ _ t) = - fromList $ catMaybes xs - pure . Just $ VArray xs - dFilter' f x = - pure $ case f _ x of - False => Nothing - True => Just x -``` - ## Parsers We are going to get mutually recursive here. Instead of using a `mutual` block, @@ -262,7 +168,6 @@ object = do pairs = do first <- keyValue rest <- many restKeyValue - -- TODO: headTail combinator for this pure $ first ::: rest occupiedObject : Parser (JSONValue TObject) occupiedObject = do diff --git a/src/SUMMARY.md b/src/SUMMARY.md index f0b09eb..2cf1e0b 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -33,4 +33,3 @@ - [Day 9 - Naive Graph Traversal](Years/Y2015/Day9.md) - [Day 10 - Digits View](Years/Y2015/Day10.md) - [Day 11 - Refinement Types](Years/Y2015/Day11.md) - - [Day 12 - Custom Parser Effect and DLists](Years/Y2015/Day12.md) diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 8f94f4f..c2a0326 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -18,7 +18,6 @@ import Years.Y2015.Day8 import Years.Y2015.Day9 import Years.Y2015.Day10 import Years.Y2015.Day11 -import Years.Y2015.Day12 ``` # Days @@ -95,12 +94,6 @@ y2015 = MkYear 2015 [ , day11 ``` -## [Day 12](Y2015/Day12.md) - -```idris - , day12 -``` - ```idris ] ``` 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]: