json: Object and array

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