From 0f6da0b95254d8da7b5e1d5fa55dbb70b9751aca Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 16:33:29 -0500
Subject: [PATCH 01/29] numbers: Create numbers module

---
 README.md             | 4 ++++
 advent.ipkg           | 1 +
 src/Parser/Numbers.md | 5 +++++
 3 files changed, 10 insertions(+)
 create mode 100644 src/Parser/Numbers.md

diff --git a/README.md b/README.md
index 52d86cd..dc78c7c 100644
--- a/README.md
+++ b/README.md
@@ -68,6 +68,10 @@ solution.
 
     Internal state of a parser
 
+  - [ParserState](src/Parser/ParserState.md)
+
+    Parsers for numerical values in multiple bases
+
 ## Index of years and days
 
 - 2015
diff --git a/advent.ipkg b/advent.ipkg
index 56f6e75..e8aff07 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -32,6 +32,7 @@ modules = Runner
         , Array
         , Parser
         , Parser.Interface
+        , Parser.Numbers
 
 -- main file (i.e. file to load at REPL)
 main = Main
diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
new file mode 100644
index 0000000..29e6ece
--- /dev/null
+++ b/src/Parser/Numbers.md
@@ -0,0 +1,5 @@
+# Numerical Parsers
+
+```idris
+module Parser.Numbers
+```

From c3a28d469e600b011f8648e97b38a60f94832c63 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 17:54:21 -0500
Subject: [PATCH 02/29] numbers: Basic module structure

---
 src/Parser/Numbers.md | 69 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 29e6ece..aa0e156 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -2,4 +2,73 @@
 
 ```idris
 module Parser.Numbers
+  
+import public Parser
+
+import Data.Vect
+import Control.Eff
+```
+
+## 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 : Parser Nat
+```
+
+## 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 => ?show_err
+  putStrLn "Input: \{string} Output: \{show result}"
+  pure $ x == result
 ```

From dd0c642cd002547f571fda11e82677bc27777d40 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 18:09:20 -0500
Subject: [PATCH 03/29] numbers: Nat unit tests

---
 src/Parser/Numbers.md | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index aa0e156..195570f 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -51,7 +51,11 @@ hex = MkBase 16
 
 ```idris
 export
-nat : Parser Nat
+nat : Base -> Parser Nat
+
+export
+natBase10 : Parser Nat
+natBase10 = nat base10
 ```
 
 ## Unit tests
@@ -68,7 +72,24 @@ roundtrip x p = do
       putStrLn "Failed to produce parser for \{string}"
       pure False
   Right result <- runEff (rundownFirst p) [handleParserStateIO state] {m = IO}
-    | Left err => ?show_err
+    | 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) 
+```

From 03b06a694499a9bad4a0bb17ad6e968e8bf3cd83 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 22:18:09 -0500
Subject: [PATCH 04/29] numbers: Nat parser

---
 src/Parser/Numbers.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 195570f..008b649 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -9,6 +9,10 @@ import Data.Vect
 import Control.Eff
 ```
 
+<!-- idris
+import System
+-->
+
 ## Base Abstraction
 
 ```idris
@@ -52,6 +56,20 @@ hex = MkBase 16
 ```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 <- parseChar (hasDigit b) id
+        | 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

From cd4d7374342ed195f2a9b2255a703f6334c23433 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 22:39:06 -0500
Subject: [PATCH 05/29] numbers: Integer parser

---
 src/Parser/Numbers.md | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 008b649..d25343b 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -76,6 +76,23 @@ natBase10 : Parser Nat
 natBase10 = nat base10
 ```
 
+### Integer
+
+```idris
+export
+integer : Base -> Parser Integer
+integer b = do
+  negative <- map isJust . tryMaybe $ parseExactChar '-'
+  value <- map natToInteger $ nat b
+  if negative
+    then pure $ negate value
+    else pure $ value
+
+export
+integerBase10 : Parser Integer
+integerBase10 = integer base10
+```
+
 ## Unit tests
 
 Test roundtripping a value through the provided parser
@@ -111,3 +128,22 @@ natRoundTrip = pure $
   && !(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) 
+```

From fbb5fc09be0bfa55f7f619e8ee54db6491725c69 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 00:00:52 -0500
Subject: [PATCH 06/29] numbers: Double Parser

