8 | module JSON.Simple.FromJSON
10 | import Data.List.Quantifiers as LQ
11 | import Data.Vect.Quantifiers as VQ
12 | import Data.SortedMap
13 | import Data.Singleton
14 | import Derive.Prelude
16 | import JSON.Simple.Option
17 | import JSON.Simple.ToJSON
20 | %language ElabReflection
29 | data JSONPathElement = Key String | Index Bits32
31 | %runElab derive "JSONPathElement" [Show,Eq]
35 | JSONPath = List JSONPathElement
39 | JSONErr = (JSONPath,String)
42 | Result : Type -> Type
43 | Result = Either JSONErr
46 | Parser : Type -> Type -> Type
47 | Parser v a = v -> Either JSONErr a
50 | orElse : Either a b -> Lazy (Either a b) -> Either a b
51 | orElse r@(Right _) _ = r
55 | (<|>) : Parser v a -> Parser v a -> Parser v a
56 | f <|> g = \vv => f vv `orElse` g vv
59 | data DecodingErr : Type where
60 | JErr : JSONErr -> DecodingErr
61 | JParseErr : ParseError Void -> DecodingErr
63 | %runElab derive "DecodingErr" [Show,Eq]
66 | DecodingResult : Type -> Type
67 | DecodingResult = Either DecodingErr
76 | formatRelativePath : JSONPath -> String
77 | formatRelativePath path = format "" path
79 | isIdentifierKey : List Char -> Bool
80 | isIdentifierKey [] = False
81 | isIdentifierKey (x::xs) = isAlpha x && all isAlphaNum xs
83 | escapeChar : Char -> String
84 | escapeChar '\'' = "\\'"
85 | escapeChar '\\' = "\\\\"
86 | escapeChar c = singleton c
88 | escapeKey : List Char -> String
89 | escapeKey = fastConcat . map escapeChar
91 | formatKey : String -> String
93 | let chars = fastUnpack key
94 | in if isIdentifierKey chars then fastPack $
'.' :: chars
95 | else "['" ++ escapeKey chars ++ "']"
97 | format : String -> JSONPath -> String
99 | format pfx (Index idx :: parts) = format (pfx ++ "[" ++ show idx ++ "]") parts
100 | format pfx (Key key :: parts) = format (pfx ++ formatKey key) parts
105 | formatPath : JSONPath -> String
106 | formatPath path = "$" ++ formatRelativePath path
111 | formatError : JSONPath -> String -> String
112 | formatError path msg = "Error in " ++ formatPath path ++ ": " ++ msg
115 | Interpolation DecodingErr where
116 | interpolate (JErr (p,s)) = formatError p s
117 | interpolate (JParseErr x) = interpolate x
124 | prettyErr : (input : String) -> DecodingErr -> String
125 | prettyErr _ = interpolate
132 | interface FromJSON a where
133 | constructor MkFromJSON
134 | fromJSON : Parser JSON a
137 | interface FromJSONKey a where
138 | constructor MkFromJSONKey
139 | fromKey : Parser String a
142 | decode : FromJSON a => String -> DecodingResult a
144 | let Right json := parseJSON Virtual s | Left err => Left (JParseErr err)
145 | Right res := fromJSON json | Left p => Left (JErr p)
149 | decodeEither : FromJSON a => String -> Either String a
150 | decodeEither s = mapFst interpolate $
decode s
153 | decodeMaybe : FromJSON a => String -> Maybe a
154 | decodeMaybe = either (const Nothing) Just . decode
161 | typeOf : JSON -> String
162 | typeOf JNull = "Null"
163 | typeOf (JBool _) = "Boolean"
164 | typeOf (JDouble _) = "Double"
165 | typeOf (JInteger _) = "Integer"
166 | typeOf (JString _) = "String"
167 | typeOf (JArray _) = "Array"
168 | typeOf (JObject _) = "Object"
171 | fail : String -> Result a
172 | fail s = Left (Nil,s)
174 | typeMismatch : String -> Parser JSON a
175 | typeMismatch expected actual =
176 | fail $
"expected \{expected}, but encountered \{typeOf actual}"
178 | unexpected : Parser JSON a
179 | unexpected actual = fail $
"unexpected \{typeOf actual}"
182 | modifyFailure : (String -> String) -> Result a -> Result a
183 | modifyFailure f = mapFst (map f)
188 | prependFailure : String -> Result a -> Result a
189 | prependFailure = modifyFailure . (++)
192 | prependContext : String -> Result a -> Result a
193 | prependContext name = prependFailure "parsing \{name} failed, "
196 | prependPath : Result a -> JSONPathElement -> Result a
197 | prependPath r elem = mapFst (\(path,s) => (elem :: path,s)) r
201 | -> (JSON -> Maybe t)
202 | -> (name : Lazy String)
205 | withValue s get n f val =
208 | Nothing => prependContext n $
typeMismatch s val
211 | withKey : Parser String a -> Parser String a
212 | withKey f = prependFailure "parsing key failed, " . f
215 | withObject : Lazy String -> Parser (List (String,JSON)) a -> Parser JSON a
216 | withObject = withValue "Object" $
\case JObject ps => Just ps;
_ => Nothing
219 | withBoolean : Lazy String -> Parser Bool a -> Parser JSON a
220 | withBoolean = withValue "Boolean" $
\case JBool b => Just b;
_ => Nothing
223 | withString : Lazy String -> Parser String a -> Parser JSON a
224 | withString = withValue "String" $
\case JString s => Just s;
_ => Nothing
227 | withNull : String -> t -> Parser JSON t
228 | withNull s x JNull = Right x
230 | prependContext s $
fail "expexted Null but encountered \{typeOf v}"
233 | eqString : Lazy String -> String -> Parser JSON ()
234 | eqString n s = withString n $
\s' =>
235 | if s == s' then Right () else fail "expected '\{s}' but got '\{s'}'"
238 | withDouble : Lazy String -> Parser Double a -> Parser JSON a
240 | withValue "Double" $
\case
241 | JDouble d => Just d
242 | JInteger n => Just (cast n)
246 | withInteger : Lazy String -> Parser Integer a -> Parser JSON a
247 | withInteger = withValue "Integer" $
\case JInteger d => Just d;
_ => Nothing
250 | pint1 : PVal1 q Void Integer
251 | pint1 = value Nothing [(decimal, bytes decimal)]
254 | withIntegerKey : Parser Integer a -> Parser String a
257 | case parseString pint1 Virtual s of
259 | Left _ => fail "not an integer: \{s}"
265 | -> (lower : Integer)
266 | -> (upper : Integer)
268 | boundedIntegral s lo up =
269 | withInteger s $
\n =>
270 | if n >= lo && n <= up
271 | then Right $
fromInteger n
272 | else fail "integer out of bounds: \{show n}"
275 | boundedIntegralKey :
277 | -> (lower : Integer)
278 | -> (upper : Integer)
280 | boundedIntegralKey lo up =
281 | withIntegerKey $
\n =>
282 | if n >= lo && n <= up
283 | then Right $
fromInteger n
284 | else fail "integer out of bounds: \{show n}"
287 | withArray : Lazy String -> Parser (List JSON) a -> Parser JSON a
288 | withArray = withValue "Array" $
\case JArray v => Just v;
_ => Nothing
294 | -> Parser (Vect n JSON) a
296 | withArrayN n = withValue "Array of length \{show n}" $
297 | \case JArray v => toVect n v;
_ => Nothing
301 | explicitParseField : Parser JSON a -> List (String,JSON) -> Parser String a
302 | explicitParseField p o key =
303 | case lookup key o of
304 | Nothing => fail "key \{show key} not found"
305 | Just v => p v `prependPath` Key key
309 | explicitParseFieldMaybe :
311 | -> List (String,JSON)
312 | -> Parser String (Maybe a)
313 | explicitParseFieldMaybe p o key =
314 | case lookup key o of
315 | Nothing => Right Nothing
316 | Just JNull => Right Nothing
317 | Just v => map Just $
p v `prependPath` Key key
321 | explicitParseFieldMaybe' :
323 | -> List (String,JSON)
325 | explicitParseFieldMaybe' p o key =
326 | case lookup key o of
327 | Nothing => p JNull `prependPath` Key key
328 | Just v => p v `prependPath` Key key
338 | field : FromJSON a => List (String,JSON) -> Parser String a
339 | field = explicitParseField fromJSON
349 | fieldMaybe : FromJSON a => List (String,JSON) -> Parser String (Maybe a)
350 | fieldMaybe = explicitParseFieldMaybe fromJSON
358 | optField : FromJSON a => List (String,JSON) -> Parser String a
359 | optField = explicitParseFieldMaybe' fromJSON
364 | fieldWithDeflt : FromJSON a => List (String,JSON) -> Lazy a -> Parser String a
365 | fieldWithDeflt ps v s = fromMaybe v <$> fieldMaybe ps s
372 | FromJSON JSON where fromJSON = Right
375 | FromJSON Void where
376 | fromJSON v = fail "Cannot parse Void"
380 | fromJSON = withArray "()" $
381 | \case Nil => Right ()
382 | _ :: _ => fail "parsing () failed, expected empty list"
385 | FromJSON Bool where
386 | fromJSON = withBoolean "Bool" Right
389 | FromJSONKey Bool where
392 | \case "True" => Right True
393 | "False" => Right False
394 | s => fail "not a bool: \{s}"
397 | FromJSON Double where
398 | fromJSON = withDouble "Double" Right
401 | pdbl1 : PVal1 q Void Double
402 | pdbl1 = value Nothing [(jsonDouble, txt jdouble)]
405 | FromJSONKey Double where
408 | case parseString pdbl1 Virtual s of
410 | Left _ => fail "not a floating point number: \{s}"
413 | FromJSON Bits8 where
414 | fromJSON = boundedIntegral "Bits8" 0 0xff
417 | FromJSON Bits16 where
418 | fromJSON = boundedIntegral "Bits16" 0 0xffff
421 | FromJSON Bits32 where
422 | fromJSON = boundedIntegral "Bits32" 0 0xffffffff
425 | FromJSON Bits64 where
426 | fromJSON = boundedIntegral "Bits64" 0 0xffffffffffffffff
430 | fromJSON = boundedIntegral "Int" (-
0x8000000000000000) 0x7fffffffffffffff
433 | FromJSON Int8 where
434 | fromJSON = boundedIntegral "Int8" (-
0x80) 0x7f
437 | FromJSON Int16 where
438 | fromJSON = boundedIntegral "Int16" (-
0x8000) 0x7fff
441 | FromJSON Int32 where
442 | fromJSON = boundedIntegral "Int32" (-
0x80000000) 0x7fffffff
445 | FromJSON Int64 where
446 | fromJSON = boundedIntegral "Int64" (-
0x8000000000000000) 0x7fffffffffffffff
449 | FromJSONKey Bits8 where
450 | fromKey = boundedIntegralKey 0 0xff
453 | FromJSONKey Bits16 where
454 | fromKey = boundedIntegralKey 0 0xffff
457 | FromJSONKey Bits32 where
458 | fromKey = boundedIntegralKey 0 0xffffffff
461 | FromJSONKey Bits64 where
462 | fromKey = boundedIntegralKey 0 0xffffffffffffffff
465 | FromJSONKey Int where
466 | fromKey = boundedIntegralKey (-
0x8000000000000000) 0x7fffffffffffffff
469 | FromJSONKey Int8 where
470 | fromKey = boundedIntegralKey (-
0x80) 0x7f
473 | FromJSONKey Int16 where
474 | fromKey = boundedIntegralKey (-
0x8000) 0x7fff
477 | FromJSONKey Int32 where
478 | fromKey = boundedIntegralKey (-
0x80000000) 0x7fffffff
481 | FromJSONKey Int64 where
482 | fromKey = boundedIntegralKey (-
0x8000000000000000) 0x7fffffffffffffff
486 | fromJSON = withInteger "Nat" $
\n =>
487 | if n >= 0 then Right $
fromInteger n
488 | else fail "not a natural number: \{show n}"
491 | FromJSONKey Nat where
492 | fromKey = withIntegerKey $
\n =>
493 | if n >= 0 then Right $
fromInteger n
494 | else fail "not a natural number: \{show n}"
497 | FromJSON Integer where
498 | fromJSON = withInteger "Integer" Right
501 | FromJSONKey Integer where
502 | fromKey = withIntegerKey Right
505 | FromJSON String where
506 | fromJSON = withString "String" Right
509 | FromJSONKey String where
510 | fromKey = withKey Right
513 | FromJSON Char where
514 | fromJSON = withString "Char" $
\str =>
516 | StrCons c "" => Right c
517 | _ => fail "expected a string of length 1"
520 | FromJSONKey Char where
521 | fromKey = withKey $
\str =>
523 | StrCons c "" => Right c
524 | _ => fail "expected a string of length 1"
527 | FromJSON a => FromJSON (Maybe a) where
528 | fromJSON JNull = Right Nothing
529 | fromJSON v = Just <$> fromJSON v
532 | FromJSON a => FromJSON (List a) where
533 | fromJSON = withArray "List" $
traverse fromJSON
536 | FromJSON a => FromJSON (SnocList a) where
537 | fromJSON = map ([<] <><) . fromJSON
540 | FromJSON a => FromJSON (List1 a) where
541 | fromJSON = withArray "List1" $
\case
542 | Nil => fail "expected non-empty list"
543 | h :: t => traverse fromJSON (h ::: t)
546 | {v : a} -> FromJSON a => ToJSON a => Eq a => FromJSON (Singleton v) where
548 | fromJSON x >>= \val => case v == val of
549 | True => Right (Val v)
550 | False => fail "Invalid value. Expected \{encode v}"
554 | -> {auto jk : FromJSONKey k}
555 | -> {auto jv : FromJSON v}
557 | -> Parser (List (String,JSON)) (SortedMap k v)
558 | sortedMap m [] = Right m
559 | sortedMap m ((x,y) :: ps) =
560 | let Right k' := fromKey x | Left err => Left err
561 | Right v' := fromJSON y | Left err => Left err
562 | in sortedMap (insert k' v' m) ps
565 | Ord k => FromJSONKey k => FromJSON v => FromJSON (SortedMap k v) where
566 | fromJSON = withObject "SortedMap" (sortedMap empty)
569 | {n : Nat} -> FromJSON a => FromJSON (Vect n a) where
570 | fromJSON = withArray "Vect \{show n}" $
\vs => case toVect n vs of
571 | Just vect => traverse fromJSON vect
572 | Nothing => fail "expected list of length \{show n}"
575 | FromJSON a => FromJSON b => FromJSON (Either a b) where
576 | fromJSON = withObject "Either" $
\o =>
577 | map Left (field o "Left") `orElse`
578 | map Right (field o "Right")
581 | FromJSON a => FromJSON b => FromJSON (a, b) where
582 | fromJSON = withArray "Pair" $
583 | \case [x,y] => [| MkPair (fromJSON x) (fromJSON y) |]
584 | _ => fail "expected a pair of values"
586 | readLQ : (ps : LQ.All.All (FromJSON . f) ts) => Parser (List JSON) (All f ts)
587 | readLQ @{[]} [] = Right []
588 | readLQ @{_::_} (x :: xs) = [| fromJSON x :: readLQ xs |]
589 | readLQ @{_::_} [] = fail "list of values too short"
590 | readLQ @{[]} _ = fail "list of values too long"
592 | readVQ : (ps : VQ.All.All (FromJSON . f) ts) => Parser (List JSON) (All f ts)
593 | readVQ @{[]} [] = Right []
594 | readVQ @{_::_} (x :: xs) = [| fromJSON x :: readVQ xs |]
595 | readVQ @{_::_} [] = fail "list of values too short"
596 | readVQ @{[]} _ = fail "list of values too long"
599 | LQ.All.All (FromJSON . f) ts => FromJSON (All f ts) where
600 | fromJSON = withArray "HList" $
readLQ
603 | VQ.All.All (FromJSON . f) ts => FromJSON (VQ.All.All f ts) where
604 | fromJSON = withArray "HVect" $
readVQ
612 | (tpe : Lazy String)
613 | -> Parser (String,JSON) a
615 | fromSingleField n f = withObject n $
617 | _ => fail "expected single field object"
626 | (tpe : Lazy String)
627 | -> Parser (String,JSON) a
629 | fromTwoElemArray n f =
630 | withArrayN 2 n $
\[x,y] => withString n (\s => f (s,y)) x
639 | (tpe : Lazy String)
640 | -> (tagField, contentField : String)
641 | -> Parser (String,JSON) a
643 | fromTaggedObject n tf cf f = withObject n $
\o => do
645 | v <- explicitParseField Right o cf