JSON.FromJSON

Interface and utilities for marshalling Idris2 values from JSON
via an intermediate `Value` representation.

For regular algebraic data types, implementations can automatically
be derived using elaborator reflection.

Operators and functionality strongly influenced by Haskell's aeson
library

Definitions

data JSONPathElement : Type

Totality: total
Visibility: public export
Constructors:

Key : String -> JSONPathElement

Index : Bits32 -> JSONPathElement

Hints:

Eq JSONPathElement

Generic JSONPathElement [[String], [Bits32]]

Meta JSONPathElement [[String], [Bits32]]

Show JSONPathElement

JSONPath : Type

Visibility: public export

JSONErr : Type

Visibility: public export

Result : Type -> Type

Visibility: public export

Parser : Type -> Type -> Type

Visibility: public export

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

Visibility: public export

data DecodingErr : Type

Totality: total
Visibility: public export
Constructors:

JErr : JSONErr -> DecodingErr

JParseErr : ParseErr -> DecodingErr

Hints:

Eq DecodingErr

Generic DecodingErr [[JSONErr], [ParseErr]]

Meta DecodingErr [[JSONErr], [ParseErr]]

Show DecodingErr

DecodingResult : Type -> Type

Visibility: public export

formatRelativePath : JSONPath -> String

  Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String'
  which represents the path relative to some root object.

Visibility: export

formatPath : JSONPath -> String

  Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String',
  representing the root object as @$@.

Visibility: export

formatError : JSONPath -> String -> String

  Annotate an error message with a
  <http://goessner.net/articles/JsonPath/ JSONPath> error location.

Visibility: export

prettyErr : String -> DecodingErr -> String

  Pretty prints a decoding error. In case of a parsing error,
  this might be printed on several lines.

Visibility: export

interface FromJSON : Type -> Type

Parameters: a
Constructor: MkFromJSON
Methods:

fromJSON : Value v obj => Parser v a

Implementations:

FromJSON Void

FromJSON ()

FromJSON Bool

FromJSON Double

FromJSON Bits8

FromJSON Bits16

FromJSON Bits32

FromJSON Bits64

FromJSON Int

FromJSON Int8

FromJSON Int16

FromJSON Int32

FromJSON Int64

FromJSON Nat

FromJSON Integer

FromJSON String

FromJSON Char

FromJSON a => FromJSON (Maybe a)

FromJSON a => FromJSON (List a)

FromJSON a => FromJSON (List1 a)

FromJSON a => FromJSON (Vect n a)

(FromJSON a, FromJSON b) => FromJSON (Either a b)

NP (FromJSON . f) ks => FromJSON (NP f ks)

(FromJSON a, FromJSON b) => FromJSON (a, b)

NP (FromJSON . f) ks => FromJSON (NS f ks)

fromJSON : FromJSON a => Value v obj => Parser v a

Visibility: public export

decodeVia : (0 v : Type) -> Value v obj => FromJSON a => String -> DecodingResult a

Visibility: export

decodeEitherVia : (0 v : Type) -> Value v obj => FromJSON a => String -> Either String a

Visibility: export

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

Visibility: export

decode : FromJSON a => String -> DecodingResult a

Visibility: export

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

Visibility: export

decodeMaybe : FromJSON a => String -> Maybe a

Visibility: export

fail : String -> Result a

Visibility: export

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

Visibility: export

prependFailure : String -> Result a -> Result a

  If the inner 'Parser' failed, prepend the given string to the failure
  message.

Visibility: export

prependContext : String -> Result a -> Result a

Visibility: export

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

Visibility: export
Fixity Declaration: infixr operator, level 3

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

Visibility: export

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

Visibility: export

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

Visibility: export

withNumber : Value v obj => Lazy String -> Parser Double a -> Parser v a

Visibility: export

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

Visibility: export

withLargeInteger : Value v obj => Lazy String -> Parser Integer a -> Parser v a

Visibility: export

boundedIntegral : Num a => Value v obj => Lazy String -> Integer -> Integer -> Parser v a

Visibility: export

boundedLargeIntegral : Num a => Value v obj => Lazy String -> Integer -> Integer -> Parser v a

Visibility: export

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

Visibility: export

explicitParseField : Object obj v => Value v obj => Parser v a -> obj -> Parser String a

  See `.:`

Visibility: export

explicitParseFieldMaybe : Object obj v => Value v obj => Parser v a -> obj -> Parser String (Maybe a)

  See `.:?`

Visibility: export

explicitParseFieldMaybe' : Object obj v => Value v obj => Parser v a -> obj -> Parser String (Maybe a)

  See `.:!`

Visibility: export

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

  Retrieve the value associated with the given key of an `IObject`.
  The result is `empty` if the key is not present or the value cannot
  be converted to the desired type.
  
  This accessor is appropriate if the key and value /must/ be present
  in an object for it to be valid.  If the key and value are
  optional, use `.:?` instead.