---
 src/Parser/Numbers.md | 111 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index d25343b..1f65bb5 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -93,6 +93,63 @@ integerBase10 : Parser Integer
 integerBase10 = integer base10
 ```
 
+### Double
+
+```idris
+export
+double : Base -> Parser Double
+double b = 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 <- parseChar (hasDigit b) id
+        | GotError e => throwParseError "\{show e} is not a digit"
+        | EndOfInput => throwParseError "End Of Input"
+      pure char
+    integer : Parser String
+    integer = do
+      sign <- tryMaybe $ parseExactChar '-'
+      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 <- parseExactChar '.'
+      error <- replaceError "Expected digit"
+      digits <- map forget $ atLeastOne error parseDigit
+      pure $ pack digits
+    exponent : Parser String
+    exponent = do
+      e <- parseTheseChars ['e', 'E']
+      sign <- parseTheseChars ['+', '-']
+      error <- replaceError "Expected digit"
+      digits <- map forget $ atLeastOne error parseDigit
+      pure . pack $ sign :: digits
+
+export
+doubleBase10 : Parser Double
+doubleBase10 = double base10
+```
+
 ## Unit tests
 
 Test roundtripping a value through the provided parser
@@ -147,3 +204,57 @@ integerRoundTrip = pure $
   && !(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 doubleBase10) [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") 
+```

From e871a91fb8e7886b4b85734bcd2007fa79f837b9 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:24:40 -0500
Subject: [PATCH 07/29] numbers: make double non base-sensitive

---
 src/Parser/Numbers.md | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 1f65bb5..fb7b780 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -96,9 +96,10 @@ integerBase10 = integer base10
 ### Double
 
 ```idris
+-- TODO: Replicate `parseDouble` logic and make this base-generic
 export
-double : Base -> Parser Double
-double b = do
+double : Parser Double
+double = do
   starting_state <- save
   integer <- integer
   fraction <- tryMaybe fraction
@@ -119,7 +120,7 @@ double b = do
   where
     parseDigit : Parser Char
     parseDigit = do
-      GotChar char <- parseChar (hasDigit b) id
+      GotChar char <- parseChar (hasDigit base10) id
         | GotError e => throwParseError "\{show e} is not a digit"
         | EndOfInput => throwParseError "End Of Input"
       pure char
@@ -144,10 +145,6 @@ double b = do
       error <- replaceError "Expected digit"
       digits <- map forget $ atLeastOne error parseDigit
       pure . pack $ sign :: digits
-
-export
-doubleBase10 : Parser Double
-doubleBase10 = double base10
 ```
 
 ## Unit tests
@@ -215,7 +212,7 @@ compareDouble string = do
       putStrLn "Failed to produce parser for \{string}"
       pure False
   Right result <- 
-    runEff (rundownFirst doubleBase10) [handleParserStateIO state] {m = IO}
+    runEff (rundownFirst double) [handleParserStateIO state] {m = IO}
     | Left err => do
       printLn err
       pure False

From 2775429bf3b5ec63a6d71522f93996757d645b2f Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:26:35 -0500
Subject: [PATCH 08/29] numbers: Fix readme

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index dc78c7c..fcbee4e 100644
--- a/README.md
+++ b/README.md
@@ -68,7 +68,7 @@ solution.
 
     Internal state of a parser
 
-  - [ParserState](src/Parser/ParserState.md)
+  - [Numbers](src/Parser/Numbers.md)
 
     Parsers for numerical values in multiple bases
 

From 6be2b5372e8db80da0734c3bf3016bee7120eccd Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:27:25 -0500
Subject: [PATCH 09/29] json: create module

---
 README.md          |  4 ++++
 advent.ipkg        |  1 +
 src/Parser/JSON.md | 12 ++++++++++++
 3 files changed, 17 insertions(+)
 create mode 100644 src/Parser/JSON.md

diff --git a/README.md b/README.md
index fcbee4e..48644ce 100644
--- a/README.md
+++ b/README.md
@@ -72,6 +72,10 @@ solution.
 
     Parsers for numerical values in multiple bases
 
+  - [JSON](src/Parser/JSON.md)
+
+  JSON Parser
+
 ## Index of years and days
 
 - 2015
diff --git a/advent.ipkg b/advent.ipkg
index e8aff07..119b03c 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -33,6 +33,7 @@ modules = Runner
         , Parser
         , Parser.Interface
         , Parser.Numbers
