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