JSON Parser
module Parser.JSON
import public Parser
import public Parser.Numbers
import Control.Monad.Eval
import Structures.Dependent.DList
JSON components
Types a JSON value is allowed to have
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
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
JSON Functions
foldl Analog for consuming a JSON structure by values. Ignores the keys in
objects.
export
dFoldL : {t : JSONType}
-> (acc -> (type : JSONType) -> (val : JSONValue type) -> acc)
-> acc -> JSONValue t -> acc
dFoldL f acc' (VObject xs) =
let recur : acc -> (v : JSONType) -> (String, JSONValue v) -> acc
recur acc' v (key, value) = dFoldL f acc' value
in DList.dFoldL recur acc' xs
dFoldL f acc' (VArray xs) =
let recur : acc -> (v : JSONType) -> JSONValue v -> acc
recur acc' v value = dFoldL f acc' value
in DList.dFoldL recur acc' xs
dFoldL f acc (VString s) = f acc _ (VString s)
dFoldL f acc (VNumber d) = f acc _ (VNumber d)
dFoldL f acc (VBool b) = f acc _ (VBool b)
dFoldL f acc VNull = f acc _ VNull
Look up a property in an object
export
getProperty : (prop : String) -> (object : JSONValue TObject)
-> Maybe (type : JSONType ** JSONValue type)
getProperty prop (VObject xs) =
case dFind (\_, (key, _) => key == prop) xs of
Nothing => Nothing
Just (type ** (_, val)) => Just (type ** val)
Return the values from an object.
export
getValues : (object : JSONValue TObject)
-> (types : List JSONType ** DList JSONType JSONValue types)
getValues (VObject xs) =
dMap' (\t, (k, v) => (t ** v)) xs
Recursively apply a filter to a JSON structure.
export
dFilter : (f : (type : JSONType) -> (val : JSONValue type) -> Bool)
-> {t : JSONType} -> JSONValue t -> Maybe (JSONValue t)
dFilter f value = eval $ dFilter' f value
where
dFilter' : (f : (type : JSONType) -> (val : JSONValue type) -> Bool)
-> {t : JSONType} -> JSONValue t -> Eval $ Maybe (JSONValue t)
dFilter' f (VObject xs) = do
True <- pure $ f _ (VObject xs)
| _ => pure Nothing
let xs = toList xs
xs : List (Maybe (x : JSONType ** (String, JSONValue x))) <-
traverse
(\(t ** (k, v)) => do
Just v <- dFilter' f v
| _ => pure Nothing
pure $ Just (t ** (k, v)))
xs
let (_ ** xs) : (t : List JSONType ** DList _ _ t) =
fromList $ catMaybes xs
pure . Just $ VObject xs
dFilter' f (VArray xs) = do
True <- pure $ f _ (VArray xs)
| _ => pure Nothing
let xs = toList xs
xs : List (Maybe (x : JSONType ** JSONValue x)) <-
traverse
(\(t ** v) => do
Just v <- dFilter' f v
| _ => pure Nothing
pure $ Just (t ** v))
xs
let (_ ** xs) : (t : List JSONType ** DList _ _ t) =
fromList $ catMaybes xs
pure . Just $ VArray xs
dFilter' f x =
pure $ case f _ x of
False => Nothing
True => Just x
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.
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
whitespace : Parser Char
whitespace = do
pnote "Whitespace character"
theseChars [' ', '\n', '\r', '\t']
Convenience function
dpairize : {t : JSONType} ->
Parser (JSONValue t) -> Parser (t' : JSONType ** JSONValue t')
dpairize x = do
x <- x
pure (_ ** x)
Top level json value parser
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
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
-- TODO: headTail combinator for this
pure $ first ::: rest
occupiedObject : Parser (JSONValue TObject)
occupiedObject = do
val <- delimited '{' '}' pairs
let (types ** xs) = DList.fromList (forget val)
pure $ VObject xs
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
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"
number = do
pnote "JSON Number"
d <- double
pure $ VNumber d
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
null = do
pnote "JSON null"
_ <- exactString "null"
pure VNull
Unit tests
Quick smoke test
-- @@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