Idris2Doc : JSON.FromJSON

JSON.FromJSON

(source)
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 (see module `Derive.FromJSON`)

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
Show JSONPathElement
JSONPath : Type
Totality: total
Visibility: public export
JSONErr : Type
Totality: total
Visibility: public export
Result : Type -> Type
Totality: total
Visibility: public export
Parser : Type -> Type -> Type
Totality: total
Visibility: public export
orElse : Either a b -> Lazy (Either a b) -> Either a b
Totality: total
Visibility: public export
(<|>) : Parser v a -> Parser v a -> Parser v a
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 2
data DecodingErr : Type
Totality: total
Visibility: public export
Constructors:
JErr : JSONErr -> DecodingErr
JParseErr : ParseError Void -> DecodingErr

Hints:
Eq DecodingErr
Interpolation DecodingErr
Show DecodingErr
DecodingResult : Type -> Type
Totality: total
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.

Totality: total
Visibility: export
formatPath : JSONPath -> String
  Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String',
  representing the root object as @$@.

Totality: total
Visibility: export
formatError : JSONPath -> String -> String
  Annotate an error message with a
  <http://goessner.net/articles/JsonPath/ JSONPath> error location.

Totality: total
Visibility: export
=DEPRECATED=
prettyErr : String -> DecodingErr -> String
  Pretty prints a decoding error. In case of a parsing error,
  this might be printed on several lines.
  
  DEPRECATED: Use `interpolate` instead

Totality: total
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 (SnocList a)
FromJSON a => FromJSON (List1 a)
FromJSON a => FromJSON (Vect n a)
FromJSON a => FromJSON b => FromJSON (Either a b)
FromJSON a => FromJSON b => FromJSON (a, b)
All (FromJSON . f) ts => FromJSON (All f ts)
All (FromJSON . f) ts => FromJSON (All f ts)
FromJSON a => FromJSON (SortedMap String a)
fromJSON : FromJSON a => Value v obj => Parser v a
Totality: total
Visibility: public export
decodeVia : (0 v : Type) -> Value v obj => FromJSON a => String -> DecodingResult a
Totality: total
Visibility: export
decodeEitherVia : (0 v : Type) -> Value v obj => FromJSON a => String -> Either String a
Totality: total
Visibility: export
decodeMaybeVia : (0 v : Type) -> Value v obj => FromJSON a => String -> Maybe a
Totality: total
Visibility: export
decode : FromJSON a => String -> DecodingResult a
Totality: total
Visibility: export
decodeEither : FromJSON a => String -> Either String a
Totality: total
Visibility: export
decodeMaybe : FromJSON a => String -> Maybe a
Totality: total
Visibility: export
fail : String -> Result a
Totality: total
Visibility: export
modifyFailure : (String -> String) -> Result a -> Result a
Totality: total
Visibility: export
prependFailure : String -> Result a -> Result a
  If the inner 'Parser' failed, prepend the given string to the failure
  message.

Totality: total
Visibility: export
prependContext : String -> Result a -> Result a
Totality: total
Visibility: export
prependPath : Result a -> JSONPathElement -> Result a
Totality: total
Visibility: export
=DEPRECATED=
(<?>) : Result a -> JSONPathElement -> Result a
  Deprecated: Use `prependPath` instead.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 9
withObject : Value v obj => Lazy String -> Parser obj a -> Parser v a
Totality: total
Visibility: export
withBoolean : Value v obj => Lazy String -> Parser Bool a -> Parser v a
Totality: total
Visibility: export
withString : Value v obj => Lazy String -> Parser String a -> Parser v a
Totality: total
Visibility: export
eqString : Value v obj => Lazy String -> String -> Parser v ()
Totality: total
Visibility: export
withDouble : Value v obj => Lazy String -> Parser Double a -> Parser v a
Totality: total
Visibility: export
withInteger : Value v obj => Lazy String -> Parser Integer a -> Parser v a
Totality: total
Visibility: export
boundedIntegral : Num a => Value v obj => Lazy String -> Integer -> Integer -> Parser v a
Totality: total
Visibility: export
withArray : Value v obj => Lazy String -> Parser (List v) a -> Parser v a
Totality: total
Visibility: export
withArrayN : Value v obj => (n : Nat) -> Lazy String -> Parser (Vect n v) a -> Parser v a
Totality: total
Visibility: export
explicitParseField : Object obj v => Value v obj => Parser v a -> obj -> Parser String a
  See `field`

