json: Janky string

README.md

@@ -68,10 +68,14 @@ solution.
 
     Internal state of a parser
 
-  - [ParserState](src/Parser/ParserState.md)
+  - [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
@@ -33,6 +34,7 @@ modules = Runner
         , Parser
         , Parser.Interface
         , Parser.Numbers
+        , Parser.JSON
 
 -- main file (i.e. file to load at REPL)
 main = Main

src/Parser/Interface.md

@@ -235,6 +235,20 @@ parseTheseChars cs = do
     EndOfInput => throwParseError "End of input"
 ```
 
+Attempt to parse an exact string
+
+```idris
+exactString : String -> Parser String
+exactString str with (asList str)
+  exactString "" | [] = pure ""
+  exactString input@(strCons c str) | (c :: x) = do
+    GotChar next <- parseChar (== c) id
+      | GotError err => throwParseError "Got \{show err} expected \{show c}"
+      | EndOfInput => throwParseError "End of input"
+    rest <- exactString str | x
+    pure input
+```
+
 ### Composition of boolean functions
 
 ```idris

src/Parser/JSON.md

@@ -0,0 +1,211 @@
+# JSON Parser
+
+```idris
+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"
+
+%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
+  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
+```
+
+```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
+```

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