From aa33fe6004ad6d9ca18f4c37e11a3ee20c39d86a Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 17:06:08 -0500 Subject: [PATCH 01/10] Some notes --- book.toml | 2 +- scripts/build-book | 2 ++ src/Parser/JSON.md | 1 + 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/book.toml b/book.toml index 4ad1625..a4387d0 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 8513e4d..f1d8b7b 100755 --- a/scripts/build-book +++ b/scripts/build-book @@ -77,6 +77,8 @@ sub katla($src, $ttc-src) { # Copy our metadata files cp-temp "book.toml"; +# TODO: Special Handling for the README so we don't need the symlink and the +# links work cp-temp "src/README.md"; cp-temp "src/SUMMARY.md"; diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 6602210..7699d29 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -168,6 +168,7 @@ object = do pairs = do first <- keyValue rest <- many restKeyValue + -- TODO: headTail combinator for this pure $ first ::: rest occupiedObject : Parser (JSONValue TObject) occupiedObject = do From 83afb8a7c41fcebe899d41aa2c1594caa1946839 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 18:30:30 -0500 Subject: [PATCH 02/10] Add JSON dFoldL --- src/Parser/JSON.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 7699d29..b69db49 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -82,6 +82,30 @@ 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 +``` + ## Parsers We are going to get mutually recursive here. Instead of using a `mutual` block, From 6afe8c2a4e3ee28ebd923059d55dffafa7bbcc90 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 19:55:35 -0500 Subject: [PATCH 03/10] Make runFirstIO more generic --- src/Parser/Interface.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md index 79583cf..53be055 100644 --- a/src/Parser/Interface.md +++ b/src/Parser/Interface.md @@ -110,7 +110,8 @@ Provide wrappers for `rundownFirst` for evaluating it in various contexts. ```idris export -runFirstIO : (f : Parser a) -> String -> IO (Either ParseError a) +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" From cd4949b2f8cefcfed4eee0579b357bb5bbeae93f Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 20:15:04 -0500 Subject: [PATCH 04/10] Export JSON show and Eq --- src/Parser/JSON.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index b69db49..60386ef 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -55,6 +55,7 @@ data JSONValue : JSONType -> Type where ``` ```idris hide +export Show (JSONValue t) where show (VObject xs) = let xs = dMap (\_,(key, value) => "\"\{key}\":\{show value}") xs @@ -69,6 +70,7 @@ 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 From e00ec274ca2a8c0cbcafebae421aaf41e086641d Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 19:47:47 -0500 Subject: [PATCH 05/10] Year 2015 Day 12 Part 1 --- README.md | 4 ++ src/SUMMARY.md | 1 + src/Years/Y2015.md | 7 +++ src/Years/Y2015/Day12.md | 99 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 111 insertions(+) create mode 100644 src/Years/Y2015/Day12.md diff --git a/README.md b/README.md index 1598931..731d675 100644 --- a/README.md +++ b/README.md @@ -128,6 +128,10 @@ 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/src/SUMMARY.md b/src/SUMMARY.md index 2cf1e0b..f0b09eb 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -33,3 +33,4 @@ - [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 c2a0326..8f94f4f 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -18,6 +18,7 @@ import Years.Y2015.Day8 import Years.Y2015.Day9 import Years.Y2015.Day10 import Years.Y2015.Day11 +import Years.Y2015.Day12 ``` # Days @@ -94,6 +95,12 @@ 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 new file mode 100644 index 0000000..92ce6dc --- /dev/null +++ b/src/Years/Y2015/Day12.md @@ -0,0 +1,99 @@ +# [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 +``` + +## Part Functions + +### Day 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)) +``` + +```idris hide +public export +day12 : Day +day12 = First 12 part1 +``` + +## References + +[^1]: From e91db14c115b21a31ba0a26a53ff372793036cbb Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 21:02:07 -0500 Subject: [PATCH 06/10] Improve build-book script --- scripts/build-book | 79 ++++++++++++++++++++++++++-------------------- 1 file changed, 44 insertions(+), 35 deletions(-) diff --git a/scripts/build-book b/scripts/build-book index f1d8b7b..62af9b9 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 cp-temp($src) { +sub copy-to-dest($src) { my $src-path = do given $src { when Str { $src.IO @@ -45,42 +45,16 @@ sub cp-temp($src) { $src-path.resolve.copy: $output-path; } -# 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); -} +# 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 -cp-temp "book.toml"; -# TODO: Special Handling for the README so we don't need the symlink and the -# links work -cp-temp "src/README.md"; -cp-temp "src/SUMMARY.md"; +copy-to-dest "book.toml"; +copy-to-dest "src/SUMMARY.md"; # Katla over the source files for paths("src", :file(*.¬-ignored)) -> $path { @@ -104,3 +78,38 @@ 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); +} From b5547ccb58307f820f456024b737ee7a1bc3e236 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 21:26:47 -0500 Subject: [PATCH 07/10] Add getProperty method to JSON --- src/Parser/JSON.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 60386ef..35f6312 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -108,6 +108,18 @@ 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) +``` + ## Parsers We are going to get mutually recursive here. Instead of using a `mutual` block, From 5760da96eb71876ef1dc4a416fd1a22f67badb6f Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 22:25:12 -0500 Subject: [PATCH 08/10] Add dFilter to json --- src/Parser/JSON.md | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 35f6312..c71d95c 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -6,6 +6,8 @@ module Parser.JSON import public Parser import public Parser.Numbers +import Control.Monad.Eval + import Structures.Dependent.DList ``` @@ -120,6 +122,50 @@ getProperty prop (VObject xs) = Just (type ** (_, val)) => Just (type ** val) ``` +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, From b2704dcbcc3a303e3224b7fffc242c1d595825d5 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 22:45:18 -0500 Subject: [PATCH 09/10] Add getValues to JSON --- src/Parser/JSON.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index c71d95c..7baf9fa 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -122,6 +122,16 @@ getProperty prop (VObject xs) = 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 From c632ab023dec68d9206f8a7dd1e18b73ef99b315 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 23:00:02 -0500 Subject: [PATCH 10/10] Year 2015 Day 12 Part 2 --- src/Years/Y2015/Day12.md | 37 +++++++++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) diff --git a/src/Years/Y2015/Day12.md b/src/Years/Y2015/Day12.md index 92ce6dc..2829698 100644 --- a/src/Years/Y2015/Day12.md +++ b/src/Years/Y2015/Day12.md @@ -72,9 +72,32 @@ sumNumbers dbl type value = dFoldL sumNumbers' dbl value 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 -### Day 1 +### Part 1 Parse our JSONs, then fold our `sumNumbers` reducer over them. @@ -88,10 +111,20 @@ part1 = do 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 = First 12 part1 +day12 = Both 12 part1 part2 ``` ## References