Language.LSP.Message.Derive

Automatic deriviation of JSON conversion interfaces.

(C) The Idris Community, 2021

Reexports

Definitions

record JSONDeriveOpts : Type

  Options for automatic derivation of `ToJSON`/`FromJSON` instances.

Totality: total
Visibility: public export
Constructor: 

MkOpts : Bool -> List (String, String) -> List (String, JSON) -> JSONDeriveOpts

Projections:

.renames : JSONDeriveOpts -> List (String, String)

  Renaming rules for arguments where the name of the argument does not
  match the correspondent key in the translated JSON object.

.staticFields : JSONDeriveOpts -> List (String, JSON)

  Fields that must be present in the JSON translation but have static
  values.

.tagged : JSONDeriveOpts -> Bool

  If tagged, values are converted to JSON object with one field where the
  key is the name of the constructor and the value is the object obtained
  from converting the arguments of the constructor.

.tagged : JSONDeriveOpts -> Bool

  If tagged, values are converted to JSON object with one field where the
  key is the name of the constructor and the value is the object obtained
  from converting the arguments of the constructor.

Totality: total
Visibility: public export

tagged : JSONDeriveOpts -> Bool

  If tagged, values are converted to JSON object with one field where the
  key is the name of the constructor and the value is the object obtained
  from converting the arguments of the constructor.

Totality: total
Visibility: public export

.renames : JSONDeriveOpts -> List (String, String)

  Renaming rules for arguments where the name of the argument does not
  match the correspondent key in the translated JSON object.

Totality: total
Visibility: public export

renames : JSONDeriveOpts -> List (String, String)

  Renaming rules for arguments where the name of the argument does not
  match the correspondent key in the translated JSON object.

Totality: total
Visibility: public export

.staticFields : JSONDeriveOpts -> List (String, JSON)

  Fields that must be present in the JSON translation but have static
  values.

Totality: total
Visibility: public export

staticFields : JSONDeriveOpts -> List (String, JSON)

  Fields that must be present in the JSON translation but have static
  values.

Totality: total
Visibility: public export

defaultOpts : JSONDeriveOpts

Totality: total
Visibility: public export

deriveToJSON : JSONDeriveOpts -> Name -> Elab ()

  Automatic derivation of `ToJSON` instances.
  NOTE: all the fields in each constructor MUST be named, record already
  comply but types declared with data must have constructors declared like
  this:
  ```idris example
  data Position : Type where
    MkPosition : (x : Integer) -> (y : Integer) -> Position
  ```
  If the tagging option is enabled, types with multiple constructors are
  translated to a JSON object with a single key-value pair where the key is
  constructor name (without the namespace) and the value is the JSON object
  translated as if untagged.
  Constructor arguments that are `Maybe` instances are omitted if `Nothing`
  and converted without the constructor if `Just`. If you need to translate a
  mandatory field that can be nullable use the `Null` type.
  
  @ opts The automatic derivation options.
  @ name The name of the type to derive for. Can be without namespace if unambigous.

Visibility: public export

deriveFromJSON : JSONDeriveOpts -> Name -> Elab ()

  Automatic derivation of `FromJSON` instances.
  NOTE: all the fields in each constructor MUST be named, record already
  comply but types declared with data must have constructors declared like
  this:
  ```idris example
  data Position : Type where
    MkPosition : (x : Integer) -> (y : Integer) -> Position
  ```
  If the tagging option is enabled, types with multiple constructors are
  translated to a JSON object with a single key-value pair where the key is
  constructor name (without the namespace) and the value is the JSON object
  translated as if untagged.
  Constructor arguments that are `Maybe` instances are omitted if `Nothing`
  and converted without the constructor if `Just`. If you need to translate a
  mandatory field that can be nullable use the `Null` type.
  
  @ opts The automatic derivation options.
  @ name The name of the type to derive for. Can be without namespace if unambigous.

Visibility: public export

deriveJSON : JSONDeriveOpts -> Name -> Elab ()

  Automatic derivation of `ToJSON` and `FromJSON` instances.
  See `deriveToJSON` and `deriveFromJSON`.
  
  @ opts The automatic derivation options.
  @ name The name of the type to derive for. Can be without namespace if unambigous.

Visibility: public export