Year 2015 Day 12 Part 2

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:

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"

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,40 +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/'<style>' .* '</style>'//;
-    $output ~~ s:g/'<br />'//;
-    $output ~~ s:g/'\\*'/*/;
-    $output ~~ s:g/'\\_'/_/;
-    $output ~~ s:g/'\\\\'/\\/;
-    $output ~~ s:g/'<code'/<pre><code/;
-    $output ~~ s:g/'</code>'/<\/code><\/pre>/;
-    $output ~~ s:g/'class="IdrisKeyword"'/class="hljs-keyword"/;
-    $output ~~ s:g/'class="IdrisModule"'/class="hljs-symbol hljs-emphasis"/;
-    $output ~~ s:g/'class="IdrisComment"'/class="hljs-comment"/;
-    $output ~~ s:g/'class="IdrisFunction"'/class="hljs-symbol"/;
-    $output ~~ s:g/'class="IdrisBound"'/class="hljs-name"/;
-    $output ~~ s:g/'class="IdrisData"'/class="hljs-title"/;
-    $output ~~ s:g/'class="IdrisType"'/class="hljs-type"/;
-    $output ~~ s:g/'class="IdrisNamespace"'/class="hljs-symbol hljs-emphasis"/;
-
-    # Spurt the output to the temporary directory
-    my $output-path = $tempdir.add: $src;
-    if !$output-path.parent.d {
-        $output-path.parent.mkdir;
-    }
-    $output-path.spurt($output);
-}
+# 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";
-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(*.&not-ignored)) -> $path {
@@ -102,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/'<style>' .* '</style>'//;
+    $output ~~ s:g/'<br />'//;
+    $output ~~ s:g/'\\*'/*/;
+    $output ~~ s:g/'\\_'/_/;
+    $output ~~ s:g/'\\\\'/\\/;
+    $output ~~ s:g/'<code'/<pre><code/;
+    $output ~~ s:g/'</code>'/<\/code><\/pre>/;
+    $output ~~ s:g/'="IdrisKeyword"'/="hljs-keyword"/;
+    $output ~~ s:g/'="IdrisModule"'/="hljs-symbol hljs-emphasis"/;
+    $output ~~ s:g/'="IdrisComment"'/="hljs-comment"/;
+    $output ~~ s:g/'="IdrisFunction"'/="hljs-symbol"/;
+    $output ~~ s:g/'="IdrisBound"'/="hljs-name"/;
+    $output ~~ s:g/'="IdrisData"'/="hljs-title"/;
+    $output ~~ s:g/'="IdrisType"'/="hljs-type"/;
+    $output ~~ s:g/'="IdrisNamespace"'/="hljs-symbol hljs-emphasis"/;
+
+    # Spurt the output to the temporary directory
+    my $output-path = $tempdir.add: $src;
+    if !$output-path.parent.d {
+        $output-path.parent.mkdir;
+    }
+    $output-path.spurt($output);
+}

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"

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
 ```
 
@@ -55,6 +57,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 +72,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
@@ -82,6 +86,96 @@ 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,
@@ -168,6 +262,7 @@ object = do
     pairs = do
       first <- keyValue
       rest <- many restKeyValue
+      -- TODO: headTail combinator for this
       pure $ first ::: rest
     occupiedObject : Parser (JSONValue TObject)
     occupiedObject = do

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)

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
   ]
 ```

src/Years/Y2015/Day12.md

@@ -0,0 +1,132 @@
+# [Year 2015 Day 12](https://adventofcode.com/2015/day/12)
+
+This day provides an introduction to our new
+[`Parser.JSON`](../../Parser/JSON.md) module, as well as the use of `DList`s[^1]
+to collect values from an indexed type family into a single collection.
+
+```idris hide
+module Years.Y2015.Day12
+
+import Control.Eff
+
+import Runner
+```
+
+```idris
+import Structures.Dependent.DList
+
+import Parser
+import Parser.JSON
+```
+
+## Parsing
+
+Parse a list of JSON values into a `DList`.
+
+`JSONValue`'s type constructor has the signature `JSONType -> Type`, forming
+what is known as an "Indexed Type Family".
+
+Each type of JSON value has a separate type, e.g. a Bool has type
+`JSONValue TBool`, a String has type `JSONValue TString`, etc. While these are
+all separate types, they all share the `JSONValue` component of the type
+constructor, making them members of the same family.
+
+Despite being members of the same type family, they still have different types,
+so we can't just shove `JSONValue`s of different types into, say, a
+`List JSONValue`, we need a collection with some amount of heterogeneity. While
+a `List (type : JSONType ** JSONValue type)` would _work_, that introduces
+various ergonomic headaches, so instead we return a `DList`[^1], a `List` like
+data structure specifically designed for collecting values from an indexed typed
+family into a single collection.
+
+The parsing logic is otherwise quite simple, we use the `many` combinator to
+turn the `value` parser, which parses a single JSON value, into one that parses
+a list of JSON values, and then use `DList`'s `fromList` method to collect the
+results into a `DList`.
+
+```idris
+parseJsons : Has (Except String) fs => Has IO fs => (input : String)
+  -> Eff fs (types : List JSONType ** DList JSONType JSONValue types) 
+parseJsons input = do
+  result <- runFirstIO (many value) input
+  case result of
+    Left err => throw $ show err
+    Right result => pure $ fromList result
+```
+
+## Solving
+
+A reducer for `DList.dFoldL` that sums all the numbers within the contained JSON
+Value.
+
+The outer function is meant to be called on a top level object, using
+`DList.dFoldL` on a `DList` of `JSONValue`s, where as the inner function
+directly reduces a `JSONValue` using `JSON.dFoldL`.
+
+```idris
+sumNumbers : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+sumNumbers dbl type value = dFoldL sumNumbers' dbl value
+  where
+    sumNumbers' : Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+    sumNumbers' dbl TNumber (VNumber d) = dbl + d
+    sumNumbers' dbl _ value = dbl
+```
+
+Filter out objects containing a "red" key
+
+```idris
+noRed  : (type : JSONType) -> (value : JSONValue type) -> Bool
+noRed TObject value = 
+  let (types ** vals) = getValues value
+  in case dFind (\t, v => 
+                  case t of
+                    TString => v == (VString "red")
+                    _ => False
+                ) vals of
+    Nothing => True
+    Just _ => False
+noRed _ value = True
+
+sumNumbersNoRed : 
+  Double -> (type : JSONType) -> (value : JSONValue type) -> Double
+sumNumbersNoRed dbl type value = 
+  case dFilter noRed value of
+    Nothing => dbl
+    Just value => sumNumbers dbl type value
+```
+
+## Part Functions
+
+### Part 1
+
+Parse our JSONs, then fold our `sumNumbers` reducer over them.
+
+```idris
+part1 : Eff (PartEff String) 
+            (Double, (types : List JSONType ** DList JSONType JSONValue types))
+part1 = do
+  input <- askAt "input"
+  (types ** values) <- parseJsons input
+  let result = dFoldL sumNumbers 0.0 values
+  pure (result, (types ** values))
+```
+
+### Part 2
+
+```idris
+part2 : (types : List JSONType ** DList JSONType JSONValue types)
+  -> Eff (PartEff String) Double
+part2 (types ** values) = do
+  let result = dFoldL sumNumbersNoRed 0.0 values
+  pure result
+```
+
+```idris hide
+public export
+day12 : Day
+day12 = Both 12 part1 part2
+```
+
+## References
+
+[^1]: <https://git.sr.ht/~thatonelutenist/Structures/tree/trunk/item/src/Structures/Dependent/DList.md>