+        , Parser.JSON
 
 -- main file (i.e. file to load at REPL)
 main = Main
diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
new file mode 100644
index 0000000..1f2377c
--- /dev/null
+++ b/src/Parser/JSON.md
@@ -0,0 +1,12 @@
+# JSON Parser
+
+```idris
+module Parser.JSON
+
+import public Parser
+import public Parser.Numbers
+```
+
+<!-- idris
+import System
+-->

From e74fe68e327c86e843f8e8d60435fa8e46900aaa Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:50:22 -0500
Subject: [PATCH 10/29] json: Define types, add sop

---
 advent.ipkg | 1 +
 1 file changed, 1 insertion(+)

diff --git a/advent.ipkg b/advent.ipkg
index 119b03c..607e26e 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -19,6 +19,7 @@ depends = base
         , tailrec
         , eff
         , elab-util
+        , sop
         , ansi
         , if-unsolved-implicit
         , c-ffi

From 06e9c09eabee79cf7c3a03f2db67555bbb9a1a5b Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 03:16:52 -0500
Subject: [PATCH 11/29] json: Parser types

---
 src/Parser/JSON.md | 84 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 1f2377c..1b08b12 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -5,8 +5,92 @@ module Parser.JSON
 
 import public Parser
 import public Parser.Numbers
+
+import Structures.Dependent.DList
 ```
 
 <!-- idris
 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
+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 "," . map show $ xs}]"
+  show (VString s) = "\"\{s}\""
+  show (VNumber d) = show d
+  show (VBool False) = "false"
+  show (VBool True) = "true"
+  show VNull = "null"
+-->
+
+## 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)
+```

From 894b0bcbf9694b0b72b02260631948281b931b92 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 04:06:17 -0500
Subject: [PATCH 12/29] json: Object and array

---
 src/Parser/JSON.md | 114 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 109 insertions(+), 5 deletions(-)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 1b08b12..faca235 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -67,6 +67,8 @@ Show (JSONValue t) where
   show (VBool False) = "false"
   show (VBool True) = "true"
   show VNull = "null"
+
+%hide Language.Reflection.TT.WithFC.value
 -->
 
 ## Parsers
@@ -78,19 +80,121 @@ 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
+  result <- 
+    parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) id
+  case result of
+    GotChar char => pure char
+    GotError err => throwParseError "Expected whitespace, got: \{show err}"
+    EndOfInput => throwParseError "End of Input"
+```
+
+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 
+  _ <- many whitespace
+  val <- oneOfE 
+    (throwParseError "Expected JSON Value") 
+    (the (List _) 
+      [
+        dpairize object
+      , dpairize array
+      , dpairize string
+      , dpairize number
+      , dpairize bool
+      , dpairize null
+      ])
+  _ <- many whitespace
+  pure val
+```
+
+Now go through our json value types
+
+```idris
+object = do
+  oneOfE 
+    (throwParseError "Expected Object") 
+    (the (List _) [emptyObject, occupiedObject])
+  where
+    emptyObject : Parser (JSONValue TObject)
+    emptyObject = do
+      _ <- parseExactChar '{'
+      _ <- many whitespace
+      _ <- parseExactChar '}'
+      pure $ VObject Nil
+    firstKeyValue : Parser (t : JSONType ** (String, JSONValue t))
+    firstKeyValue = do
+      _ <- many whitespace
+      VString key <- string
+      _ <- many whitespace
+      _ <- parseExactChar ':'
+      (typ ** val) <- value
+      pure (typ ** (key, val))
+    restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
+    restKeyValue = do
+      _ <- parseExactChar ','
+      firstKeyValue
+    occupiedObject : Parser (JSONValue TObject)
+    occupiedObject = do
+      _ <- parseExactChar '{'
+      first <- firstKeyValue
+      rest <- many restKeyValue
+      _ <- parseExactChar '}'
+      let (types ** xs) = DList.fromList (first :: rest)
+      pure $ VObject xs
+```
+
+```idris
+array = do
+  oneOfE 
+    (throwParseError "Expected Array") 
+    (the (List _) [emptyArray, occupiedArray])
+  where
+    emptyArray : Parser (JSONValue TArray)
+    emptyArray = do
+      _ <- parseExactChar '['
+      _ <- many whitespace
+      _ <- parseExactChar ']'
+      pure $ VArray Nil
+    restValue : Parser (t : JSONType ** JSONValue t)
+    restValue = do
+      _ <- parseExactChar ','
+      value
+    occupiedArray : Parser (JSONValue TArray)
+    occupiedArray = do
+      _ <- parseExactChar '['
+      first <- value
+      rest <- many restValue
+      _ <- parseExactChar ']'
+      let (types ** xs) = DList.fromList (first :: rest)
+      pure $ VArray xs
+```

