JSON.Encoder

(source)

The interfaces in this module abstract over how we
encode and decode values from and to JSON.

This allows us to use different (probably backend dependant)
intermediary data representations to be used by the actual
marshallers `ToJSON` and `FromJSON`.

Reexports

import public JSON.Parser

Definitions

interface Encoder : Type -> Type

  Abstraction over JSON value encoding.

Parameters: v
Methods:

stringify : v -> String

  Converts the intermediary data representation
  to a JSON string.

string : String -> v

  Encodes a `String` value.

double : Double -> v

  Encodes a `Double` as a JSON `Double`.

integer : Integer -> v

  Encodes a `Double` as a JSON `Integer`.

boolean : Bool -> v

  Encodes a `Bool` as a JSON `Boolean`.

array : List v -> v

  Encodes a `List` of values as a JSON `Array`.

object : List (String, v) -> v

  Encodes a `List` key-value pairs as a JSON `Object`

null : v

Implementation:

Encoder JSON

stringify : Encoder v => v -> String

  Converts the intermediary data representation
  to a JSON string.

Visibility: public export

string : Encoder v => String -> v

  Encodes a `String` value.

Visibility: public export

double : Encoder v => Double -> v

  Encodes a `Double` as a JSON `Double`.

Visibility: public export

integer : Encoder v => Integer -> v

  Encodes a `Double` as a JSON `Integer`.

Visibility: public export

boolean : Encoder v => Bool -> v

  Encodes a `Bool` as a JSON `Boolean`.

Visibility: public export

array : Encoder v => List v -> v

  Encodes a `List` of values as a JSON `Array`.

Visibility: public export

object : Encoder v => List (String, v) -> v

  Encodes a `List` key-value pairs as a JSON `Object`

Visibility: public export

null : Encoder v => v

Visibility: public export

interface Object : Type -> Type -> Type

  Abstraction over JSON Object representation for decoding.
  It is important that `obj` is the type that guides interface
  resolution here, otherwise operators like `.:` cannot conveniently
  be used, since Idris needs additional guidance to resolve interfaces.

Parameters: obj, v
Methods:

lookup : String -> obj -> Maybe v
pairs : obj -> List (String, v)

Implementation:

Object (List (String, JSON)) JSON

lookup : Object obj v => String -> obj -> Maybe v

Visibility: public export

pairs : Object obj v => obj -> List (String, v)

Visibility: public export

interface Value : Type -> Type -> Type

  Abstraction over JSON value representation for decoding.

Parameters: v, obj
Constraints: Object obj v
Methods:

typeOf : v -> String

  Returns the actual value. This should be one of
  "String", "Null", "Object", "Number", "Boolean", or "Array".
  However, other types are possible as well, as this is
  only used for error messages when something goes wrong.

parse : Origin -> String -> Either (ParseError Void) v

  Tries to convert a string to an intermediare value.

getObject : v -> Maybe obj

  Tries to convert a value to an `Object`.

getArray : v -> Maybe (List v)

  Tries to convert a value to an `Array` of values.

getBoolean : v -> Maybe Bool

  Tries to convert a value to a `Boolean`.

getDouble : v -> Maybe Double

  Tries to convert a value to a `Double`.

getInteger : v -> Maybe Integer

  Tries to convert a value to an `Integer`.

getString : v -> Maybe String

  Tries to convert a value to a `String`.

isNull : v -> Bool

  `True`, if the value in question is `null`.

Implementation:

Value JSON (List (String, JSON))

typeOf : Value v obj => v -> String

  Returns the actual value. This should be one of
  "String", "Null", "Object", "Number", "Boolean", or "Array".
  However, other types are possible as well, as this is
  only used for error messages when something goes wrong.

Visibility: public export

parse : Value v obj => Origin -> String -> Either (ParseError Void) v

  Tries to convert a string to an intermediare value.

Visibility: public export

getObject : Value v obj => v -> Maybe obj

  Tries to convert a value to an `Object`.

Visibility: public export

getArray : Value v obj => v -> Maybe (List v)

  Tries to convert a value to an `Array` of values.

Visibility: public export

getBoolean : Value v obj => v -> Maybe Bool

  Tries to convert a value to a `Boolean`.

Visibility: public export

getDouble : Value v obj => v -> Maybe Double

  Tries to convert a value to a `Double`.

Visibility: public export

getInteger : Value v obj => v -> Maybe Integer

  Tries to convert a value to an `Integer`.

Visibility: public export

getString : Value v obj => v -> Maybe String

  Tries to convert a value to a `String`.

Visibility: public export

isNull : Value v obj => v -> Bool

  `True`, if the value in question is `null`.

Visibility: public export

getArrayN : Value v obj => (n : Nat) -> v -> Maybe (Vect n v)

Visibility: public export