8 | module JSON.FromJSON

 10 | import Data.Either

 11 | import Data.List.Quantifiers as LQ

 12 | import Data.SortedMap

 13 | import Data.Vect.Quantifiers as VQ

 14 | import Derive.Prelude

 15 | import JSON.ToJSON

 16 | import JSON.Option

 17 | import JSON.Encoder

 19 | %language ElabReflection

 21 | %default total

 27 | public export

 28 | data JSONPathElement = Key String | Index Bits32

 30 | %runElab derive "JSONPathElement" [Show,Eq]

 32 | public export

 33 | JSONPath : Type

 34 | JSONPath = List JSONPathElement

 36 | public export

 37 | JSONErr : Type

 38 | JSONErr = (JSONPath,String)

 40 | public export

 41 | Result : Type -> Type

 42 | Result = Either JSONErr

 44 | public export

 45 | Parser : Type -> Type -> Type

 46 | Parser v a = v -> Either JSONErr a

 48 | public export

 49 | orElse : Either a b -> Lazy (Either a b) -> Either a b

 50 | orElse r@(Right _) _ = r

 51 | orElse _           v = v

 53 | public export

 54 | (<|>) : Parser v a -> Parser v a -> Parser v a

 55 | f <|> g = \vv => f vv `orElse` g vv

 57 | public export

 58 | data DecodingErr : Type where

 59 |   JErr      : JSONErr -> DecodingErr

 60 |   JParseErr : ParseError Void -> DecodingErr

 62 | %runElab derive "DecodingErr" [Show,Eq]

 64 | public export

 65 | DecodingResult : Type -> Type

 66 | DecodingResult = Either DecodingErr

 75 | formatRelativePath : JSONPath -> String

 76 | formatRelativePath path = format "" path

 78 |   where

 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

 92 |     formatKey key =

 93 |       let chars := fastUnpack key

 94 |        in if isIdentifierKey chars then fastPack $ '.' :: chars

 95 |           else "['" ++ escapeKey chars ++ "']"

 97 |     format : String -> JSONPath -> String

 98 |     format pfx []                = pfx

 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

123 | export %deprecate

124 | prettyErr : (input : String) -> DecodingErr -> String

125 | prettyErr _ = interpolate

131 | public export

132 | interface FromJSON a  where

133 |   constructor MkFromJSON

134 |   fromJSON : forall v,obj . Value v obj => Parser v a

136 | export %inline

137 | decodeVia :

138 |      (0 v : Type)

139 |   -> {auto _ : Value v obj}

140 |   -> {auto _ : FromJSON a}

141 |   -> String

142 |   -> DecodingResult a

143 | decodeVia v s =

144 |   let Right json := parse {v} Virtual s | Left err => Left (JParseErr err)

145 |       Right res  := fromJSON json       | Left p   => Left (JErr p)

146 |    in Right res

148 | export %inline

149 | decodeEitherVia :

150 |      (0 v : Type)

151 |   -> {auto _ : Value v obj}

152 |   -> {auto _ : FromJSON a}

153 |   -> String

154 |   -> Either String a

155 | decodeEitherVia v s = mapFst interpolate $ decodeVia v s

157 | export %inline

158 | decodeMaybeVia : (0 v : Type) -> Value v obj => FromJSON a => String -> Maybe a

159 | decodeMaybeVia v = either (const Nothing) Just . decodeVia v

161 | export %inline

162 | decode : FromJSON a => String -> DecodingResult a

163 | decode = decodeVia JSON

165 | export %inline

166 | decodeEither : FromJSON a => String -> Either String a

167 | decodeEither = decodeEitherVia JSON

169 | export %inline

170 | decodeMaybe : FromJSON a => String -> Maybe a

171 | decodeMaybe = decodeMaybeVia JSON

177 | export %inline

178 | fail : String -> Result a

179 | fail s = Left (Nil,s)

181 | typeMismatch : Value v obj => String -> Parser v a

182 | typeMismatch expected actual =

183 |   fail $ "expected \{expected}, but encountered \{typeOf actual}"

185 | unexpected : Value v obj => Parser v a

186 | unexpected actual = fail $ "unexpected \{typeOf actual}"

188 | export %inline

189 | modifyFailure : (String -> String) -> Result a -> Result a

190 | modifyFailure f = mapFst (map f)

194 | export %inline

195 | prependFailure : String -> Result a -> Result a

196 | prependFailure = modifyFailure . (++)

198 | export %inline

199 | prependContext : String -> Result a -> Result a

200 | prependContext name = prependFailure "parsing \{name} failed, "

