
   0 | module JSON.RPC
   1 | 
   2 | import JSON.Simple
   3 | import JSON.Simple.Derive
   4 | 
   5 | import public Data.Singleton
   6 | import Data.List.Quantifiers
   7 | import Data.DPair
   8 | import Decidable.Equality
   9 | 
  10 | %language ElabReflection
  11 | 
  12 | -- custom serialisers/deserialisers
  13 | IgnoreMissingKeyToJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
  14 | IgnoreMissingKeyToJSON = customFromJSON Export ({replaceMissingKeysWithNull := const True} defaultOptions)
  15 | 
  16 | IgnoreMissingKeyFromJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
  17 | IgnoreMissingKeyFromJSON = customToJSON Export ({replaceMissingKeysWithNull := const True} defaultOptions)
  18 | 
  19 | IgnoreMissingParamFromJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
  20 | IgnoreMissingParamFromJSON =
  21 |   customFromJSON Export ({replaceMissingKeysWithNull := (== "params")} defaultOptions)
  22 | 
  23 | UntaggedFromJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
  24 | UntaggedFromJSON = customFromJSON Export ({sum := UntaggedValue} defaultOptions)
  25 | 
  26 | UntaggedToJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)
  27 | UntaggedToJSON = customToJSON Export ({sum := UntaggedValue} defaultOptions)
  28 | 
  29 | ||| A dictionary of JSON values
  30 | public export
  31 | record JSONObject where
  32 |   constructor MkJSONObject
  33 |   toList : List (String, JSON)
  34 | 
  35 | %runElab derive "JSONObject" [Eq]
  36 | 
  37 | public export %inline
  38 | fromList : List (String, JSON) -> JSONObject
  39 | fromList = MkJSONObject
  40 | 
  41 | export
  42 | FromJSON JSONObject where
  43 |   fromJSON (JObject ls) = MkJSONObject <$> traverse (traverse fromJSON) ls
  44 |   fromJSON _ = fail "expected JSON object"
  45 | 
  46 | export
  47 | ToJSON JSONObject where
  48 |   toJSON (MkJSONObject ls) = JObject ls
  49 | 
  50 | export
  51 | Show JSONObject where
  52 |   show x = encode x
  53 | 
  54 | export
  55 | Interpolation JSONObject where
  56 |   interpolate x = encode x
  57 | 
  58 | ||| A list of JSON values
  59 | public export
  60 | JSONArray : Type
  61 | JSONArray = List JSON
  62 | 
  63 | public export
  64 | record Null where
  65 |   constructor MkNull
  66 | 
  67 | export
  68 | Eq Null where
  69 |   _ == _ = True
  70 | 
  71 | export
  72 | Show Null where
  73 |   show _ = "null"
  74 | 
  75 | export
  76 | Interpolation Null where
  77 |   interpolate _ = "null"
  78 | 
  79 | export
  80 | DecEq Null where
  81 |   decEq MkNull MkNull = Yes Refl
  82 | 
  83 | public export
  84 | ToJSON Null where
  85 |   toJSON _ = JNull
  86 | 
  87 | public export
  88 | FromJSON Null where
  89 |   fromJSON JNull = pure MkNull
  90 |   fromJSON actual =
  91 |     fail "expected null, but encountered \{typeOf actual}"
  92 | 
  93 | -- JSONRPC id values are either Integers, Strings or Null
  94 | public export
  95 | data JSONRPCId : Type where
  96 |   IntegerId : Integer -> JSONRPCId
  97 |   StringId : String -> JSONRPCId
  98 |   NullId : Null -> JSONRPCId
  99 | 
 100 | public export %inline
 101 | NoId : JSONRPCId
 102 | NoId = NullId MkNull
 103 | 
 104 | %runElab derive "JSONRPCId"
 105 |   [Eq, UntaggedToJSON, UntaggedFromJSON]
 106 | 
 107 | export
 108 | Show JSONRPCId where
 109 |   show x = encode x
 110 | 
 111 | public export
 112 | data Parameters : Type where
 113 |   NullParam : Null -> Parameters
 114 |   ByPosition : JSONArray -> Parameters
 115 |   ByName : JSONObject -> Parameters
 116 | 
 117 | public export %inline
 118 | ByName' : List (String, JSON) -> Parameters
 119 | ByName' = ByName . MkJSONObject
 120 | 
 121 | -- create parameters from a json object
 122 | -- create an empty object if the json given isn't an object
 123 | export
 124 | ByNameFromJSON : JSON -> Parameters
 125 | ByNameFromJSON (JObject fields) = ByName (MkJSONObject fields)
 126 | ByNameFromJSON _ = ByName (MkJSONObject [])
 127 | 
 128 | %runElab derive "Parameters"
 129 |   [Eq, UntaggedToJSON, UntaggedFromJSON]
 130 | 
 131 | public export %inline
 132 | NoParam : Parameters
 133 | NoParam = NullParam MkNull
 134 | 
 135 | public export %inline
 136 | Named : List (String, JSON) -> Parameters
 137 | Named = ByName . MkJSONObject
 138 | 
 139 | export
 140 | Show Parameters where
 141 |   show x = encode x
 142 | 
 143 | public export
 144 | record Request where
 145 |   constructor MkRequest'
 146 |   jsonrpc : Singleton "2.0"
 147 |   method : String
 148 |   params : Parameters
 149 |   id : JSONRPCId
 150 | 
 151 | %runElab derive "Request" [ Eq, ToJSON, IgnoreMissingParamFromJSON ]
 152 | 
 153 | export
 154 | Show Request where
 155 |   show x = encode x
 156 | 
 157 | export
 158 | Interpolation Request where
 159 |   interpolate x = encode x
 160 | 
 161 | public export %inline
 162 | MkRequest : String -> Parameters -> JSONRPCId -> Request
 163 | MkRequest = MkRequest' (Val "2.0")
 164 | 
 165 | ||| A JSONRPC notification contains the same information as a request without the id
 166 | public export
 167 | record Notification where
 168 |   constructor MkNotification'
 169 |   jsonrpc : Singleton "2.0"
 170 |   method : String
 171 |   params : Parameters
 172 | 
 173 | %runElab derive "Notification" [ Eq, ToJSON, IgnoreMissingParamFromJSON ]
 174 | 
 175 | export
 176 | Show Notification where
 177 |   show x = encode x
 178 | 
 179 | export
 180 | Interpolation Notification where
 181 |   interpolate x = encode x
 182 | 
 183 | public export %inline
 184 | MkNotification : String -> Parameters -> Notification
 185 | MkNotification = MkNotification' (Val "2.0")
 186 | 
 187 | ||| A JSON RPC Response has a result field that contains the payload
 188 | public export
 189 | record ResponseSuccess where
 190 |   constructor MkResponseSuccess'
 191 |   jsonrpc : Singleton "2.0"
 192 |   result : JSON
 193 |   id : JSONRPCId
 194 | 
 195 | %runElab derive "ResponseSuccess" [ Eq, ToJSON, FromJSON ]
 196 | 
 197 | export
 198 | Show ResponseSuccess where
 199 |   show x = encode x
 200 | 
 201 | export
 202 | Interpolation ResponseSuccess where
 203 |   interpolate x = encode x
 204 | 
 205 | public export %inline
 206 | MkResponseSuccess : JSON -> JSONRPCId -> ResponseSuccess
 207 | MkResponseSuccess = MkResponseSuccess' (Val "2.0")
 208 | 
 209 | 
 210 | -- Errors and error codes
 211 | public export
 212 | data ErrorCode
 213 |   = ParseError
 214 |   | InvalidRequest
 215 |   | MethodNotFound
 216 |   | InvalidParams
 217 |   | InternalError
 218 |   | ServerError Integer -- between -32000 and -32099
 219 |   | CustomError Integer
 220 | 
 221 | %runElab derive "ErrorCode" [ Eq, Ord ]
 222 | 
 223 | export
 224 | FromJSON ErrorCode where
 225 |   fromJSON (JInteger (-32700)) = pure $ ParseError
 226 |   fromJSON (JInteger (-32600)) = pure $ InvalidRequest
 227 |   fromJSON (JInteger (-32601)) = pure $ MethodNotFound
 228 |   fromJSON (JInteger (-32602)) = pure $ InvalidParams
 229 |   fromJSON (JInteger (-32603)) = pure $ InternalError
 230 |   fromJSON (JInteger n) =
 231 |     case (n >= -32099 && n <= (-32000)) of
 232 |          True => pure $ ServerError n
 233 |          _ => pure $ CustomError n
 234 |   fromJSON _ = fail "not an integer"
 235 | 
 236 | export
 237 | (.code) : ErrorCode -> Integer
 238 | (.code) ParseError = (-32700)
 239 | (.code) InvalidRequest = (-32600)
 240 | (.code) MethodNotFound = (-32601)
 241 | (.code) InvalidParams = (-32602)
 242 | (.code) InternalError = (-32603)
 243 | (.code) (ServerError i) = i
 244 | (.code) (CustomError i) = i
 245 | 
 246 | export
 247 | ToJSON ErrorCode where
 248 |   toJSON x = JInteger x.code
 249 | 
 250 | export
 251 | Show ErrorCode where
 252 |   show x = show x.code
 253 | 
 254 | export
 255 | Interpolation ErrorCode where
 256 |   interpolate x = show x.code
 257 | 
 258 | public export
 259 | record Error where
 260 |   constructor MkError
 261 |   code : ErrorCode
 262 |   message : String
 263 |   data_ : Maybe JSON
 264 | 
 265 | mapData : String -> String
 266 | mapData "data_" = "data"
 267 | mapData x = x
 268 | 
 269 | %runElab derive "Error" [ customToJSON Export ({fieldNameModifier := mapData} defaultOptions)]
 270 | 
 271 | nothingEqNull : Maybe JSON -> Maybe JSON -> Bool
 272 | nothingEqNull Nothing Nothing = True
 273 | nothingEqNull (Just JNull) Nothing = True
 274 | nothingEqNull Nothing (Just JNull) = True
 275 | nothingEqNull (Just x) (Just y) = x == y
 276 | nothingEqNull _ _ = False
 277 | 
 278 | export
 279 | Eq Error where
 280 |   MkError c1 m1 d1 == MkError c2 m2 d2 = c1 == c2 && m1 == m2 && nothingEqNull d1 d2
 281 | 
 282 | 
 283 | export
 284 | FromJSON Error where
 285 |   fromJSON (JObject xs) = do
 286 |     let Just code = lookup "code" xs
 287 |       | Nothing => fail #"expected field "code""#
 288 |     let Just message = lookup "message" xs
 289 |       | Nothing => fail #"expected field "message""#
 290 |     -- if the data is missing, simply fill the field with `Nothing`
 291 |     data_ <- traverse fromJSON (lookup "data" xs )
 292 |     pure $ MkError
 293 |       !(fromJSON code)
 294 |       !(fromJSON message)
 295 |       data_
 296 |   fromJSON _ = fail "expected object"
 297 | 
 298 | export
 299 | Show Error where
 300 |   show x = encode x
 301 | 
 302 | export
 303 | Interpolation Error where
 304 |   interpolate x = encode x
 305 | 
 306 | ||| A JSON RPC error has an error field containing information about the error
 307 | public export
 308 | record ResponseError where
 309 |   constructor MkResponseError'
 310 |   jsonrpc : Singleton "2.0"
 311 |   error : Error
 312 |   id : JSONRPCId
 313 | 
 314 | %runElab derive "ResponseError" [ Eq, ToJSON, FromJSON ]
 315 | 
 316 | export
 317 | Show ResponseError where
 318 |   show x = encode x
 319 | 
 320 | export
 321 | Interpolation ResponseError where
 322 |   interpolate x = encode x
 323 | 
 324 | public export %inline
 325 | MkResponseError : Error -> JSONRPCId -> ResponseError
 326 | MkResponseError = MkResponseError' (Val "2.0")
 327 | 
 328 | public export
 329 | data Response : Type where
 330 |   Success : ResponseSuccess -> Response
 331 |   Failure : ResponseError -> Response
 332 | 
 333 | export
 334 | rpcSuccessResponse :
 335 |   ToJSON a =>
 336 |   JSONRPCId ->
 337 |   a -> RPC.Response
 338 | rpcSuccessResponse requestID result
 339 |   = Success $ MkResponseSuccess (toJSON result) requestID
 340 | 
 341 | %runElab derive "Response"
 342 |   [Eq, UntaggedToJSON, UntaggedFromJSON]
 343 | 
 344 | export
 345 | Show Response where
 346 |   show x = encode x
 347 | 
 348 | ||| A JSONRPCMessage is either a request or a notification. Invalid messages
 349 | ||| are not represented.
 350 | public export
 351 | data Message : Type where
 352 |   Req : Request -> Message
 353 |   Notif : Notification -> Message
 354 | 
 355 | %runElab derive "Message"
 356 |   [Eq, UntaggedToJSON, UntaggedFromJSON]
 357 | 
 358 | export
 359 | Show Message where
 360 |   show x = encode x
 361 | 
 362 | export
 363 | Interpolation Message where
 364 |   interpolate x = encode x
 365 | 
 366 | -- a batch request contains json that either parses
 367 | public export
 368 | JSONRPCBatch : Type
 369 | JSONRPCBatch = List (Maybe Message)
 370 | 
 371 | ------------------------------------------------------------------------------------
 372 | -- Default errors from the spec
 373 | ------------------------------------------------------------------------------------
 374 | 
 375 | ||| There is a parse error in the JSON we received
 376 | export
 377 | rpcJSONParseError : ResponseError
 378 | rpcJSONParseError =
 379 |   MkResponseError
 380 |     (MkError ParseError "Parse error" Nothing) NoId
 381 | 
 382 | ||| Request is not even valid
 383 | export
 384 | rpcInvalidRequestError : ResponseError
 385 | rpcInvalidRequestError =
 386 |   MkResponseError
 387 |     (MkError InvalidRequest "Invalid Request" Nothing) NoId
 388 | 
 389 | ||| This is when everything is OK but the method used cannot be found
 390 | ||| in the implementation
 391 | export
 392 | rpcMissingMethod : JSONRPCId -> ResponseError
 393 | rpcMissingMethod = MkResponseError (MkError MethodNotFound "Method not found" Nothing)
 394 | 
 395 |