HTTP.API.Decode

Definitions

data DecodeErr : Type

  Error type that occurs when decoding a value or other piece of
  information.

Totality: total
Visibility: public export
Constructors:

ReadErr : String -> String -> String -> DecodeErr

  A `ReadErr` typically occurs when reading a single value
  from a string or bytestring.
  
  @type    : String description of the type we tried to read
  @value   : The string from which the value should be read
  @details : Additional information about why reading the value failed.

ContentErr : String -> String -> DecodeErr

  A `ContentErr` is - in general - a more technical error that happend
  when parsing the body of a message. The `details` field typically
  holds the detailed description from the parser about what went
  actually wrong.

Msg : String -> DecodeErr

  An arbitrary custom error message.

Hints:

Eq DecodeErr

FromJSON DecodeErr

Interpolation DecodeErr

Show DecodeErr

ToJSON DecodeErr

readErr : String -> ByteString -> DecodeErr

  Utility constructor for `ReadErr`.

Totality: total
Visibility: export

contentErr : String -> Interpolation a => a -> DecodeErr

  Utility constructor for `ContentErr`.

Totality: total
Visibility: export

setType : String -> DecodeErr -> DecodeErr

  Adjusts the `type` field of a decode error.

Totality: total
Visibility: export

setValue : String -> DecodeErr -> DecodeErr

  Adjusts the `type` field of a decode error.

Totality: total
Visibility: export

modMsg : (String -> String) -> DecodeErr -> DecodeErr

  Adjusts the `message` or `details` field of a decode error.

Totality: total
Visibility: export

decodeErr : Status -> DecodeErr -> RequestErr

Totality: total
Visibility: export

interface Decode : Type -> Type

  An interface for decoding value from a sequence of raw bytes.

Parameters: a
Methods:

decode : ByteString -> Either DecodeErr a

Implementations:

Decode ByteString

Decode String

Decode Nat

Decode Integer

Decode Bits8

Decode Bits16

Decode Bits32

Decode Bits64

Decode Int8

Decode Int16

Decode Int32

Decode Int64

Decode Double

Decode OAuthToken

decode : Decode a => ByteString -> Either DecodeErr a

Totality: total
Visibility: public export

decodeAs : (0 a : Type) -> Decode a => ByteString -> Either DecodeErr a

  Utiliy alias for `decode` that allows to explicitly specify the
  target type.

Totality: total
Visibility: public export

interface DecodeMany : Type -> Type

  An interface for decoding values by reading a prefix
  of a list of bytestrings such as a path in a URL.

Parameters: a
Methods:

simulateDecode : List ByteString -> Maybe (List ByteString)

decodeMany : List ByteString -> Either DecodeErr (List ByteString, a)

Implementations:

Decode a => DecodeMany a

Decode a => DecodeMany (SnocList a)

Decode a => DecodeMany (List a)

All (DecodeMany . f) ts => DecodeMany (All f ts)

DecodeMany a => DecodeMany (Vect n a)

simulateDecode : DecodeMany a => List ByteString -> Maybe (List ByteString)

Totality: total
Visibility: public export

decodeMany : DecodeMany a => List ByteString -> Either DecodeErr (List ByteString, a)

Totality: total
Visibility: public export

decodeAll : SnocList a -> Decode a -> List ByteString -> Either DecodeErr (List ByteString, SnocList a)

Totality: total
Visibility: export

interface DecodeVia : Type -> Type -> Type

Parameters: from, to
Methods:

fromBytes : Parameters -> ByteString -> Either DecodeErr from

decodeFrom : from -> Either DecodeErr to

mediaType : MediaType

Implementations:

FromJSON a => DecodeVia JSON a

FromFormData a => DecodeVia FormData a

fromBytes : DecodeVia from to => Parameters -> ByteString -> Either DecodeErr from

Totality: total
Visibility: public export

decodeFrom : DecodeVia from to => from -> Either DecodeErr to

Totality: total
Visibility: public export

mediaType : DecodeVia from to => MediaType

Totality: total
Visibility: public export

decodeVia : DecodeVia from to => Parameters -> ByteString -> Either DecodeErr to

Totality: total
Visibility: export

interface FromFormData : Type -> Type

Parameters: a
Methods:

fromFormData : FormData -> Either DecodeErr a

fromFormData : FromFormData a => FormData -> Either DecodeErr a

Totality: total
Visibility: public export

getFDBytes : String -> FormData -> Either DecodeErr ByteString

Totality: total
Visibility: export

refinedEither : Decode a => String -> (a -> Either String b) -> ByteString -> Either DecodeErr b

Totality: total
Visibility: export

refined : Decode a => String -> Lazy String -> (a -> Maybe b) -> ByteString -> Either DecodeErr b

Totality: total
Visibility: export

bounded : (0 a : Type) -> Decode a => Ord a => Cast a b => String -> a -> a -> ByteString -> Either DecodeErr b

Totality: total
Visibility: export

decodeTest : (0 a : Type) -> Decode a => Show a => String -> IO ()

  Testing facility for value decoding.
  
  Example usage at the REPL:
  
  ```
  :exec decodeTest Double "12.112"
  ```

Totality: total
Visibility: export

decodeManyTest : (0 a : Type) -> DecodeMany a => Show a => String -> IO ()

  Testing facility for path decoding.
  
  Example usage at the REPL:
  
  ```
  :exec decodeTest (Vect 3 Nat) "https://www.hock.com/1/2/3?foo=bar"
  ```

Totality: total
Visibility: export