
   0 | ||| Interface and utilities for marshalling Idris2 values from JSON
   1 | ||| via an intermediate `Value` representation.
   2 | |||
   3 | ||| For regular algebraic data types, implementations can automatically
   4 | ||| be derived using elaborator reflection (see module `Derive.FromJSON`)
   5 | |||
   6 | ||| Operators and functionality strongly influenced by Haskell's aeson
   7 | ||| library
   8 | module JSON.Simple.FromJSON
   9 | 
  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
  15 | import JSON.Parser
  16 | import JSON.Simple.Option
  17 | import JSON.Simple.ToJSON
  18 | import Text.ILex
  19 | import Text.ILex.State.Regular
  20 | 
  21 | %language ElabReflection
  22 | 
  23 | %default total
  24 | 
  25 | --------------------------------------------------------------------------------
  26 | --          Types
  27 | --------------------------------------------------------------------------------
  28 | 
  29 | public export
  30 | data JSONPathElement = Key String | Index Bits32
  31 | 
  32 | %runElab derive "JSONPathElement" [Show,Eq]
  33 | 
  34 | public export
  35 | JSONPath : Type
  36 | JSONPath = List JSONPathElement
  37 | 
  38 | public export
  39 | JSONErr : Type
  40 | JSONErr = (JSONPath,String)
  41 | 
  42 | public export
  43 | Result : Type -> Type
  44 | Result = Either JSONErr
  45 | 
  46 | public export
  47 | Parser : Type -> Type -> Type
  48 | Parser v a = v -> Either JSONErr a
  49 | 
  50 | public export
  51 | orElse : Either a b -> Lazy (Either a b) -> Either a b
  52 | orElse r@(Right _) _ = r
  53 | orElse _           v = v
  54 | 
  55 | public export
  56 | (<|>) : Parser v a -> Parser v a -> Parser v a
  57 | f <|> g = \vv => f vv `orElse` g vv
  58 | 
  59 | public export
  60 | data DecodingErr : Type where
  61 |   JErr      : JSONErr -> DecodingErr
  62 |   JParseErr : ParseError Void -> DecodingErr
  63 | 
  64 | %runElab derive "DecodingErr" [Show,Eq]
  65 | 
  66 | public export
  67 | DecodingResult : Type -> Type
  68 | DecodingResult = Either DecodingErr
  69 | 
  70 | --------------------------------------------------------------------------------
  71 | --          Error Formatting
  72 | --------------------------------------------------------------------------------
  73 | 
  74 | ||| Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String'
  75 | ||| which represents the path relative to some root object.
  76 | export
  77 | formatRelativePath : JSONPath -> String
  78 | formatRelativePath path = format "" path
  79 |   where
  80 |     isIdentifierKey : List Char -> Bool
  81 |     isIdentifierKey []      = False
  82 |     isIdentifierKey (x::xs) = isAlpha x && all isAlphaNum xs
  83 | 
  84 |     escapeChar : Char -> String
  85 |     escapeChar '\'' = "\\'"
  86 |     escapeChar '\\' = "\\\\"
  87 |     escapeChar c    = singleton c
  88 | 
  89 |     escapeKey : List Char -> String
  90 |     escapeKey = fastConcat . map escapeChar
  91 | 
  92 |     formatKey : String -> String
  93 |     formatKey key =
  94 |       let chars = fastUnpack key
  95 |        in if isIdentifierKey chars then fastPack $ '.' :: chars
  96 |           else "['" ++ escapeKey chars ++ "']"
  97 | 
  98 |     format : String -> JSONPath -> String
  99 |     format pfx []                = pfx
 100 |     format pfx (Index idx :: parts) = format (pfx ++ "[" ++ show idx ++ "]") parts
 101 |     format pfx (Key key :: parts)   = format (pfx ++ formatKey key) parts
 102 | 
 103 | ||| Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String',
 104 | ||| representing the root object as @$@.
 105 | export
 106 | formatPath : JSONPath -> String
 107 | formatPath path = "$" ++ formatRelativePath path
 108 | 
 109 | ||| Annotate an error message with a
 110 | ||| <http://goessner.net/articles/JsonPath/ JSONPath> error location.
 111 | export
 112 | formatError : JSONPath -> String -> String
 113 | formatError path msg = "Error in " ++ formatPath path ++ ": " ++ msg
 114 | 
 115 | export
 116 | Interpolation DecodingErr where
 117 |   interpolate (JErr (p,s))  = formatError p s
 118 |   interpolate (JParseErr x) = interpolate x
 119 | 
 120 | ||| Pretty prints a decoding error. In case of a parsing error,
 121 | ||| this might be printed on several lines.
 122 | |||
 123 | ||| DEPRECATED: Use `interpolate` instead
 124 | export %deprecate
 125 | prettyErr : (input : String) -> DecodingErr -> String
 126 | prettyErr _ = interpolate
 127 | 
 128 | --------------------------------------------------------------------------------
 129 | --          Interface
 130 | --------------------------------------------------------------------------------
 131 | 
 132 | public export
 133 | interface FromJSON a  where
 134 |   constructor MkFromJSON
 135 |   fromJSON : Parser JSON a
 136 | 
 137 | public export
 138 | interface FromJSONKey a  where
 139 |   constructor MkFromJSONKey
 140 |   fromKey : Parser String a
 141 | 
 142 | export %inline
 143 | decode : FromJSON a => String -> DecodingResult a
 144 | decode s =
 145 |   let Right json := parseJSON Virtual s | Left err => Left (JParseErr err)
 146 |       Right res  := fromJSON json       | Left p   => Left (JErr p)
 147 |    in Right res
 148 | 
 149 | export %inline
 150 | decodeEither : FromJSON a => String -> Either String a
 151 | decodeEither s = mapFst interpolate $ decode s
 152 | 
 153 | export %inline
 154 | decodeMaybe : FromJSON a => String -> Maybe a
 155 | decodeMaybe = either (const Nothing) Just . decode
 156 | 
 157 | --------------------------------------------------------------------------------
 158 | --          Parsing Utilities
 159 | --------------------------------------------------------------------------------
 160 | 
 161 | export
 162 | typeOf : JSON -> String
 163 | typeOf JNull        = "Null"
 164 | typeOf (JBool _)    = "Boolean"
 165 | typeOf (JDouble _)  = "Double"
 166 | typeOf (JInteger _)  = "Integer"
 167 | typeOf (JString _)  = "String"
 168 | typeOf (JArray _)   = "Array"
 169 | typeOf (JObject _)  = "Object"
 170 | 
 171 | export %inline
 172 | fail : String -> Result a
 173 | fail s = Left (Nil,s)
 174 | 
 175 | typeMismatch : String -> Parser JSON a
 176 | typeMismatch expected actual =
 177 |   fail $ "expected \{expected}, but encountered \{typeOf actual}"
 178 | 
 179 | unexpected : Parser JSON a
 180 | unexpected actual = fail $ "unexpected \{typeOf actual}"
 181 | 
 182 | export %inline
 183 | modifyFailure : (String -> String) -> Result a -> Result a
 184 | modifyFailure f = mapFst (map f)
 185 | 
 186 | ||| If the inner 'Parser' failed, prepend the given string to the failure
 187 | ||| message.
 188 | export %inline
 189 | prependFailure : String -> Result a -> Result a
 190 | prependFailure = modifyFailure . (++)
 191 | 
 192 | export %inline
 193 | prependContext : String -> Result a -> Result a
 194 | prependContext name = prependFailure "parsing \{name} failed, "
 195 | 
 196 | export %inline
 197 | prependPath : Result a -> JSONPathElement -> Result a
 198 | prependPath r elem = mapFst (\(path,s) => (elem :: path,s)) r
 199 | 
 200 | withValue :
 201 |      (type : String)
 202 |   -> (JSON -> Maybe t)
 203 |   -> (name : Lazy String)
 204 |   -> Parser t a
 205 |   -> Parser JSON a
 206 | withValue s get n f val =
 207 |   case get val of
 208 |     Just v  => f v
 209 |     Nothing => prependContext n $ typeMismatch s val
 210 | 
 211 | export %inline
 212 | withKey : Parser String a -> Parser String a
 213 | withKey f = prependFailure "parsing key failed, " . f
 214 | 
 215 | export %inline
 216 | withObject : Lazy String -> Parser (List (String,JSON)) a -> Parser JSON a
 217 | withObject = withValue "Object" $ \case JObject ps => Just ps; _ => Nothing
 218 | 
 219 | export %inline
 220 | withBoolean : Lazy String -> Parser Bool a -> Parser JSON a
 221 | withBoolean = withValue "Boolean" $ \case JBool b => Just b; _ => Nothing
 222 | 
 223 | export %inline
 224 | withString : Lazy String -> Parser String a -> Parser JSON a
 225 | withString = withValue "String" $ \case JString s => Just s; _ => Nothing
 226 | 
 227 | export
 228 | withNull : String -> t -> Parser JSON t
 229 | withNull s x JNull = Right x
 230 | withNull s _ v     =
 231 |   prependContext s $ fail "expexted Null but encountered \{typeOf v}"
 232 | 
 233 | export %inline
 234 | eqString : Lazy String -> String -> Parser JSON ()
 235 | eqString n s = withString n $ \s' =>
 236 |   if s == s' then Right () else fail "expected '\{s}' but got '\{s'}'"
 237 | 
 238 | export %inline
 239 | withDouble : Lazy String -> Parser Double a -> Parser JSON a
 240 | withDouble =
 241 |   withValue "Double" $ \case
 242 |     JDouble d  => Just d
 243 |     JInteger n => Just (cast n)
 244 |     _          => Nothing
 245 | 
 246 | export
 247 | withInteger : Lazy String -> Parser Integer a -> Parser JSON a
 248 | withInteger = withValue "Integer" $ \case JInteger d => Just d; _ => Nothing
 249 | 
 250 | -- Value parser for integers
 251 | pint1 : PVal1 q Void Integer
 252 | pint1 = value Nothing [(decimal, bytes decimal)]
 253 | 
 254 | export
 255 | withIntegerKey : Parser Integer a -> Parser String a
 256 | withIntegerKey f =
 257 |   withKey $ \s =>
 258 |     case parseString pint1 Virtual s of
 259 |       Right v => f v
 260 |       Left  _ => fail "not an integer: \{s}"
 261 | 
 262 | export
 263 | boundedIntegral :
 264 |      {auto _ : Num a}
 265 |   -> Lazy String
 266 |   -> (lower : Integer)
 267 |   -> (upper : Integer)
 268 |   -> Parser JSON a
 269 | boundedIntegral s lo up =
 270 |   withInteger s $ \n =>
 271 |     if n >= lo && n <= up
 272 |        then Right $ fromInteger n
 273 |        else fail "integer out of bounds: \{show n}"
 274 | 
 275 | export
 276 | boundedIntegralKey :
 277 |      {auto _ : Num a}
 278 |   -> (lower : Integer)
 279 |   -> (upper : Integer)
 280 |   -> Parser String a
 281 | boundedIntegralKey lo up =
 282 |   withIntegerKey $ \n =>
 283 |     if n >= lo && n <= up
 284 |        then Right $ fromInteger n
 285 |        else fail "integer out of bounds: \{show n}"
 286 | 
 287 | export
 288 | withArray : Lazy String -> Parser (List JSON) a -> Parser JSON a
 289 | withArray = withValue "Array" $ \case JArray v => Just v; _ => Nothing
 290 | 
 291 | export
 292 | withArrayN :
 293 |      (n : Nat)
 294 |   -> Lazy String
 295 |   -> Parser (Vect n JSON) a
 296 |   -> Parser JSON a
 297 | withArrayN n = withValue "Array of length \{show n}" $
 298 |   \case JArray v => toVect n v; _ => Nothing
 299 | 
 300 | ||| See `field`
 301 | export
 302 | explicitParseField : Parser JSON a -> List (String,JSON) -> Parser String a
 303 | explicitParseField p o key =
 304 |   case lookup key o of
 305 |     Nothing => fail "key \{show key} not found"
 306 |     Just v  => p v `prependPath` Key key
 307 | 
 308 | ||| See `fieldMaybe`
 309 | export
 310 | explicitParseFieldMaybe :
 311 |      Parser JSON a
 312 |   -> List (String,JSON)
 313 |   -> Parser String (Maybe a)
 314 | explicitParseFieldMaybe p o key =
 315 |   case lookup key o of
 316 |     Nothing    => Right Nothing
 317 |     Just JNull => Right Nothing
 318 |     Just v     => map Just $ p v `prependPath` Key key
 319 | 
 320 | ||| See `optField`
 321 | export
 322 | explicitParseFieldMaybe' :
 323 |      Parser JSON a
 324 |   -> List (String,JSON)
 325 |   -> Parser String a
 326 | explicitParseFieldMaybe' p o key =
 327 |   case lookup key o of
 328 |     Nothing => p JNull `prependPath` Key key
 329 |     Just v  => p v `prependPath` Key key
 330 | 
 331 | ||| Retrieve the value associated with the given key of an `IObject`.
 332 | ||| The result is `empty` if the key is not present or the value cannot
 333 | ||| be converted to the desired type.
 334 | |||
 335 | ||| This accessor is appropriate if the key and value /must/ be present
 336 | ||| in an object for it to be valid.  If the key and value are
 337 | ||| optional, use `optField` instead.
 338 | export %inline
 339 | field : FromJSON a => List (String,JSON) -> Parser String a
 340 | field = explicitParseField fromJSON
 341 | 
 342 | ||| Retrieve the value associated with the given key of an `IObject`. The
 343 | ||| result is `Nothing` if the key is not present or if its value is `Null`,
 344 | ||| or `empty` if the value cannot be converted to the desired type.
 345 | |||
 346 | ||| This accessor is most useful if the key and value can be absent
 347 | ||| from an object without affecting its validity.  If the key and
 348 | ||| value are mandatory, use `field` instead.
 349 | export %inline
 350 | fieldMaybe : FromJSON a => List (String,JSON) -> Parser String (Maybe a)
 351 | fieldMaybe = explicitParseFieldMaybe fromJSON
 352 | 
 353 | ||| Retrieve the value associated with the given key of an `IObject`
 354 | ||| passing on `Null` in case the given key is missing.
 355 | |||
 356 | ||| This differs from `fieldMaybe` in that it can be used with any converter
 357 | ||| accepting `Null` as an input.
 358 | export %inline
 359 | optField : FromJSON a => List (String,JSON) -> Parser String a
 360 | optField = explicitParseFieldMaybe' fromJSON
 361 | 
 362 | ||| Retrieve the value associated with the given key of an `IObject`
 363 | ||| using the given default value in case the key is missing.
 364 | export %inline
 365 | fieldWithDeflt : FromJSON a => List (String,JSON) -> Lazy a -> Parser String a
 366 | fieldWithDeflt ps v s = fromMaybe v <$> fieldMaybe ps s
 367 | 
 368 | --------------------------------------------------------------------------------
 369 | --          Implementations
 370 | --------------------------------------------------------------------------------
 371 | 
 372 | export
 373 | FromJSON JSON where fromJSON = Right
 374 | 
 375 | export
 376 | FromJSON Void where
 377 |   fromJSON v = fail "Cannot parse Void"
 378 | 
 379 | export
 380 | FromJSON () where
 381 |   fromJSON = withArray "()" $
 382 |     \case Nil    => Right ()
 383 |           _ :: _ => fail "parsing () failed, expected empty list"
 384 | 
 385 | export
 386 | FromJSON Bool where
 387 |   fromJSON = withBoolean "Bool" Right
 388 | 
 389 | export
 390 | FromJSONKey Bool where
 391 |   fromKey =
 392 |     withKey $
 393 |       \case "True"  => Right True
 394 |             "False" => Right False
 395 |             s       => fail "not a bool: \{s}"
 396 | 
 397 | export
 398 | FromJSON Double where
 399 |   fromJSON = withDouble "Double" Right
 400 | 
 401 | -- Value parser for floating point numbers
 402 | pdbl1 : PVal1 q Void Double
 403 | pdbl1 = value Nothing [(jsonDouble, txt jdouble)]
 404 | 
 405 | export
 406 | FromJSONKey Double where
 407 |   fromKey =
 408 |     withKey $ \s =>
 409 |       case parseString pdbl1 Virtual s of
 410 |         Right v => Right v
 411 |         Left  _ => fail "not a floating point number: \{s}"
 412 | 
 413 | export
 414 | FromJSON Bits8 where
 415 |   fromJSON = boundedIntegral "Bits8" 0 0xff
 416 | 
 417 | export
 418 | FromJSON Bits16 where
 419 |   fromJSON = boundedIntegral "Bits16" 0 0xffff
 420 | 
 421 | export
 422 | FromJSON Bits32 where
 423 |   fromJSON = boundedIntegral "Bits32" 0 0xffffffff
 424 | 
 425 | export
 426 | FromJSON Bits64 where
 427 |   fromJSON = boundedIntegral "Bits64" 0 0xffffffffffffffff
 428 | 
 429 | export
 430 | FromJSON Int where
 431 |   fromJSON = boundedIntegral "Int" (-0x8000000000000000) 0x7fffffffffffffff
 432 | 
 433 | export
 434 | FromJSON Int8 where
 435 |   fromJSON = boundedIntegral "Int8" (-0x80) 0x7f
 436 | 
 437 | export
 438 | FromJSON Int16 where
 439 |   fromJSON = boundedIntegral "Int16" (-0x8000) 0x7fff
 440 | 
 441 | export
 442 | FromJSON Int32 where
 443 |   fromJSON = boundedIntegral "Int32" (-0x80000000) 0x7fffffff
 444 | 
 445 | export
 446 | FromJSON Int64 where
 447 |   fromJSON = boundedIntegral "Int64" (-0x8000000000000000) 0x7fffffffffffffff
 448 | 
 449 | export
 450 | FromJSONKey Bits8 where
 451 |   fromKey = boundedIntegralKey 0 0xff
 452 | 
 453 | export
 454 | FromJSONKey Bits16 where
 455 |   fromKey = boundedIntegralKey 0 0xffff
 456 | 
 457 | export
 458 | FromJSONKey Bits32 where
 459 |   fromKey = boundedIntegralKey 0 0xffffffff
 460 | 
 461 | export
 462 | FromJSONKey Bits64 where
 463 |   fromKey = boundedIntegralKey 0 0xffffffffffffffff
 464 | 
 465 | export
 466 | FromJSONKey Int where
 467 |   fromKey = boundedIntegralKey (-0x8000000000000000) 0x7fffffffffffffff
 468 | 
 469 | export
 470 | FromJSONKey Int8 where
 471 |   fromKey = boundedIntegralKey (-0x80) 0x7f
 472 | 
 473 | export
 474 | FromJSONKey Int16 where
 475 |   fromKey = boundedIntegralKey (-0x8000) 0x7fff
 476 | 
 477 | export
 478 | FromJSONKey Int32 where
 479 |   fromKey = boundedIntegralKey (-0x80000000) 0x7fffffff
 480 | 
 481 | export
 482 | FromJSONKey Int64 where
 483 |   fromKey = boundedIntegralKey (-0x8000000000000000) 0x7fffffffffffffff
 484 | 
 485 | export
 486 | FromJSON Nat where
 487 |   fromJSON = withInteger "Nat" $ \n =>
 488 |     if n >= 0 then Right $ fromInteger n
 489 |     else fail "not a natural number: \{show n}"
 490 | 
 491 | export
 492 | FromJSONKey Nat where
 493 |   fromKey = withIntegerKey $ \n =>
 494 |     if n >= 0 then Right $ fromInteger n
 495 |     else fail "not a natural number: \{show n}"
 496 | 
 497 | export %inline
 498 | FromJSON Integer where
 499 |   fromJSON = withInteger "Integer" Right
 500 | 
 501 | export %inline
 502 | FromJSONKey Integer where
 503 |   fromKey = withIntegerKey Right
 504 | 
 505 | export %inline
 506 | FromJSON String where
 507 |   fromJSON = withString "String" Right
 508 | 
 509 | export %inline
 510 | FromJSONKey String where
 511 |   fromKey = withKey Right
 512 | 
 513 | export
 514 | FromJSON Char where
 515 |   fromJSON = withString "Char" $ \str =>
 516 |     case strM str of
 517 |       StrCons c "" => Right c
 518 |       _            => fail "expected a string of length 1"
 519 | 
 520 | export
 521 | FromJSONKey Char where
 522 |   fromKey = withKey $ \str =>
 523 |     case strM str of
 524 |       StrCons c "" => Right c
 525 |       _            => fail "expected a string of length 1"
 526 | 
 527 | export
 528 | FromJSON a => FromJSON (Maybe a) where
 529 |   fromJSON JNull = Right Nothing
 530 |   fromJSON v     = Just <$> fromJSON v
 531 | 
 532 | export
 533 | FromJSON a => FromJSON (List a) where
 534 |   fromJSON = withArray "List" $ traverse fromJSON
 535 | 
 536 | export
 537 | FromJSON a => FromJSON (SnocList a) where
 538 |   fromJSON = map ([<] <><) . fromJSON
 539 | 
 540 | export
 541 | FromJSON a => FromJSON (List1 a) where
 542 |   fromJSON = withArray "List1" $ \case
 543 |     Nil    => fail "expected non-empty list"
 544 |     h :: t => traverse fromJSON (h ::: t)
 545 | 
 546 | export
 547 | {v : a} -> FromJSON a => ToJSON a => Eq a => FromJSON (Singleton v) where
 548 |   fromJSON x =
 549 |     fromJSON x >>= \val => case v == val of
 550 |       True  => Right (Val v)
 551 |       False => fail "Invalid value. Expected \{encode v}"
 552 | 
 553 | sortedMap :
 554 |      {auto ord : Ord k}
 555 |   -> {auto jk  : FromJSONKey k}
 556 |   -> {auto jv  : FromJSON v}
 557 |   -> SortedMap k v
 558 |   -> Parser (List (String,JSON)) (SortedMap k v)
 559 | sortedMap m []            = Right m
 560 | sortedMap m ((x,y) :: ps) =
 561 |   let Right k' := fromKey x  | Left err => Left err
 562 |       Right v' := fromJSON y | Left err => Left err
 563 |    in sortedMap (insert k' v' m) ps
 564 | 
 565 | export %inline
 566 | Ord k => FromJSONKey k => FromJSON v => FromJSON (SortedMap k v) where
 567 |   fromJSON = withObject "SortedMap" (sortedMap empty)
 568 | 
 569 | export
 570 | {n : Nat} -> FromJSON a => FromJSON (Vect n a) where
 571 |   fromJSON = withArray "Vect \{show n}" $ \vs => case toVect n vs of
 572 |     Just vect => traverse fromJSON vect
 573 |     Nothing   => fail "expected list of length \{show n}"
 574 | 
 575 | export
 576 | FromJSON a => FromJSON b => FromJSON (Either a b) where
 577 |   fromJSON = withObject "Either" $ \o =>
 578 |     map Left (field o "Left") `orElse`
 579 |     map Right (field o "Right")
 580 | 
 581 | export
 582 | FromJSON a => FromJSON b => FromJSON (a, b) where
 583 |   fromJSON = withArray "Pair" $
 584 |     \case [x,y] => [| MkPair (fromJSON x) (fromJSON y) |]
 585 |           _     => fail "expected a pair of values"
 586 | 
 587 | readLQ : (ps : LQ.All.All (FromJSON . f) ts) => Parser (List JSON) (All f ts)
 588 | readLQ @{[]} [] = Right []
 589 | readLQ @{_::_} (x :: xs) = [| fromJSON x :: readLQ xs |]
 590 | readLQ @{_::_} [] = fail "list of values too short"
 591 | readLQ @{[]} _    = fail "list of values too long"
 592 | 
 593 | readVQ : (ps : VQ.All.All (FromJSON . f) ts) => Parser (List JSON) (All f ts)
 594 | readVQ @{[]} [] = Right []
 595 | readVQ @{_::_} (x :: xs) = [| fromJSON x :: readVQ xs |]
 596 | readVQ @{_::_} [] = fail "list of values too short"
 597 | readVQ @{[]} _    = fail "list of values too long"
 598 | 
 599 | export
 600 | LQ.All.All (FromJSON . f) ts => FromJSON (All f ts) where
 601 |   fromJSON = withArray "HList" $ readLQ
 602 | 
 603 | export
 604 | VQ.All.All (FromJSON . f) ts => FromJSON (VQ.All.All f ts) where
 605 |   fromJSON = withArray "HVect" $ readVQ
 606 | 
 607 | ||| Tries to decode a value encoded as a single field object of the given name.
 608 | |||
 609 | ||| This corresponds to the `ObjectWithSingleField` option
 610 | ||| for encoding sum types.
 611 | export
 612 | fromSingleField :
 613 |      (tpe : Lazy String)
 614 |   -> Parser (String,JSON) a
 615 |   -> Parser JSON a
 616 | fromSingleField n f = withObject n $
 617 |   \case [p] => f p
 618 |         _   => fail "expected single field object"
 619 | 
 620 | ||| Tries to decode a value encoded as a two-element array with the given
 621 | ||| constructor name.
 622 | |||
 623 | ||| This corresponds to the `TwoElemArray` option
 624 | ||| for encoding sum types.
 625 | export
 626 | fromTwoElemArray :
 627 |      (tpe : Lazy String)
 628 |   -> Parser (String,JSON) a
 629 |   -> Parser JSON a
 630 | fromTwoElemArray n f =
 631 |   withArrayN 2 n $ \[x,y] => withString n (\s => f (s,y)) x
 632 | 
 633 | ||| Tries to decode a value encoded as a tagged object with the given
 634 | ||| tag and content field, plus tag value.
 635 | |||
 636 | ||| This corresponds to the `TaggedObject` option
 637 | ||| for encoding sum types.
 638 | export
 639 | fromTaggedObject :
 640 |      (tpe : Lazy String)
 641 |   -> (tagField, contentField : String)
 642 |   -> Parser (String,JSON) a
 643 |   -> Parser JSON a
 644 | fromTaggedObject n tf cf f = withObject n $ \o => do
 645 |   s <- field o tf
 646 |   v <- explicitParseField Right o cf
 647 |   f (s,v)
 648 |