JSON.Simple.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 (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 : Parser JSON a

Implementations:

FromJSON JSON

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 => ToJSON a => Eq a => FromJSON (Singleton v)

Ord k => FromJSONKey k => FromJSON v => FromJSON (SortedMap k v)

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 : FromJSON a => Parser JSON a

Totality: total
Visibility: public export

interface FromJSONKey : Type -> Type

Parameters: a
Constructor: 

MkFromJSONKey

Methods:

fromKey : Parser String a

Implementations:

FromJSONKey Bool

FromJSONKey Double

FromJSONKey Bits8

FromJSONKey Bits16

FromJSONKey Bits32

FromJSONKey Bits64

FromJSONKey Int

FromJSONKey Int8

FromJSONKey Int16

FromJSONKey Int32

FromJSONKey Int64

FromJSONKey Nat

FromJSONKey Integer

FromJSONKey String

FromJSONKey Char

fromKey : FromJSONKey a => Parser String a

Totality: total
Visibility: public 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

typeOf : JSON -> String

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

withKey : Parser String a -> Parser String a

Totality: total
Visibility: export

withObject : Lazy String -> Parser (List (String, JSON)) a -> Parser JSON a

Totality: total
Visibility: export

withBoolean : Lazy String -> Parser Bool a -> Parser JSON a

Totality: total
Visibility: export

withString : Lazy String -> Parser String a -> Parser JSON a

Totality: total
Visibility: export

withNull : String -> t -> Parser JSON t

Totality: total
Visibility: export

eqString : Lazy String -> String -> Parser JSON ()

Totality: total
Visibility: export

withDouble : Lazy String -> Parser Double a -> Parser JSON a

Totality: total
Visibility: export

withInteger : Lazy String -> Parser Integer a -> Parser JSON a

Totality: total
Visibility: export

withIntegerKey : Parser Integer a -> Parser String a

Totality: total
Visibility: export

boundedIntegral : Num a => Lazy String -> Integer -> Integer -> Parser JSON a

Totality: total
Visibility: export

boundedIntegralKey : Num a => Integer -> Integer -> Parser String a

Totality: total
Visibility: export

withArray : Lazy String -> Parser (List JSON) a -> Parser JSON a

Totality: total
Visibility: export

withArrayN : (n : Nat) -> Lazy String -> Parser (Vect n JSON) a -> Parser JSON a

Totality: total
Visibility: export

explicitParseField : Parser JSON a -> List (String, JSON) -> Parser String a

  See `field`

Totality: total
Visibility: export

explicitParseFieldMaybe : Parser JSON a -> List (String, JSON) -> Parser String (Maybe a)

  See `fieldMaybe`

Totality: total
Visibility: export

explicitParseFieldMaybe' : Parser JSON a -> List (String, JSON) -> Parser String a

  See `optField`

Totality: total
Visibility: export

field : FromJSON a => List (String, JSON) -> 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

fieldMaybe : FromJSON a => List (String, JSON) -> 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

optField : FromJSON a => List (String, JSON) -> 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

fieldWithDeflt : FromJSON a => List (String, JSON) -> Lazy a -> Parser String a

  Retrieve the value associated with the given key of an `IObject`
  using the given default value in case the key is missing.

Totality: total
Visibility: export

fromSingleField : Lazy String -> Parser (String, JSON) a -> Parser JSON 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 : Lazy String -> Parser (String, JSON) a -> Parser JSON 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 : Lazy String -> String -> String -> Parser (String, JSON) a -> Parser JSON 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