Visibility: export
Fixity Declaration: infixr operator, level 9

(.:?) : Object obj v => Value v obj => FromJSON a => obj -> Parser String (Maybe a)

  Retrieve the value associated with the given key of an `IObject`. The
  result is `Nothing` if the key is not present or if its value is `Null`,
  or `empty` if the value cannot be converted to the desired type.
  
  This accessor is most useful if the key and value can be absent
  from an object without affecting its validity.  If the key and
  value are mandatory, use `.:` instead.

Visibility: export
Fixity Declaration: infixr operator, level 3

(.:!) : Object obj v => Value v obj => FromJSON a => obj -> Parser String (Maybe a)

  Retrieve the value associated with the given key of an `IObject`
  The result is `Nothing` if the key is not present or 'empty' if the
  value cannot be converted to the desired type.
  
  This differs from `.:?` by attempting to parse `Null` the same as any
  other JSON value, instead of interpreting it as `Nothing`.

Visibility: export
Fixity Declaration: infixr operator, level 3

parseField : Object obj v => Value v obj => FromJSON a => obj -> Parser String a

  Function variant of `.:`.

Visibility: export

parseFieldMaybe : Object obj v => Value v obj => FromJSON a => obj -> Parser String (Maybe a)

  Function variant of `.:?`.

Visibility: export

parseFieldMaybe' : Object obj v => Value v obj => FromJSON a => obj -> Parser String (Maybe a)

  Function variant of `.:!`.

Visibility: export

sopNewtype : Value v obj => FromJSON (f k) => Parser v (SOP f [[k]])

  Decodes a newtype-like sum of products
  (exactly one single value constructor) by wrapping
  the decoded value in `MkSOP . Z`.

Visibility: export

sopEnum : Value v obj => TypeInfo' k kss -> {auto 0 _ : EnumType kss} -> Parser v (SOP f kss)

  Decodes an enum-like sum of products
  (only nullary constructors) by trying to extract one of the
  constructors' name

Visibility: export

sopRecord : Value v obj => NP (FromJSON . f) ks => TypeInfo [ks] -> Parser v (SOP f [ks])

  Decodes a single-constructor sum of products. The
  constructor's name is ignored.

Visibility: export

sop : Value v obj => POP (FromJSON . f) kss => SumEncoding -> TypeInfo' k kss -> Parser v (SOP_ k f kss)

  Decodes a sum of products as specified by the passed
  `SumEncoding` (see its documentation for details) using
  the given `TypeInfo` to decode constructor and argument names.
  
  See also `sopRecord` for decoding values with a single constructor,
  `sopEnum` for decoding enum types (only nullary constructors),
  and `sopNewtype` for decoding newtype wrappers.

Visibility: export

genNewtypeFromJSON : Value v obj => Generic a [[k]] => FromJSON k => Parser v a

  Generic version of `sopNewtype`.

Visibility: export

genEnumFromJSON : Value v obj => Meta a kss => {auto 0 _ : EnumType kss} -> Parser v a

  Generic version of `sopEnum`.

Visibility: export

genEnumFromJSON' : Value v obj => Meta a kss => {auto 0 _ : EnumType kss} -> (String -> String) -> Parser v a

  Like `genEnumFromJSON`, but uses the given function to adjust
  constructor names before being used as tags.

Visibility: export

genRecordFromJSON : Value v obj => Meta a [ks] => NP FromJSON ks => Parser v a

  Generic version of `sopRecord`.

Visibility: export

genRecordFromJSON' : Value v obj => Meta a [ks] => NP FromJSON ks => (String -> String) -> Parser v a

  Like `genRecordFromJSON`, but uses the given function to adjust
  field names before being used as tags.

Visibility: export

genFromJSON : Value v obj => Meta a code => POP FromJSON code => SumEncoding -> Parser v a

Visibility: export

genFromJSON' : Value v obj => Meta a code => POP FromJSON code => (String -> String) -> (String -> String) -> SumEncoding -> Parser v a

Visibility: export

customFromJSON : TTImp -> DeriveUtil -> InterfaceImpl

Visibility: export

FromJSON : DeriveUtil -> InterfaceImpl

  Derives a `FromJSON` implementation for the given data type

Visibility: export

RecordFromJSON : DeriveUtil -> InterfaceImpl

  Derives a `FromJSON` implementation for the given single-constructor
  data type

Visibility: export

EnumFromJSON : DeriveUtil -> InterfaceImpl

  Derives a `FromJSON` implementation for the given enum type

Visibility: export

NewtypeFromJSON : DeriveUtil -> InterfaceImpl

  Derives a `FromJSON` implementation for the given newtype

Visibility: export