From e3d563e6a3213bf75e19d8f2de452494865771ec Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 04:39:25 -0500
Subject: [PATCH 13/29] json: Janky string

---
 src/Parser/JSON.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index faca235..453177a 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -198,3 +198,14 @@ array = do
       let (types ** xs) = DList.fromList (first :: rest)
       pure $ VArray xs
 ```
+
+```idris
+string = do
+  _ <- parseExactChar '"'
+  -- TODO: Handle control characters properly
+  e1 <- parseError "Expected non-quote, got quote"
+  e2 <- parseError "End of input"
+  contents <- parseString . many $ parseCharE (not . (== '"')) (\_ => e1) e2
+  _ <- parseExactChar '"'
+  pure $ VString contents
+```

From 3029432699fa8f74a11cf35a759319aa9ed2e994 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 05:07:42 -0500
Subject: [PATCH 14/29] core: export exactString

---
 src/Parser/Interface.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Parser/Interface.md b/src/Parser/Interface.md
index 2c65cfa..3dc4251 100644
--- a/src/Parser/Interface.md
+++ b/src/Parser/Interface.md
@@ -238,6 +238,7 @@ parseTheseChars cs = do
 Attempt to parse an exact string
 
 ```idris
+export
 exactString : String -> Parser String
 exactString str with (asList str)
   exactString "" | [] = pure ""

From 5ced7050837485f24fd6e638fbf7506d867b1e1e Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 16:33:29 -0500
Subject: [PATCH 15/29] numbers: Create numbers module

---
 README.md             | 4 ++++
 advent.ipkg           | 1 +
 src/Parser/Numbers.md | 5 +++++
 3 files changed, 10 insertions(+)
 create mode 100644 src/Parser/Numbers.md

diff --git a/README.md b/README.md
index 52d86cd..dc78c7c 100644
--- a/README.md
+++ b/README.md
@@ -68,6 +68,10 @@ solution.
 
     Internal state of a parser
 
+  - [ParserState](src/Parser/ParserState.md)
+
+    Parsers for numerical values in multiple bases
+
 ## Index of years and days
 
 - 2015
diff --git a/advent.ipkg b/advent.ipkg
index 56f6e75..e8aff07 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -32,6 +32,7 @@ modules = Runner
         , Array
         , Parser
         , Parser.Interface
+        , Parser.Numbers
 
 -- main file (i.e. file to load at REPL)
 main = Main
diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
new file mode 100644
index 0000000..29e6ece
--- /dev/null
+++ b/src/Parser/Numbers.md
@@ -0,0 +1,5 @@
+# Numerical Parsers
+
+```idris
+module Parser.Numbers
+```

From 55813e44648a1dc635793d23ce9fc4cb80031afc Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 17:54:21 -0500
Subject: [PATCH 16/29] numbers: Basic module structure

---
 src/Parser/Numbers.md | 69 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 29e6ece..aa0e156 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -2,4 +2,73 @@
 
 ```idris
 module Parser.Numbers
+  
+import public Parser
+
+import Data.Vect
+import Control.Eff
+```
+
+## 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 : Parser Nat
+```
+
+## 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 => ?show_err
+  putStrLn "Input: \{string} Output: \{show result}"
+  pure $ x == result
 ```

From 9515e3e1c5a09cee8af02a30b20a82630face19d Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 18:09:20 -0500
Subject: [PATCH 17/29] numbers: Nat unit tests

---
 src/Parser/Numbers.md | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index aa0e156..195570f 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -51,7 +51,11 @@ hex = MkBase 16
 
 ```idris
 export
-nat : Parser Nat
+nat : Base -> Parser Nat
+
+export
+natBase10 : Parser Nat
+natBase10 = nat base10
 ```
 
 ## Unit tests