202 | export %inline

203 | prependPath : Result a -> JSONPathElement -> Result a

204 | prependPath r elem = mapFst (\(path,s) => (elem :: path,s)) r

206 | export infixr 9 <?>, .:, .:?, .:!

209 | export %inline %deprecate

210 | (<?>) : Result a -> JSONPathElement -> Result a

211 | (<?>) = prependPath

213 | withValue :

214 |      {auto _ : Value v obj}

215 |   -> (type : String)

216 |   -> (v -> Maybe t)

217 |   -> (name : Lazy String)

218 |   -> Parser t a

219 |   -> Parser v a

220 | withValue s get n f val =

221 |   case get val of

222 |     Just v  => f v

223 |     Nothing => prependContext n $ typeMismatch s val

225 | export %inline

226 | withObject : Value v obj => Lazy String -> Parser obj a -> Parser v a

227 | withObject = withValue "Object" getObject

229 | export %inline

230 | withBoolean : Value v obj => Lazy String -> Parser Bool a -> Parser v a

231 | withBoolean = withValue "Boolean" getBoolean

233 | export %inline

234 | withString : Value v obj => Lazy String -> Parser String a -> Parser v a

235 | withString = withValue "String" getString

237 | export %inline

238 | eqString : Value v obj => Lazy String -> String -> Parser v ()

239 | eqString n s = withString n $ \s' =>

