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