@@ -68,7 +72,24 @@ roundtrip x p = do
       putStrLn "Failed to produce parser for \{string}"
       pure False
   Right result <- runEff (rundownFirst p) [handleParserStateIO state] {m = IO}
-    | Left err => ?show_err
+    | 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) 
+```

From 6734740946d01cf9fe90cf4ffef5caeb5c18a7e4 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 22:18:09 -0500
Subject: [PATCH 18/29] numbers: Nat parser

---
 src/Parser/Numbers.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 195570f..008b649 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -9,6 +9,10 @@ import Data.Vect
 import Control.Eff
 ```
 
+<!-- idris
+import System
+-->
+
 ## Base Abstraction
 
 ```idris
@@ -52,6 +56,20 @@ hex = MkBase 16
 ```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 <- parseChar (hasDigit b) id
+        | 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

From 025b76672dea9cef87c46e2f284cdcc3d38ca450 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 22:39:06 -0500
Subject: [PATCH 19/29] numbers: Integer parser

---
 src/Parser/Numbers.md | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 008b649..d25343b 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -76,6 +76,23 @@ natBase10 : Parser Nat
 natBase10 = nat base10
 ```
 
+### Integer
+
+```idris
+export
+integer : Base -> Parser Integer
+integer b = do
+  negative <- map isJust . tryMaybe $ parseExactChar '-'
+  value <- map natToInteger $ nat b
+  if negative
+    then pure $ negate value
+    else pure $ value
+
+export
+integerBase10 : Parser Integer
+integerBase10 = integer base10
+```
+
 ## Unit tests
 
 Test roundtripping a value through the provided parser
@@ -111,3 +128,22 @@ natRoundTrip = pure $
   && !(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) 
+```

From c1a2cf496365591ddad62f8d0948ffe3a363ff0d Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 00:00:52 -0500
Subject: [PATCH 20/29] numbers: Double Parser

---
 src/Parser/Numbers.md | 111 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index d25343b..1f65bb5 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -93,6 +93,63 @@ integerBase10 : Parser Integer
 integerBase10 = integer base10
 ```
 
+### Double
+
+```idris
+export
+double : Base -> Parser Double
+double b = 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 <- parseChar (hasDigit b) id
+        | GotError e => throwParseError "\{show e} is not a digit"
+        | EndOfInput => throwParseError "End Of Input"
+      pure char
+    integer : Parser String
+    integer = do
+      sign <- tryMaybe $ parseExactChar '-'
+      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 <- parseExactChar '.'
+      error <- replaceError "Expected digit"
+      digits <- map forget $ atLeastOne error parseDigit
+      pure $ pack digits
+    exponent : Parser String
+    exponent = do
+      e <- parseTheseChars ['e', 'E']
+      sign <- parseTheseChars ['+', '-']
+      error <- replaceError "Expected digit"
+      digits <- map forget $ atLeastOne error parseDigit
+      pure . pack $ sign :: digits
+
+export
+doubleBase10 : Parser Double
+doubleBase10 = double base10
+```
+
 ## Unit tests
 
 Test roundtripping a value through the provided parser
@@ -147,3 +204,57 @@ integerRoundTrip = pure $
   && !(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 doubleBase10) [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") 
+```

From 7c7950956a0f2d5a425ed3cb68d15839be429b73 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:24:40 -0500
Subject: [PATCH 21/29] numbers: make double non base-sensitive

---
 src/Parser/Numbers.md | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 1f65bb5..fb7b780 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -96,9 +96,10 @@ integerBase10 = integer base10
 ### Double
 
 ```idris
+-- TODO: Replicate `parseDouble` logic and make this base-generic
 export
-double : Base -> Parser Double
-double b = do
+double : Parser Double
+double = do
   starting_state <- save
   integer <- integer
   fraction <- tryMaybe fraction
@@ -119,7 +120,7 @@ double b = do
   where
     parseDigit : Parser Char
     parseDigit = do
-      GotChar char <- parseChar (hasDigit b) id
+      GotChar char <- parseChar (hasDigit base10) id
         | GotError e => throwParseError "\{show e} is not a digit"
         | EndOfInput => throwParseError "End Of Input"
       pure char
@@ -144,10 +145,6 @@ double b = do
       error <- replaceError "Expected digit"
       digits <- map forget $ atLeastOne error parseDigit
       pure . pack $ sign :: digits
-
-export
-doubleBase10 : Parser Double
-doubleBase10 = double base10
 ```
 
 ## Unit tests
