Idris2Doc : JSON.RPC

JSON.RPC

(source)
Reexports
import public Data.Singleton
Definitions
record JSONObject : Type
  A dictionary of JSON values

  Totality: total
  Visibility: public export
  Constructor: 
MkJSONObject : List (String, JSON) -> JSONObject

  Projection: 
.toList : JSONObject -> List (String, JSON)

  Hints:
  
Eq JSONObject
  
FromJSON JSONObject
  
Interpolation JSONObject
  
Show JSONObject
  
ToJSON JSONObject
.toList : JSONObject -> List (String, JSON)
  Visibility: public export
toList : JSONObject -> List (String, JSON)
  Visibility: public export
fromList : List (String, JSON) -> JSONObject
  Visibility: public export
JSONArray : Type
  A list of JSON values

  Visibility: public export
data Null : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkNull : Null

  Hints:
  
DecEq Null
  
Eq Null
  
FromJSON Null
  
Interpolation Null
  
Show Null
  
ToJSON Null
data JSONRPCId : Type
  Totality: total
  Visibility: public export
  Constructors:
  
IntegerId : Integer -> JSONRPCId
  
StringId : String -> JSONRPCId
  
NullId : Null -> JSONRPCId

  Hints:
  
Eq JSONRPCId
  
FromJSON JSONRPCId
  
Show JSONRPCId
  
ToJSON JSONRPCId
NoId : JSONRPCId
  Visibility: public export
data Parameters : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NullParam : Null -> Parameters
  
ByPosition : JSONArray -> Parameters
  
ByName : JSONObject -> Parameters

  Hints:
  
Eq Parameters
  
FromJSON Parameters
  
Show Parameters
  
ToJSON Parameters
ByName' : List (String, JSON) -> Parameters
  Visibility: public export
ByNameFromJSON : JSON -> Parameters
  Visibility: export
NoParam : Parameters
  Visibility: public export
Named : List (String, JSON) -> Parameters
  Visibility: public export
record Request : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRequest' : Singleton "2.0" -> String -> Parameters -> JSONRPCId -> Request

  Projections:
  
.id : Request -> JSONRPCId
  
.jsonrpc : Request -> Singleton "2.0"
  
.method : Request -> String
  
.params : Request -> Parameters

  Hints:
  
Eq Request
  
FromJSON Request
  
Interpolation Request
  
Show Request
  
ToJSON Request
.jsonrpc : Request -> Singleton "2.0"
  Visibility: public export
jsonrpc : Request -> Singleton "2.0"
  Visibility: public export
.method : Request -> String
  Visibility: public export
method : Request -> String
  Visibility: public export
.params : Request -> Parameters
  Visibility: public export
params : Request -> Parameters
  Visibility: public export
.id : Request -> JSONRPCId
  Visibility: public export
id : Request -> JSONRPCId
  Visibility: public export
MkRequest : String -> Parameters -> JSONRPCId -> Request
  Visibility: public export
record Notification : Type
  A JSONRPC notification contains the same information as a request without the id

  Totality: total
  Visibility: public export
  Constructor: 
MkNotification' : Singleton "2.0" -> String -> Parameters -> Notification

  Projections:
  
.jsonrpc : Notification -> Singleton "2.0"
  
.method : Notification -> String
  
.params : Notification -> Parameters

  Hints:
  
Eq Notification
  
FromJSON Notification
  
Interpolation Notification
  
Show Notification
  
ToJSON Notification
.jsonrpc : Notification -> Singleton "2.0"
  Visibility: public export
jsonrpc : Notification -> Singleton "2.0"
  Visibility: public export
.method : Notification -> String
  Visibility: public export
method : Notification -> String
  Visibility: public export
.params : Notification -> Parameters
  Visibility: public export
params : Notification -> Parameters
  Visibility: public export
MkNotification : String -> Parameters -> Notification
  Visibility: public export
record ResponseSuccess : Type
  A JSON RPC Response has a result field that contains the payload

  Totality: total
  Visibility: public export
  Constructor: 
MkResponseSuccess' : Singleton "2.0" -> JSON -> JSONRPCId -> ResponseSuccess

  Projections:
  
.id : ResponseSuccess -> JSONRPCId
  
