Mdbook tweaks

.gitignore

@@ -4,3 +4,5 @@ inputs/
 support/*.o
 support/advent-support
 tmp/
+book/
+index.html

README.md

@@ -6,6 +6,9 @@ Idris files.
 
 ## Authors Note
 
+This entire book is a single literate code base, the source code is available at
+<https://git.stranger.systems/Idris/advent>.
+
 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.
@@ -22,7 +25,7 @@ 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:
-https://git.stranger.systems/Idris/advent.rss
+<https://git.stranger.systems/Idris/advent.rss>.
 
 ## Index of non-day modules
 
@@ -56,6 +59,26 @@ solution.
   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
 
 - 2015

advent.ipkg

@@ -19,6 +19,7 @@ depends = base
         , tailrec
         , eff
         , elab-util
+        , sop
         , ansi
         , if-unsolved-implicit
         , c-ffi
@@ -30,6 +31,10 @@ modules = Runner
         , Util.Eff
         , Util.Digits
         , Array
+        , Parser
+        , Parser.Interface
+        , Parser.Numbers
+        , Parser.JSON
 
 -- main file (i.e. file to load at REPL)
 main = Main

book.toml

@@ -0,0 +1,13 @@
+[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"

scripts/build-book

@@ -0,0 +1,101 @@
+#!/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 cp-temp($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;
+}
+
+# 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/'<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);
+}
+
+# Copy our metadata files
+cp-temp "book.toml";
+cp-temp "src/README.md";
+cp-temp "src/SUMMARY.md";
+
+# Katla over the source files
+for paths("src", :file(*.&not-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 <mdbook build>;
+    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;
+}

src/Array.md

@@ -12,9 +12,9 @@ import Decidable.Equality
 import Control.WellFounded
 ```
 
-<!-- idris
+```idris hide
 import System
--->
+```
 
 ```idris
 %default total
@@ -89,9 +89,9 @@ Iterable (LazyList a) a where
 
 ## Immutable arrays
 
-<!-- idris
+```idris hide
 namespace Immutable
--->
+```
 
 Immutable arrays created from vectors that provide constant time indexing and
 slicing operations.

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
+```idris hide
 Show Error where
   show (OptionsError errs) =
     let errs = unlines . map ("  " ++) . lines . joinBy "\n" $ errs
@@ -98,7 +98,7 @@ Show Error where
   show (SolveError year day part err) =
     let err = unlines . map ("  " ++) . lines . show $ err
     in "Error solving day \{show day} part \{show part} of year \{show year}: \n" ++ err
--->
+```
 
 ## Extract the year and day
 

src/Parser.md

@@ -0,0 +1,8 @@
+# Parsing Utilties
+
+```idris
+module Parser
+
+import public Parser.Interface as Parser
+import public Parser.ParserState as Parser
+```

src/Parser/Interface.md

@@ -0,0 +1,332 @@
+# 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 : (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 
+```

src/Parser/JSON.md

@@ -0,0 +1,285 @@
+# JSON Parser
+
+```idris
+module Parser.JSON
+
+import public Parser
+import public Parser.Numbers
+
+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
+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
+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
+```
+
+## 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
+      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
+```

src/Parser/Numbers.md

@@ -0,0 +1,257 @@
+# 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") 
+```

src/Parser/ParserState.md

@@ -0,0 +1,369 @@
+# 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]: <https://github.com/stefan-hoeck/idris2-barbies>

src/README.md

@@ -0,0 +1 @@
+../README.md

src/SUMMARY.md

@@ -0,0 +1,35 @@
+# 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)

src/Util.md

@@ -29,9 +29,9 @@ repeatN (S times') f seed = repeatN times' f (f seed)
 
 ## Either
 
-<!-- idris
+```idris hide
 namespace Either
--->
+```
 
 ### mapLeft
 
@@ -47,9 +47,9 @@ Applies a function to the contents of a `Left` if the value of the given
 
 ## List
 
-<!-- idris 
+```idris hide
 namespace List
--->
+```
 
 ### contains
 
@@ -94,12 +94,12 @@ Define some operations for pairs of numbers, treating them roughly like vectors
 
 ### Addition and Subtraction
 
-<!-- idris
+```idris hide
 export infixl 8 >+<
 export infixl 8 >-<
 
 namespace Pair
--->
+```
 
 ```idris
   public export
@@ -115,9 +115,9 @@ namespace Pair
 
 Extend `Data.SortedSet`
 
-<!-- idris
+```idris hide
 namespace Set
--->
+```
 
 ### length
 
@@ -133,9 +133,9 @@ Count the number of elements in a sorted set
 
 Extend `Data.String`
 
-<!-- idris
+```idris hide
 namespace String
--->
+```
 
 ### isSubstr
 

src/Util/Digits.md

@@ -6,11 +6,11 @@ module Util.Digits
 import Data.Monoid.Exponentiation
 ```
 
-<!-- idris
+```idris hide
 import System
 
 %default total
--->
+```
 
 This module provides views and associated functionality for treating `Integers`
 as if they were lists of numbers.
@@ -22,10 +22,10 @@ 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
+```idris hide
 -- This mutual block isn't strictly required, but is useful for literate purposes
 mutual
--->
+```
 
 ## Primitive functionality
 
@@ -50,14 +50,14 @@ most significant digit.
 
 For a clarifying example:
 
-<!-- idris
+```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]
@@ -121,14 +121,14 @@ least significant digit.
 
 For a clarifying example:
 
-<!-- idris
+```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]

src/Util/Eff.md

@@ -36,7 +36,7 @@ data Level : Type where
   Other : (n : Nat) -> {auto _ : n `GT` 4} -> Level
 ```
 
-<!-- idris
+```idris hide
 export
 levelToNat : Level -> Nat
 levelToNat Err = 0
@@ -67,7 +67,7 @@ export infixl 8 >+
 export
 (>+) : Level -> Nat -> Level
 (>+) x k = natToLevel (k + levelToNat x)
--->
+```
 
 Convert a `Level` into a colorized tag
 

src/Years/Y2015.md

@@ -6,7 +6,7 @@ import Structures.Dependent.FreshList
 import Runner
 ```
 
-<!-- idris
+```idris hide
 import Years.Y2015.Day1
 import Years.Y2015.Day2
 import Years.Y2015.Day3
@@ -18,7 +18,7 @@ import Years.Y2015.Day8
 import Years.Y2015.Day9
 import Years.Y2015.Day10
 import Years.Y2015.Day11
--->
+```
 
 # Days
 

src/Years/Y2015/Day1.md

@@ -3,7 +3,7 @@
 Pretty simple, basic warmup problem, nothing really novel is on display here
 except the effectful part computations.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day1
 
 import Control.Eff
@@ -11,7 +11,7 @@ import Control.Eff
 import Runner
 
 %default total
--->
+```
 
 ## Solver Functions
 
@@ -76,8 +76,8 @@ part2 x = do
   pure $ findBasement 1 0 input
 ```
 
-<!-- idris
+```idris hide
 public export
 day1 : Day
 day1 = Both 1 part1 part2
--->
+```

src/Years/Y2015/Day10.md

@@ -3,13 +3,13 @@
 This day doesn't really add anything new, but we will show off our new views for
 viewing integers as lists of digits.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day10
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -22,9 +22,9 @@ import Util
 import Util.Digits
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 # Solver Functions
 
@@ -118,8 +118,8 @@ part2 digits = do
   pure $ count (const True) output
 ```
 
-<!-- idris
+```idris hide
 public export
 day10 : Day
 day10 = Both 10 part1 part2
--->
+```

src/Years/Y2015/Day11.md

@@ -10,13 +10,13 @@ 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 
+```idris hide
 module Years.Y2015.Day11
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.Vect
@@ -55,13 +55,13 @@ record PasswordChar where
 %name PasswordChar pc
 ```
 
-<!-- idris
+```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,
@@ -227,12 +227,12 @@ part2 password = do
   pure $ passwordToString next_password
 ```
 
-<!-- idris
+```idris hide
 public export
 day11 : Day
 day11 = Both 11 part1 part2
--->
+```
 
 ## References
 
-[^1]: https://github.com/stefan-hoeck/idris2-refined/
+[^1]: <https://github.com/stefan-hoeck/idris2-refined/>

src/Years/Y2015/Day2.md

@@ -2,13 +2,13 @@
 
 This day provides us our first little taste of effectful parsing
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day2
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.List
@@ -16,9 +16,9 @@ import Data.List1
 import Data.String
 ```
 
-<!-- idris 
+```idris hide
 %default total
--->
+```
 
 ## Box structure
 
@@ -130,8 +130,8 @@ part2 : (boxes : List Box) -> Eff (PartEff String) Integer
 part2 boxes = pure . sum . map totalRibbon $ boxes
 ```
 
-<!-- idris
+```idris hide
 public export
 day2 : Day
 day2 = Both 2 part1 part2
--->
+```

src/Years/Y2015/Day3.md

@@ -3,13 +3,13 @@
 This day provides a gentle introduction to `mutual` blocks and mutually
 recursive functions.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day3
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.SortedSet
@@ -18,9 +18,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -152,8 +152,8 @@ part2 movements = do
   pure . length $ locations
 ```
 
-<!-- idris
+```idris hide
 public export
 day3 : Day
 day3 = Both 3 part1 part2
--->
+```

src/Years/Y2015/Day4.md

@@ -3,13 +3,13 @@
 This day introduces us to a little bit of FFI, linking to openssl to use it's
 `MD5` functionality.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day4
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -196,8 +196,8 @@ part2 seed = do
   pure number
 ```
 
-<!-- idris
+```idris hide
 public export
 day4 : Day
 day4 = Both 4 part1 part2
--->
+```

src/Years/Y2015/Day5.md

@@ -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
+```idris hide
 module Years.Y2015.Day5
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -20,9 +20,9 @@ import Data.String
 import Util
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Nice Strings
 
@@ -213,8 +213,8 @@ part2 _ = do
   pure x
 ```
 
-<!-- idris
+```idris hide
 public export
 day5 : Day
 day5 = Both 5 part1 part2
--->
+```

src/Years/Y2015/Day6.md

@@ -1,16 +1,14 @@
-# \[Year 2015 Day 6\](https://adventofcode.com/2015/day/
-
-6.
+# [Year 2015 Day 6](https://adventofcode.com/2015/day/6)
 
 Introduction to the advent of code classic 2d grid problem.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day6
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Util
@@ -23,9 +21,9 @@ import Data.String
 import Data.IORef
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -77,12 +75,12 @@ The three types of action that can be performed on a light.
 data Action = On | Off | Toggle
 ```
 
-<!-- idris
+```idris hide
 Show Action where
   show On = "on"
   show Off = "off"
   show Toggle = "toggle"
--->
+```
 
 The range of coordinates that a command affects
 
@@ -92,11 +90,11 @@ record Range (rows, cols : Nat) where
   top_left, bottom_right : Coord rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Range rows cols) where
   show (MkRange top_left bottom_right) = 
     "\{show top_left} -> \{show bottom_right}"
--->
+```
 
 Helper function to extract a range of values from our Grid.
 
@@ -121,11 +119,11 @@ record Command (rows, cols : Nat) where
   range : Range rows cols
 ```
 
-<!-- idris
+```idris hide
 Show (Command rows cols) where
   show (MkCmd action range) = 
     "{\{show action}: \{show range}}"
--->
+```
 
 ### Parsing
 
@@ -336,8 +334,8 @@ part2 commands = do
   pure brightness
 ```
 
-<!-- idris
+```idris hide
 public export
 day6 : Day
 day6 = Both 6 part1 part2
--->
+```

src/Years/Y2015/Day7.md

@@ -1,6 +1,4 @@
-# \[Year 2015 Day 7\](https://adventofcode.com/2015/day/
-
-7.
+# [Year 2015 Day 7](https://adventofcode.com/2015/day/7)
 
 This day provides us a gentle introduction to dependent maps.
 
@@ -15,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
+```idris hide
 module Years.Y2015.Day7
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.Bits
@@ -33,9 +31,9 @@ import Data.SortedMap.Dependent
 import Decidable.Equality
 ```
 
-<!-- idris
+```idris hide
 %default total
--->
+```
 
 ## Parsing and data structures
 
@@ -254,8 +252,8 @@ part2 (circut, value) = do
   pure value
 ```
 
-<!-- idris
+```idris hide
 public export covering
 day7 : Day
 day7 = Both 7 part1 part2
--->
+```

src/Years/Y2015/Day8.md

@@ -3,7 +3,7 @@
 This day provides a more in depth introduction to writing effectful parsers,
 making use of state and non-determinism in our parsers.
 
-<!-- idris
+```idris hide
 module Years.Y2015.Day8
 
 import Control.Eff
@@ -11,7 +11,7 @@ import Control.Eff
 import Data.Primitives.Interpolation
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -344,8 +344,8 @@ part2 inputs = do
   pure difference
 ```
 
-<!-- idris
+```idris hide
 public export
 day8 : Day
 day8 = Both 8 part1 part2
--->
+```

src/Years/Y2015/Day9.md

@@ -6,13 +6,13 @@ 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
+```idris hide
 module Years.Y2015.Day9
 
 import Control.Eff
 
 import Runner
--->
+```
 
 ```idris
 import Data.String
@@ -70,10 +70,10 @@ DistanceMap : Type
 DistanceMap = SortedMap Location (List LP)
 ```
 
-<!-- idris
+```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.
 
@@ -287,8 +287,8 @@ part2 (distance_map, pairs) = do
   pure len
 ```
 
-<!-- idris
+```idris hide
 public export
 day9 : Day
 day9 = Both 9 part1 part2
--->
+```