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