.jsonrpc : ResponseSuccess -> Singleton "2.0"
  
.result : ResponseSuccess -> JSON

  Hints:
  
Eq ResponseSuccess
  
FromJSON ResponseSuccess
  
Interpolation ResponseSuccess
  
Show ResponseSuccess
  
ToJSON ResponseSuccess
.jsonrpc : ResponseSuccess -> Singleton "2.0"
  Visibility: public export
jsonrpc : ResponseSuccess -> Singleton "2.0"
  Visibility: public export
.result : ResponseSuccess -> JSON
  Visibility: public export
result : ResponseSuccess -> JSON
  Visibility: public export
.id : ResponseSuccess -> JSONRPCId
  Visibility: public export
id : ResponseSuccess -> JSONRPCId
  Visibility: public export
MkResponseSuccess : JSON -> JSONRPCId -> ResponseSuccess
  Visibility: public export
data ErrorCode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ParseError : ErrorCode
  
InvalidRequest : ErrorCode
  
MethodNotFound : ErrorCode
  
InvalidParams : ErrorCode
  
InternalError : ErrorCode
  
ServerError : Integer -> ErrorCode
  
CustomError : Integer -> ErrorCode

  Hints:
  
Eq ErrorCode
  
FromJSON ErrorCode
  
Interpolation ErrorCode
  
Ord ErrorCode
  
Show ErrorCode
  
ToJSON ErrorCode
.code : ErrorCode -> Integer
  Visibility: export
record Error : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkError : ErrorCode -> String -> Maybe JSON -> Error

  Projections:
  
.code : Error -> ErrorCode
  
.data_ : Error -> Maybe JSON
  
.message : Error -> String

  Hints:
  
Eq Error
  
FromJSON Error
  
Interpolation Error
  
Show Error
  
ToJSON Error
.code : Error -> ErrorCode
  Visibility: public export
code : Error -> ErrorCode
  Visibility: public export
.message : Error -> String
  Visibility: public export
message : Error -> String
  Visibility: public export
.data_ : Error -> Maybe JSON
  Visibility: public export
data_ : Error -> Maybe JSON
  Visibility: public export
record ResponseError : Type
  A JSON RPC error has an error field containing information about the error

  Totality: total
  Visibility: public export
  Constructor: 
MkResponseError' : Singleton "2.0" -> Error -> JSONRPCId -> ResponseError

  Projections:
  
.error : ResponseError -> Error
  
.id : ResponseError -> JSONRPCId
  
.jsonrpc : ResponseError -> Singleton "2.0"

  Hints:
  
Eq ResponseError
  
FromJSON ResponseError
  
Interpolation ResponseError
  
Show ResponseError
  
ToJSON ResponseError
.jsonrpc : ResponseError -> Singleton "2.0"
  Visibility: public export
jsonrpc : ResponseError -> Singleton "2.0"
  Visibility: public export
.error : ResponseError -> Error
  Visibility: public export
error : ResponseError -> Error
  Visibility: public export
.id : ResponseError -> JSONRPCId
  Visibility: public export
id : ResponseError -> JSONRPCId
  Visibility: public export
MkResponseError : Error -> JSONRPCId -> ResponseError
  Visibility: public export
data Response : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Success : ResponseSuccess -> Response
  
Failure : ResponseError -> Response

  Hints:
  
Eq Response
  
FromJSON Response
  
Show Response
  
ToJSON Response
rpcSuccessResponse : ToJSON a => JSONRPCId -> a -> Response
  Visibility: export
data Message : Type
  A JSONRPCMessage is either a request or a notification. Invalid messages
  are not represented.

  Totality: total
  Visibility: public export
  Constructors:
  
Req : Request -> Message
  
Notif : Notification -> Message

  Hints:
  
Eq Message
  
FromJSON Message
  
Interpolation Message
  
Show Message
  
ToJSON Message
JSONRPCBatch : Type
  Visibility: public export
rpcJSONParseError : ResponseError
  There is a parse error in the JSON we received

  Visibility: export
rpcInvalidRequestError : ResponseError
  Request is not even valid

  Visibility: export
rpcMissingMethod : JSONRPCId -> ResponseError
  This is when everything is OK but the method used cannot be found
  in the implementation

  Visibility: export