@@ -215,7 +212,7 @@ compareDouble string = do
       putStrLn "Failed to produce parser for \{string}"
       pure False
   Right result <- 
-    runEff (rundownFirst doubleBase10) [handleParserStateIO state] {m = IO}
+    runEff (rundownFirst double) [handleParserStateIO state] {m = IO}
     | Left err => do
       printLn err
       pure False

From 352822a5181516e888e09b047434ed4ab198ce31 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:26:35 -0500
Subject: [PATCH 22/29] numbers: Fix readme

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index dc78c7c..fcbee4e 100644
--- a/README.md
+++ b/README.md
@@ -68,7 +68,7 @@ solution.
 
     Internal state of a parser
 
-  - [ParserState](src/Parser/ParserState.md)
+  - [Numbers](src/Parser/Numbers.md)
 
     Parsers for numerical values in multiple bases
 

From fdb166a2a6374e1ffef970f2ed2c2b65fdd0ba41 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:27:25 -0500
Subject: [PATCH 23/29] json: create module

---
 README.md          |  4 ++++
 advent.ipkg        |  1 +
 src/Parser/JSON.md | 12 ++++++++++++
 3 files changed, 17 insertions(+)
 create mode 100644 src/Parser/JSON.md

diff --git a/README.md b/README.md
index fcbee4e..48644ce 100644
--- a/README.md
+++ b/README.md
@@ -72,6 +72,10 @@ solution.
 
     Parsers for numerical values in multiple bases
 
+  - [JSON](src/Parser/JSON.md)
+
+  JSON Parser
+
 ## Index of years and days
 
 - 2015
diff --git a/advent.ipkg b/advent.ipkg
index e8aff07..119b03c 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -33,6 +33,7 @@ modules = Runner
         , Parser
         , Parser.Interface
         , Parser.Numbers
+        , Parser.JSON
 
 -- main file (i.e. file to load at REPL)
 main = Main
diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
new file mode 100644
index 0000000..1f2377c
--- /dev/null
+++ b/src/Parser/JSON.md
@@ -0,0 +1,12 @@
+# JSON Parser
+
+```idris
+module Parser.JSON
+
+import public Parser
+import public Parser.Numbers
+```
+
+<!-- idris
+import System
+-->

From 1a9fce3860ffaa3dcd5e1bf291743650171b5e2b Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 02:50:22 -0500
Subject: [PATCH 24/29] json: Define types, add sop

---
 advent.ipkg | 1 +
 1 file changed, 1 insertion(+)

diff --git a/advent.ipkg b/advent.ipkg
index 119b03c..607e26e 100644
--- a/advent.ipkg
+++ b/advent.ipkg
@@ -19,6 +19,7 @@ depends = base
         , tailrec
         , eff
         , elab-util
+        , sop
         , ansi
         , if-unsolved-implicit
         , c-ffi

From 8b111a183909acecc91bd302e37987b63b7a159c Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 03:16:52 -0500
Subject: [PATCH 25/29] json: Parser types

---
 src/Parser/JSON.md | 84 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 1f2377c..1b08b12 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -5,8 +5,92 @@ module Parser.JSON
 
 import public Parser
 import public Parser.Numbers
+
+import Structures.Dependent.DList
 ```
 
 <!-- idris
 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
+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 "," . map show $ xs}]"
+  show (VString s) = "\"\{s}\""
+  show (VNumber d) = show d
+  show (VBool False) = "false"
+  show (VBool True) = "true"
+  show VNull = "null"
+-->
+
+## 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)
+```

From cc9b0edfb23b4e5700d942d1d2852702b1a63157 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 04:06:17 -0500
Subject: [PATCH 26/29] json: Object and array

---
 src/Parser/JSON.md | 114 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 109 insertions(+), 5 deletions(-)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 1b08b12..faca235 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -67,6 +67,8 @@ Show (JSONValue t) where
   show (VBool False) = "false"
   show (VBool True) = "true"
   show VNull = "null"
+
+%hide Language.Reflection.TT.WithFC.value
 -->
 
 ## Parsers