240 |   if s == s' then Right () else fail "expected '\{s}' but got '\{s'}'"

242 | export %inline

243 | withDouble : Value v obj => Lazy String -> Parser Double a -> Parser v a

244 | withDouble = withValue "Double" getDouble

246 | export %inline

247 | withInteger : Value v obj => Lazy String -> Parser Integer a -> Parser v a

248 | withInteger = withValue "Integer" getInteger

251 | boundedIntegral :

252 |      {auto _ : Num a}

253 |   -> {auto _ : Value v obj}

254 |   -> Lazy String

255 |   -> (lower : Integer)

256 |   -> (upper : Integer)

257 |   -> Parser v a

258 | boundedIntegral s lo up =

259 |   withInteger s $ \n =>

260 |     if n >= lo && n <= up

261 |       then pure $ fromInteger n

262 |       else fail "integer out of bounds: \{show n}"

264 | export %inline

265 | withArray : Value v obj => Lazy String -> Parser (List v) a -> Parser v a

266 | withArray = withValue "Array" getArray

268 | export %inline

269 | withArrayN :

270 |      {auto _ : Value v obj}

271 |   -> (n : Nat)

272 |   -> Lazy String

273 |   -> Parser (Vect n v) a

274 |   -> Parser v a

275 | withArrayN n = withValue "Array of length \{show n}" (getArrayN n)

279 | explicitParseField :

280 |      {auto _ : Object obj v}

281 |   -> {auto _ : Value v obj}

282 |   -> Parser v a

283 |   -> obj

284 |   -> Parser String a

285 | explicitParseField p o key =

286 |   case lookup key o of

287 |     Nothing => fail "key \{show key} not found"

288 |     Just v  => p v `prependPath` Key key

292 | explicitParseFieldMaybe :

293 |      {auto _ : Object obj v}

294 |   -> {auto _ : Value v obj}

295 |   -> Parser v a

296 |   -> obj

297 |   -> Parser String (Maybe a)

298 | explicitParseFieldMaybe p o key =

299 |   case lookup key o of

300 |     Nothing => Right Nothing

301 |     Just v  =>

302 |       if isNull v then Right Nothing else map Just $ p v `prependPath` Key key

306 | explicitParseFieldMaybe' :

307 |      {auto _ : Object obj v}

308 |   -> {auto _ : Encoder v}

309 |   -> {auto _ : Value v obj}

310 |   -> Parser v a

311 |   -> obj

312 |   -> Parser String a

313 | explicitParseFieldMaybe' p o key =

314 |   case lookup key o of

315 |     Nothing   => p null `prependPath` Key key

316 |     Just v    => p v `prependPath` Key key

325 | export %inline

326 | field : Object obj v => Value v obj => FromJSON a => obj -> Parser String a

327 | field = explicitParseField fromJSON

330 | export %deprecate %inline

331 | (.:) : Object obj v => Value v obj => FromJSON a => obj -> Parser String a

332 | (.:) = field

341 | export %inline

342 | fieldMaybe :

343 |      {auto _ : Object obj v}

344 |   -> {auto _ : FromJSON a}

345 |   -> {auto _ : Value v obj}

346 |   -> obj

347 |   -> Parser String (Maybe a)

348 | fieldMaybe = explicitParseFieldMaybe fromJSON

352 | export %inline

353 | fieldWithDeflt :

354 |      {auto _ : Object obj v}

355 |   -> {auto _ : FromJSON a}

356 |   -> {auto _ : Value v obj}

357 |   -> obj

358 |   -> Lazy a

359 |   -> Parser String a

360 | fieldWithDeflt o v s = fromMaybe v <$> fieldMaybe o s

363 | export %deprecate %inline

364 | (.:?) :

365 |      {auto _ : Object obj v}

366 |   -> {auto _ : FromJSON a}

367 |   -> {auto _ : Value v obj}

368 |   -> obj

369 |   -> Parser String (Maybe a)

370 | (.:?) = fieldMaybe

377 | export %inline

378 | optField :

379 |      {auto _ : Object obj v}

380 |   -> {auto _ : Encoder v}

381 |   -> {auto _ : FromJSON a}

382 |   -> {auto _ : Value v obj}

383 |   -> obj

384 |   -> Parser String a

385 | optField = explicitParseFieldMaybe' fromJSON

388 | export %deprecate %inline

389 | (.:!) :

390 |      {auto _ : Object obj v}

391 |   -> {auto _ : Encoder v}

392 |   -> {auto _ : FromJSON a}

393 |   -> {auto _ : Value v obj}

394 |   -> obj

395 |   -> Parser String a

396 | (.:!) = optField

401 | export %deprecate %inline

402 | parseField :

403 |      {auto _ : Object obj v}

404 |   -> {auto _ : FromJSON a}

405 |   -> {auto _ : Value v obj}

406 |   -> obj

407 |   -> Parser String a

408 | parseField = field

413 | export %deprecate %inline

414 | parseFieldMaybe :

415 |      {auto _ : Object obj v}

416 |   -> {auto _ : FromJSON a}

417 |   -> {auto _ : Value v obj}

418 |   -> obj

419 |   -> Parser String (Maybe a)

420 | parseFieldMaybe = fieldMaybe

425 | export %deprecate

426 | parseFieldMaybe' :

427 |      {auto _ : Object obj v}

428 |   -> {auto _ : FromJSON a}

429 |   -> {auto _ : Encoder v}

430 |   -> {auto _ : Value v obj}

431 |   -> obj

432 |   -> Parser String a

433 | parseFieldMaybe' = optField

440 | FromJSON Void where

441 |   fromJSON v = fail "Cannot parse Void"

444 | FromJSON () where

445 |   fromJSON = withArray "()" $

446 |     \case Nil    => pure ()

447 |           _ :: _ => fail "parsing () failed, expected empty list"

450 | FromJSON Bool where

451 |   fromJSON = withBoolean "Bool" pure

454 | FromJSON Double where

455 |   fromJSON = withDouble "Double" pure

458 | FromJSON Bits8 where

459 |   fromJSON = boundedIntegral "Bits8" 0 0xff

462 | FromJSON Bits16 where

463 |   fromJSON = boundedIntegral "Bits16" 0 0xffff

466 | FromJSON Bits32 where

467 |   fromJSON = boundedIntegral "Bits32" 0 0xffffffff

470 | FromJSON Bits64 where

471 |   fromJSON = boundedIntegral "Bits64" 0 0xffffffffffffffff

474 | FromJSON Int where

475 |   fromJSON = boundedIntegral "Int" (-0x8000000000000000) 0x7fffffffffffffff

478 | FromJSON Int8 where

479 |   fromJSON = boundedIntegral "Int8" (-0x80) 0x7f

482 | FromJSON Int16 where

483 |   fromJSON = boundedIntegral "Int16" (-0x8000) 0x7fff

486 | FromJSON Int32 where

487 |   fromJSON = boundedIntegral "Int32" (-0x80000000) 0x7fffffff

490 | FromJSON Int64 where

491 |   fromJSON = boundedIntegral "Int64" (-0x8000000000000000) 0x7fffffffffffffff

494 | FromJSON Nat where

495 |   fromJSON = withInteger "Nat" $ \n =>

496 |     if n >= 0 then pure $ fromInteger n

497 |     else fail #"not a natural number: \#{show n}"#

500 | FromJSON Integer where

501 |   fromJSON = withInteger "Integer" pure

504 | FromJSON String where

505 |   fromJSON = withString "String" pure

508 | FromJSON Char where

509 |   fromJSON = withString "Char" $ \str =>

510 |     case strM str of

511 |       (StrCons c "") => pure c

512 |       _ => fail "expected a string of length 1"

515 | FromJSON a => FromJSON (Maybe a) where

516 |   fromJSON v = if isNull v then pure Nothing else Just <$> fromJSON v

519 | FromJSON a => FromJSON (List a) where

520 |   fromJSON = withArray "List" $ traverse fromJSON

523 | FromJSON a => FromJSON (SnocList a) where

524 |   fromJSON = map ([<] <><) . fromJSON

527 | FromJSON a => FromJSON (List1 a) where

528 |   fromJSON = withArray "List1" $

529 |     \case Nil    => fail "expected non-empty list"

530 |           h :: t => traverse fromJSON (h ::: t)

533 | {n : Nat} -> FromJSON a => FromJSON (Vect n a) where

534 |   fromJSON = withArray "Vect \{show n}" $ \vs =>

535 |     case toVect n vs of

536 |       Just vect => traverse fromJSON vect

537 |       Nothing   => fail "expected list of length \{show n}"

540 | FromJSON a => FromJSON b => FromJSON (Either a b) where

541 |   fromJSON = withObject "Either" $ \o =>

542 |     map Left (field o "Left") `orElse`

543 |     map Right (field o "Right")

546 | FromJSON a => FromJSON b => FromJSON (a, b) where

547 |   fromJSON = withArray "Pair" $

548 |     \case [x,y] => [| MkPair (fromJSON x) (fromJSON y) |]

549 |           _     => fail "expected a pair of values"

551 | readLQ :

552 |      {auto _ : Value v obj}

553 |   -> {auto ps : LQ.All.All (FromJSON . f) ts}

554 |   -> Parser (List v) (LQ.All.All f ts)

555 | readLQ @{_} @{[]} [] = Right []

556 | readLQ @{_} @{_::_} (x :: xs) = [| fromJSON x :: readLQ xs |]

557 | readLQ @{_} @{_::_} [] = fail "list of values too short"

558 | readLQ @{_} @{[]} _    = fail "list of values too long"

560 | readVQ :

561 |      {auto _ : Value v obj}

562 |   -> {auto ps : VQ.All.All (FromJSON . f) ts}

563 |   -> Parser (List v) (VQ.All.All f ts)

564 | readVQ @{_} @{[]} [] = Right []

565 | readVQ @{_} @{_::_} (x :: xs) = [| fromJSON x :: readVQ xs |]

566 | readVQ @{_} @{_::_} [] = fail "list of values too short"

567 | readVQ @{_} @{[]} _    = fail "list of values too long"

570 | LQ.All.All (FromJSON . f) ts => FromJSON (LQ.All.All f ts) where

571 |   fromJSON = withArray "HList" $ readLQ

574 | VQ.All.All (FromJSON . f) ts => FromJSON (VQ.All.All f ts) where

575 |   fromJSON = withArray "HVect" $ readVQ

578 | FromJSON a => FromJSON (SortedMap String a) where

579 |   fromJSON object =

580 |     case pairs <$> getObject object of

581 |          Just props => maybe (fail "expected an object with string keys and values") Right $

582 |                          foldr (\(key, val), sortedMap => pure $ insert key !(eitherToMaybe $ fromJSON val) !sortedMap)

583 |                                (Just SortedMap.empty)

584 |                                props

585 |          Nothing => fail "expected an object"

592 | fromSingleField :

593 |      {auto _ : Object obj v}

594 |   -> {auto _ : Value v obj}

595 |   -> (tpe : Lazy String)

596 |   -> Parser (String,v) a

597 |   -> Parser v a

598 | fromSingleField n f = withObject n $ \o => case pairs o of

599 |   [p] => f p

600 |   _   => fail "expected single field object"

608 | fromTwoElemArray :

609 |      {auto _ : Object obj v}

610 |   -> {auto _ : Value v obj}

611 |   -> (tpe : Lazy String)

612 |   -> Parser (String,v) a

613 |   -> Parser v a

614 | fromTwoElemArray n f =

615 |   withArrayN 2 n $ \[x,y] => withString n (\s => f (s,y)) x

623 | fromTaggedObject :

624 |      {auto _ : Object obj v}

625 |   -> {auto _ : Value v obj}

626 |   -> (tpe : Lazy String)

627 |   -> (tagField, contentField : String)

628 |   -> Parser (String,v) a

629 |   -> Parser v a

630 | fromTaggedObject n tf cf f = withObject n $ \o => do

631 |   s <- field o tf

632 |   v <- explicitParseField pure o cf

633 |   f (s,v)