Totality: total
Visibility: export
explicitParseFieldMaybe : Object obj v => Value v obj => Parser v a -> obj -> Parser String (Maybe a)
  See `fieldMaybe`

Totality: total
Visibility: export
explicitParseFieldMaybe' : Object obj v => Encoder v => Value v obj => Parser v a -> obj -> Parser String a
  See `optField`

Totality: total
Visibility: export
field : 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 `optField` instead.

Totality: total
Visibility: export
=DEPRECATED=
(.:) : Object obj v => Value v obj => FromJSON a => obj -> Parser String a
  Deprecated: Use `field` instead

Totality: total
Visibility: export
Fixity Declarations:
infixr operator, level 9
infixr operator, level 9
fieldMaybe : Object obj v => FromJSON a => Value v obj => 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 `field` instead.

Totality: total
Visibility: export
fieldWithDeflt : Object obj v => FromJSON a => Value v obj => obj -> Lazy a -> Parser String a
  Retrieve the value associated with the given key of an `Object`
  using the given default value in case the key is missing.

Totality: total
Visibility: export
=DEPRECATED=
(.:?) : Object obj v => FromJSON a => Value v obj => obj -> Parser String (Maybe a)
  Deprecated: Use `fieldMaybe` instead

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 9
optField : Object obj v => Encoder v => FromJSON a => Value v obj => obj -> Parser String a
  Retrieve the value associated with the given key of an `IObject`
  passing on `Null` in case the given key is missing.
  
  This differs from `fieldMaybe` in that it can be used with any converter
  accepting `Null` as an input.

Totality: total
Visibility: export
=DEPRECATED=
(.:!) : Object obj v => Encoder v => FromJSON a => Value v obj => obj -> Parser String a
  Deprecated: Use `optField` instead

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 9
=DEPRECATED=
parseField : Object obj v => FromJSON a => Value v obj => obj -> Parser String a
  Function variant of `.:`.
  
  Deprecated: Use `field` instead

Totality: total
Visibility: export
=DEPRECATED=
parseFieldMaybe : Object obj v => FromJSON a => Value v obj => obj -> Parser String (Maybe a)
  Function variant of `.:?`.
  
  Deprecated: Use `fieldMaybe` instead

Totality: total
Visibility: export
=DEPRECATED=
parseFieldMaybe' : Object obj v => FromJSON a => Encoder v => Value v obj => obj -> Parser String a
  Function variant of `.:!`.
  
  Deprecated: Use `optField` instead

Totality: total
Visibility: export
fromSingleField : Object obj v => Value v obj => Lazy String -> Parser (String, v) a -> Parser v a
  Tries to decode a value encoded as a single field object of the given name.
  
  This corresponds to the `ObjectWithSingleField` option
  for encoding sum types.

Totality: total
Visibility: export
fromTwoElemArray : Object obj v => Value v obj => Lazy String -> Parser (String, v) a -> Parser v a
  Tries to decode a value encoded as a two-element array with the given
  constructor name.
  
  This corresponds to the `TwoElemArray` option
  for encoding sum types.

Totality: total
Visibility: export
fromTaggedObject : Object obj v => Value v obj => Lazy String -> String -> String -> Parser (String, v) a -> Parser v a
  Tries to decode a value encoded as a tagged object with the given
  tag and content field, plus tag value.
  
  This corresponds to the `TaggedObject` option
  for encoding sum types.

Totality: total
Visibility: export