@@ -78,19 +80,121 @@ 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
+  result <- 
+    parseChar (\x => any (== x) $ the (List _) [' ', '\n', '\r', '\t']) id
+  case result of
+    GotChar char => pure char
+    GotError err => throwParseError "Expected whitespace, got: \{show err}"
+    EndOfInput => throwParseError "End of Input"
+```
+
+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 
+  _ <- many whitespace
+  val <- oneOfE 
+    (throwParseError "Expected JSON Value") 
+    (the (List _) 
+      [
+        dpairize object
+      , dpairize array
+      , dpairize string
+      , dpairize number
+      , dpairize bool
+      , dpairize null
+      ])
+  _ <- many whitespace
+  pure val
+```
+
+Now go through our json value types
+
+```idris
+object = do
+  oneOfE 
+    (throwParseError "Expected Object") 
+    (the (List _) [emptyObject, occupiedObject])
+  where
+    emptyObject : Parser (JSONValue TObject)
+    emptyObject = do
+      _ <- parseExactChar '{'
+      _ <- many whitespace
+      _ <- parseExactChar '}'
+      pure $ VObject Nil
+    firstKeyValue : Parser (t : JSONType ** (String, JSONValue t))
+    firstKeyValue = do
+      _ <- many whitespace
+      VString key <- string
+      _ <- many whitespace
+      _ <- parseExactChar ':'
+      (typ ** val) <- value
+      pure (typ ** (key, val))
+    restKeyValue : Parser (t : JSONType ** (String, JSONValue t))
+    restKeyValue = do
+      _ <- parseExactChar ','
+      firstKeyValue
+    occupiedObject : Parser (JSONValue TObject)
+    occupiedObject = do
+      _ <- parseExactChar '{'
+      first <- firstKeyValue
+      rest <- many restKeyValue
+      _ <- parseExactChar '}'
+      let (types ** xs) = DList.fromList (first :: rest)
+      pure $ VObject xs
+```
+
+```idris
+array = do
+  oneOfE 
+    (throwParseError "Expected Array") 
+    (the (List _) [emptyArray, occupiedArray])
+  where
+    emptyArray : Parser (JSONValue TArray)
+    emptyArray = do
+      _ <- parseExactChar '['
+      _ <- many whitespace
+      _ <- parseExactChar ']'
+      pure $ VArray Nil
+    restValue : Parser (t : JSONType ** JSONValue t)
+    restValue = do
+      _ <- parseExactChar ','
+      value
+    occupiedArray : Parser (JSONValue TArray)
+    occupiedArray = do
+      _ <- parseExactChar '['
+      first <- value
+      rest <- many restValue
+      _ <- parseExactChar ']'
+      let (types ** xs) = DList.fromList (first :: rest)
+      pure $ VArray xs
+```

From 69e36774b53ca514b7a436718b88da0abc690ed1 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 04:39:25 -0500
Subject: [PATCH 27/29] json: Janky string

---
 src/Parser/JSON.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index faca235..453177a 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -198,3 +198,14 @@ array = do
       let (types ** xs) = DList.fromList (first :: rest)
       pure $ VArray xs
 ```
+
+```idris
+string = do
+  _ <- parseExactChar '"'
+  -- TODO: Handle control characters properly
+  e1 <- parseError "Expected non-quote, got quote"
+  e2 <- parseError "End of input"
+  contents <- parseString . many $ parseCharE (not . (== '"')) (\_ => e1) e2
+  _ <- parseExactChar '"'
+  pure $ VString contents
+```

From e46e1663b984fe318c7ab3c6b1195f672a47ef73 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 05:04:54 -0500
Subject: [PATCH 28/29] json: number

---
 src/Parser/JSON.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index 453177a..c4d987d 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -209,3 +209,9 @@ string = do
   _ <- parseExactChar '"'
   pure $ VString contents
 ```
+
+```idris
+number = do
+  d <- double
+  pure $ VNumber d
+```

From 2111e20f33a004f560e2190743264a582c9d9bbf Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 25 Jan 2025 05:09:24 -0500
Subject: [PATCH 29/29] json: Bool and null

---
 src/Parser/JSON.md | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md
index c4d987d..7e83fd7 100644
--- a/src/Parser/JSON.md
+++ b/src/Parser/JSON.md
@@ -215,3 +215,25 @@ number = do
   d <- double
   pure $ VNumber d
 ```
+
+```idris
+bool = do
+  oneOfE
+    (throwParseError "Expected Bool")
+    (the (List _) [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
+  _ <- exactString "null"
+  pure VNull
+```