3 | module Language.LSP.Message.Message
7 | import Language.LSP.Message.CallHierarchy
8 | import Language.LSP.Message.Cancel
9 | import Language.LSP.Message.CodeAction
10 | import Language.LSP.Message.CodeLens
11 | import Language.LSP.Message.Command
12 | import Language.LSP.Message.Completion
13 | import Language.LSP.Message.Declaration
14 | import Language.LSP.Message.Definition
15 | import Language.LSP.Message.Derive
16 | import Language.LSP.Message.Diagnostics
17 | import Language.LSP.Message.DocumentColor
18 | import Language.LSP.Message.DocumentFormatting
19 | import Language.LSP.Message.DocumentHighlight
20 | import Language.LSP.Message.DocumentLink
21 | import Language.LSP.Message.DocumentSymbols
22 | import Language.LSP.Message.FoldingRange
23 | import Language.LSP.Message.Hover
24 | import Language.LSP.Message.Implementation
25 | import Language.LSP.Message.Initialize
26 | import Language.LSP.Message.LinkedEditingRange
27 | import Language.LSP.Message.Location
28 | import Language.LSP.Message.Method
29 | import Language.LSP.Message.Moniker
30 | import Language.LSP.Message.Progress
31 | import Language.LSP.Message.References
32 | import Language.LSP.Message.Registration
33 | import Language.LSP.Message.Rename
34 | import Language.LSP.Message.SelectionRange
35 | import Language.LSP.Message.SemanticTokens
36 | import Language.LSP.Message.SignatureHelp
37 | import Language.LSP.Message.TextDocument
38 | import Language.LSP.Message.Trace
39 | import Language.LSP.Message.Utils
40 | import Language.LSP.Message.Window
41 | import Language.LSP.Message.Workspace
42 | import Language.Reflection
44 | %language ElabReflection
49 | MessageParams : (method : Method from type) -> Type
50 | MessageParams Initialize = InitializeParams
51 | MessageParams Initialized = InitializedParams
52 | MessageParams Shutdown = Maybe Null
53 | MessageParams Exit = Maybe Null
54 | MessageParams SetTrace = SetTraceParams
55 | MessageParams WindowWorkDoneProgressCancel = WorkDoneProgressCancelParams
56 | MessageParams WorkspaceDidChangeWorkspaceFolders = DidChangeWorkspaceFoldersParams
57 | MessageParams WorkspaceDidChangeConfiguration = DidChangeConfigurationParams
58 | MessageParams WorkspaceDidChangeWatchedFiles = DidChangeWatchedFilesParams
59 | MessageParams WorkspaceSymbol = WorkspaceSymbolParams
60 | MessageParams WorkspaceExecuteCommand = ExecuteCommandParams
61 | MessageParams WorkspaceWillCreateFiles = CreateFilesParams
62 | MessageParams TextDocumentDidOpen = DidOpenTextDocumentParams
63 | MessageParams TextDocumentDidChange = DidChangeTextDocumentParams
64 | MessageParams TextDocumentWillSave = WillSaveTextDocumentParams
65 | MessageParams TextDocumentWillSaveWaitUntil = WillSaveTextDocumentParams
66 | MessageParams TextDocumentDidSave = DidSaveTextDocumentParams
67 | MessageParams TextDocumentDidClose = DidCloseTextDocumentParams
68 | MessageParams CompletionItemResolve = CompletionItem
69 | MessageParams TextDocumentHover = HoverParams
70 | MessageParams TextDocumentSignatureHelp = SignatureHelpParams
71 | MessageParams TextDocumentDeclaration = DeclarationParams
72 | MessageParams TextDocumentDefinition = DefinitionParams
73 | MessageParams TextDocumentTypeDefinition = TypeDefinitionParams
74 | MessageParams TextDocumentImplementation = ImplementationParams
75 | MessageParams TextDocumentReferences = ReferenceParams
76 | MessageParams TextDocumentDocumentHighlight = DocumentHighlightParams
77 | MessageParams TextDocumentDocumentSymbol = DocumentSymbolParams
78 | MessageParams TextDocumentCodeAction = CodeActionParams
79 | MessageParams CodeActionResolve = CodeAction
80 | MessageParams TextDocumentCodeLens = CodeLensParams
81 | MessageParams CodeLensResolve = CodeLens
82 | MessageParams TextDocumentDocumentLink = DocumentLinkParams
83 | MessageParams DocumentLinkResolve = DocumentLink
84 | MessageParams TextDocumentDocumentColor = DocumentColorParams
85 | MessageParams TextDocumentFormatting = DocumentFormattingParams
86 | MessageParams TextDocumentRangeFormatting = DocumentRangeFormattingParams
87 | MessageParams TextDocumentOnTypeFormatting = DocumentOnTypeFormattingParams
88 | MessageParams TextDocumentRename = RenameParams
89 | MessageParams TextDocumentPrepareRename = PrepareRenameParams
90 | MessageParams TextDocumentFoldingRange = FoldingRangeParams
91 | MessageParams TextDocumentSelectionRange = SelectionRangeParams
92 | MessageParams TextDocumentPrepareCallHierarchy = CallHierarchyParams
93 | MessageParams CallHierarchyIncomingCalls = CallHierarchyIncomingCallsParams
94 | MessageParams CallHierarchyOutgoingCalls = CallHierarchyOutgoingCallsParams
95 | MessageParams TextDocumentSemanticTokensFull = SemanticTokensParams
96 | MessageParams TextDocumentSemanticTokensFullDelta = SemanticTokensDeltaParams
97 | MessageParams TextDocumentSemanticTokensRange = SemanticTokensRangeParams
98 | MessageParams WorkspaceSemanticTokensRefresh = Maybe Null
99 | MessageParams TextDocumentLinkedEditingRange = LinkedEditingRangeParams
100 | MessageParams TextDocumentMoniker = MonikerParams
101 | MessageParams LogTrace = LogTraceParams
102 | MessageParams WindowShowMessage = ShowMessageParams
103 | MessageParams WindowShowMessageRequest = ShowMessageRequestParams
104 | MessageParams WindowShowDocument = ShowDocumentParams
105 | MessageParams WindowLogMessage = LogMessageParams
106 | MessageParams WindowWorkDoneProgressCreate = WorkDoneProgressCreateParams
107 | MessageParams TelemetryEvent = JSON
108 | MessageParams ClientRegisterCapability = RegistrationParams
109 | MessageParams ClientUnregisterCapability = UnregistrationParams
110 | MessageParams WorkspaceWorkspaceFolders = Maybe Null
111 | MessageParams WorkspaceConfiguration = ConfigurationParams
112 | MessageParams WorkspaceApplyEdit = ApplyWorkspaceEditParams
113 | MessageParams TextDocumentPublishDiagnostics = PublishDiagnosticsParams
114 | MessageParams TextDocumentCompletion = CompletionParams
115 | MessageParams WorkspaceCodeLensRefresh = Maybe Null
116 | MessageParams CancelRequest = CancelParams
117 | MessageParams Progress = OneOf [WorkDoneProgressBegin, WorkDoneProgressReport, WorkDoneProgressEnd]
120 | findParamsImpl : (method : Method from type) -> FromJSON (MessageParams method)
121 | findParamsImpl Initialize = %search
122 | findParamsImpl Initialized = %search
123 | findParamsImpl Shutdown = %search
124 | findParamsImpl Exit = %search
125 | findParamsImpl SetTrace = %search
126 | findParamsImpl WindowWorkDoneProgressCancel = %search
127 | findParamsImpl WorkspaceDidChangeWorkspaceFolders = %search
128 | findParamsImpl WorkspaceDidChangeConfiguration = %search
129 | findParamsImpl WorkspaceDidChangeWatchedFiles = %search
130 | findParamsImpl WorkspaceSymbol = %search
131 | findParamsImpl WorkspaceExecuteCommand = %search
132 | findParamsImpl WorkspaceWillCreateFiles = %search
133 | findParamsImpl TextDocumentDidOpen = %search
134 | findParamsImpl TextDocumentDidChange = %search
135 | findParamsImpl TextDocumentWillSave = %search
136 | findParamsImpl TextDocumentWillSaveWaitUntil = %search
137 | findParamsImpl TextDocumentDidSave = %search
138 | findParamsImpl TextDocumentDidClose = %search
139 | findParamsImpl CompletionItemResolve = %search
140 | findParamsImpl TextDocumentHover = %search
141 | findParamsImpl TextDocumentSignatureHelp = %search
142 | findParamsImpl TextDocumentDeclaration = %search
143 | findParamsImpl TextDocumentDefinition = %search
144 | findParamsImpl TextDocumentTypeDefinition = %search
145 | findParamsImpl TextDocumentImplementation = %search
146 | findParamsImpl TextDocumentReferences = %search
147 | findParamsImpl TextDocumentDocumentHighlight = %search
148 | findParamsImpl TextDocumentDocumentSymbol = %search
149 | findParamsImpl TextDocumentCodeAction = %search
150 | findParamsImpl CodeActionResolve = %search
151 | findParamsImpl TextDocumentCodeLens = %search
152 | findParamsImpl CodeLensResolve = %search
153 | findParamsImpl TextDocumentDocumentLink = %search
154 | findParamsImpl DocumentLinkResolve = %search
155 | findParamsImpl TextDocumentDocumentColor = %search
156 | findParamsImpl TextDocumentFormatting = %search
157 | findParamsImpl TextDocumentRangeFormatting = %search
158 | findParamsImpl TextDocumentOnTypeFormatting = %search
159 | findParamsImpl TextDocumentRename = %search
160 | findParamsImpl TextDocumentPrepareRename = %search
161 | findParamsImpl TextDocumentFoldingRange = %search
162 | findParamsImpl TextDocumentSelectionRange = %search
163 | findParamsImpl TextDocumentPrepareCallHierarchy = %search
164 | findParamsImpl CallHierarchyIncomingCalls = %search
165 | findParamsImpl CallHierarchyOutgoingCalls = %search
166 | findParamsImpl TextDocumentSemanticTokensFull = %search
167 | findParamsImpl TextDocumentSemanticTokensFullDelta = %search
168 | findParamsImpl TextDocumentSemanticTokensRange = %search
169 | findParamsImpl WorkspaceSemanticTokensRefresh = %search
170 | findParamsImpl TextDocumentLinkedEditingRange = %search
171 | findParamsImpl TextDocumentMoniker = %search
172 | findParamsImpl LogTrace = %search
173 | findParamsImpl WindowShowMessage = %search
174 | findParamsImpl WindowShowMessageRequest = %search
175 | findParamsImpl WindowShowDocument = %search
176 | findParamsImpl WindowLogMessage = %search
177 | findParamsImpl WindowWorkDoneProgressCreate = %search
178 | findParamsImpl TelemetryEvent = %search
179 | findParamsImpl ClientRegisterCapability = %search
180 | findParamsImpl ClientUnregisterCapability = %search
181 | findParamsImpl WorkspaceWorkspaceFolders = %search
182 | findParamsImpl WorkspaceConfiguration = %search
183 | findParamsImpl WorkspaceApplyEdit = %search
184 | findParamsImpl TextDocumentPublishDiagnostics = %search
185 | findParamsImpl TextDocumentCompletion = %search
186 | findParamsImpl WorkspaceCodeLensRefresh = %search
187 | findParamsImpl CancelRequest = %search
188 | findParamsImpl Progress = %search
192 | ResponseResult : (method : Method from Request) -> Type
193 | ResponseResult Initialize = InitializeResult
194 | ResponseResult Shutdown = Maybe Null
195 | ResponseResult WorkspaceSymbol = OneOf [List SymbolInformation, Null]
196 | ResponseResult WorkspaceExecuteCommand = JSON
197 | ResponseResult WorkspaceWillCreateFiles = OneOf [WorkspaceEdit, Null]
198 | ResponseResult TextDocumentWillSaveWaitUntil = OneOf [List TextEdit, Null]
199 | ResponseResult CompletionItemResolve = CompletionItem
200 | ResponseResult TextDocumentHover = OneOf [Hover, Null]
201 | ResponseResult TextDocumentSignatureHelp = OneOf [SignatureHelp, Null]
202 | ResponseResult TextDocumentDeclaration = OneOf [Location, List Location, List LocationLink, Null]
203 | ResponseResult TextDocumentDefinition = OneOf [Location, List Location, List LocationLink, Null]
204 | ResponseResult TextDocumentTypeDefinition = OneOf [Location, List Location, List LocationLink, Null]
205 | ResponseResult TextDocumentImplementation = OneOf [Location, List Location, List LocationLink, Null]
206 | ResponseResult TextDocumentReferences = OneOf [List Location, Null]
207 | ResponseResult TextDocumentDocumentHighlight = OneOf [List DocumentHighlight, Null]
208 | ResponseResult TextDocumentDocumentSymbol = OneOf [List DocumentSymbol, List SymbolInformation, Null]
209 | ResponseResult TextDocumentCodeAction = OneOf [List (OneOf [Command, CodeAction]), Null]
210 | ResponseResult CodeActionResolve = CodeAction
211 | ResponseResult TextDocumentCodeLens = OneOf [List CodeLens, Null]
212 | ResponseResult CodeLensResolve = Maybe Null
213 | ResponseResult TextDocumentDocumentLink = OneOf [List DocumentLink, Null]
214 | ResponseResult DocumentLinkResolve = DocumentLink
215 | ResponseResult TextDocumentDocumentColor = List ColorInformation
216 | ResponseResult TextDocumentFormatting = OneOf [List TextEdit, Null]
217 | ResponseResult TextDocumentRangeFormatting = OneOf [List TextEdit, Null]
218 | ResponseResult TextDocumentOnTypeFormatting = OneOf [List TextEdit, Null]
219 | ResponseResult TextDocumentRename = OneOf [WorkspaceEdit, Null]
220 | ResponseResult TextDocumentPrepareRename = OneOf [Range, PrepareRenamePlaceholderResponse, PrepareRenameDefaultResponse, Null]
221 | ResponseResult TextDocumentFoldingRange = OneOf [List FoldingRange, Null]
222 | ResponseResult TextDocumentSelectionRange = OneOf [List SelectionRange, Null]
223 | ResponseResult TextDocumentPrepareCallHierarchy = OneOf [List CallHierarchyItem, Null]
224 | ResponseResult CallHierarchyIncomingCalls = OneOf [List CallHierarchyIncomingCall, Null]
225 | ResponseResult CallHierarchyOutgoingCalls = OneOf [List CallHierarchyOutgoingCall, Null]
226 | ResponseResult TextDocumentSemanticTokensFull = OneOf [SemanticTokens, Null]
227 | ResponseResult TextDocumentSemanticTokensFullDelta = OneOf [SemanticTokens, SemanticTokensDelta, Null]
228 | ResponseResult TextDocumentSemanticTokensRange = OneOf [SemanticTokens, Null]
229 | ResponseResult WorkspaceSemanticTokensRefresh = Maybe Null
230 | ResponseResult TextDocumentLinkedEditingRange = OneOf [LinkedEditingRanges, Null]
231 | ResponseResult TextDocumentMoniker = OneOf [List Moniker, Null]
232 | ResponseResult WindowShowMessageRequest = OneOf [MessageActionItem, Null]
233 | ResponseResult WindowShowDocument = ShowDocumentResult
234 | ResponseResult WindowWorkDoneProgressCreate = Maybe Null
235 | ResponseResult ClientRegisterCapability = Maybe Null
236 | ResponseResult ClientUnregisterCapability = Maybe Null
237 | ResponseResult WorkspaceWorkspaceFolders = OneOf [List WorkspaceFolder, Null]
238 | ResponseResult WorkspaceConfiguration = List JSON
239 | ResponseResult WorkspaceApplyEdit = ApplyWorkspaceEditResponse
240 | ResponseResult TextDocumentCompletion = OneOf [List CompletionItem, CompletionList, Null]
241 | ResponseResult WorkspaceCodeLensRefresh = Maybe Null
243 | findNotificationImpl : (method : Method from Notification) -> ToJSON (MessageParams method)
244 | findNotificationImpl Initialized = %search
245 | findNotificationImpl Exit = %search
246 | findNotificationImpl SetTrace = %search
247 | findNotificationImpl WindowWorkDoneProgressCancel = %search
248 | findNotificationImpl WorkspaceDidChangeWorkspaceFolders = %search
249 | findNotificationImpl WorkspaceDidChangeConfiguration = %search
250 | findNotificationImpl WorkspaceDidChangeWatchedFiles = %search
251 | findNotificationImpl TextDocumentDidOpen = %search
252 | findNotificationImpl TextDocumentDidChange = %search
253 | findNotificationImpl TextDocumentWillSave = %search
254 | findNotificationImpl TextDocumentDidSave = %search
255 | findNotificationImpl TextDocumentDidClose = %search
256 | findNotificationImpl LogTrace = %search
257 | findNotificationImpl WindowShowMessage = %search
258 | findNotificationImpl WindowLogMessage = %search
259 | findNotificationImpl TelemetryEvent = %search
260 | findNotificationImpl TextDocumentPublishDiagnostics = %search
261 | findNotificationImpl CancelRequest = %search
262 | findNotificationImpl Progress = %search
264 | findRequestImpl : (method : Method from Request) -> ToJSON (MessageParams method)
265 | findRequestImpl Initialize = %search
266 | findRequestImpl Shutdown = %search
267 | findRequestImpl WorkspaceSymbol = %search
268 | findRequestImpl WorkspaceExecuteCommand = %search
269 | findRequestImpl WorkspaceWillCreateFiles = %search
270 | findRequestImpl TextDocumentWillSaveWaitUntil = %search
271 | findRequestImpl CompletionItemResolve = %search
272 | findRequestImpl TextDocumentHover = %search
273 | findRequestImpl TextDocumentSignatureHelp = %search
274 | findRequestImpl TextDocumentDeclaration = %search
275 | findRequestImpl TextDocumentDefinition = %search
276 | findRequestImpl TextDocumentTypeDefinition = %search
277 | findRequestImpl TextDocumentImplementation = %search
278 | findRequestImpl TextDocumentReferences = %search
279 | findRequestImpl TextDocumentDocumentHighlight = %search
280 | findRequestImpl TextDocumentDocumentSymbol = %search
281 | findRequestImpl TextDocumentCodeAction = %search
282 | findRequestImpl CodeActionResolve = %search
283 | findRequestImpl TextDocumentCodeLens = %search
284 | findRequestImpl CodeLensResolve = %search
285 | findRequestImpl TextDocumentDocumentLink = %search
286 | findRequestImpl DocumentLinkResolve = %search
287 | findRequestImpl TextDocumentDocumentColor = %search
288 | findRequestImpl TextDocumentFormatting = %search
289 | findRequestImpl TextDocumentRangeFormatting = %search
290 | findRequestImpl TextDocumentOnTypeFormatting = %search
291 | findRequestImpl TextDocumentRename = %search
292 | findRequestImpl TextDocumentPrepareRename = %search
293 | findRequestImpl TextDocumentFoldingRange = %search
294 | findRequestImpl TextDocumentSelectionRange = %search
295 | findRequestImpl TextDocumentPrepareCallHierarchy = %search
296 | findRequestImpl CallHierarchyIncomingCalls = %search
297 | findRequestImpl CallHierarchyOutgoingCalls = %search
298 | findRequestImpl TextDocumentSemanticTokensFull = %search
299 | findRequestImpl TextDocumentSemanticTokensFullDelta = %search
300 | findRequestImpl TextDocumentSemanticTokensRange = %search
301 | findRequestImpl WorkspaceSemanticTokensRefresh = %search
302 | findRequestImpl TextDocumentLinkedEditingRange = %search
303 | findRequestImpl TextDocumentMoniker = %search
304 | findRequestImpl WindowShowMessageRequest = %search
305 | findRequestImpl WindowShowDocument = %search
306 | findRequestImpl WindowWorkDoneProgressCreate = %search
307 | findRequestImpl ClientRegisterCapability = %search
308 | findRequestImpl ClientUnregisterCapability = %search
309 | findRequestImpl WorkspaceWorkspaceFolders = %search
310 | findRequestImpl WorkspaceConfiguration = %search
311 | findRequestImpl WorkspaceApplyEdit = %search
312 | findRequestImpl TextDocumentCompletion = %search
313 | findRequestImpl WorkspaceCodeLensRefresh = %search
315 | findResultImpl : (method : Method from Request) -> ToJSON (ResponseResult method)
316 | findResultImpl Initialize = %search
317 | findResultImpl Shutdown = %search
318 | findResultImpl WorkspaceSymbol = %search
319 | findResultImpl WorkspaceExecuteCommand = %search
320 | findResultImpl WorkspaceWillCreateFiles = %search
321 | findResultImpl TextDocumentWillSaveWaitUntil = %search
322 | findResultImpl CompletionItemResolve = %search
323 | findResultImpl TextDocumentHover = %search
324 | findResultImpl TextDocumentSignatureHelp = %search
325 | findResultImpl TextDocumentDeclaration = %search
326 | findResultImpl TextDocumentDefinition = %search
327 | findResultImpl TextDocumentTypeDefinition = %search
328 | findResultImpl TextDocumentImplementation = %search
329 | findResultImpl TextDocumentReferences = %search
330 | findResultImpl TextDocumentDocumentHighlight = %search
331 | findResultImpl TextDocumentDocumentSymbol = %search
332 | findResultImpl TextDocumentCodeAction = %search
333 | findResultImpl CodeActionResolve = %search
334 | findResultImpl TextDocumentCodeLens = %search
335 | findResultImpl CodeLensResolve = %search
336 | findResultImpl TextDocumentDocumentLink = %search
337 | findResultImpl DocumentLinkResolve = %search
338 | findResultImpl TextDocumentDocumentColor = %search
339 | findResultImpl TextDocumentFormatting = %search
340 | findResultImpl TextDocumentRangeFormatting = %search
341 | findResultImpl TextDocumentOnTypeFormatting = %search
342 | findResultImpl TextDocumentRename = %search
343 | findResultImpl TextDocumentPrepareRename = %search
344 | findResultImpl TextDocumentFoldingRange = %search
345 | findResultImpl TextDocumentSelectionRange = %search
346 | findResultImpl TextDocumentPrepareCallHierarchy = %search
347 | findResultImpl CallHierarchyIncomingCalls = %search
348 | findResultImpl CallHierarchyOutgoingCalls = %search
349 | findResultImpl TextDocumentSemanticTokensFull = %search
350 | findResultImpl TextDocumentSemanticTokensFullDelta = %search
351 | findResultImpl TextDocumentSemanticTokensRange = %search
352 | findResultImpl WorkspaceSemanticTokensRefresh = %search
353 | findResultImpl TextDocumentLinkedEditingRange = %search
354 | findResultImpl TextDocumentMoniker = %search
355 | findResultImpl WindowShowMessageRequest = %search
356 | findResultImpl WindowShowDocument = %search
357 | findResultImpl WindowWorkDoneProgressCreate = %search
358 | findResultImpl ClientRegisterCapability = %search
359 | findResultImpl ClientUnregisterCapability = %search
360 | findResultImpl WorkspaceWorkspaceFolders = %search
361 | findResultImpl WorkspaceConfiguration = %search
362 | findResultImpl WorkspaceApplyEdit = %search
363 | findResultImpl TextDocumentCompletion = %search
364 | findResultImpl WorkspaceCodeLensRefresh = %search
370 | fromMaybeJSONParameters : (method : Method from type) -> Maybe JSON -> Maybe (MessageParams method)
371 | fromMaybeJSONParameters Exit arg =
372 | pure $
join $
arg >>= (fromJSON @{findParamsImpl Exit})
373 | fromMaybeJSONParameters Shutdown arg =
374 | pure $
join $
arg >>= (fromJSON @{findParamsImpl Shutdown})
375 | fromMaybeJSONParameters WorkspaceSemanticTokensRefresh arg =
376 | pure $
join $
arg >>= (fromJSON @{findParamsImpl WorkspaceSemanticTokensRefresh})
377 | fromMaybeJSONParameters WorkspaceWorkspaceFolders arg =
378 | pure $
join $
arg >>= (fromJSON @{findParamsImpl WorkspaceWorkspaceFolders})
379 | fromMaybeJSONParameters WorkspaceCodeLensRefresh arg =
380 | pure $
join $
arg >>= (fromJSON @{findParamsImpl WorkspaceCodeLensRefresh})
381 | fromMaybeJSONParameters method arg = arg >>= (fromJSON @{findParamsImpl method})
385 | data NotificationMessage : Method from Notification -> Type where
386 | MkNotificationMessage : (method : Method from Notification)
387 | -> (params : MessageParams method)
388 | -> NotificationMessage method
391 | {method : Method from Notification} -> ToJSON (NotificationMessage method) where
392 | toJSON (MkNotificationMessage method params) =
393 | JObject ([("jsonrpc", JString "2.0"), ("method", toJSON method), ("params", toJSON @{findNotificationImpl method} params)])
396 | FromJSON (
from ** method : Method from Notification ** NotificationMessage method)
where
397 | fromJSON (JObject arg) = do
398 | lookup "jsonrpc" arg >>= (guard . (== JString "2.0"))
399 | (
from ** meth)
<- lookup "method" arg >>= fromJSON {a = (
from ** Method from Notification)
}
401 | Exit => do let par = lookup "params" arg >>= (fromJSON @{findParamsImpl meth})
402 | pure (
from ** meth ** MkNotificationMessage meth (join par))
403 | _ => do par <- lookup "params" arg >>= (fromJSON @{findParamsImpl meth})
404 | pure (
from ** meth ** MkNotificationMessage meth par)
405 | fromJSON _ = neutral
407 | namespace NotificationMessage
409 | method : {0 m : Method from Notification} -> NotificationMessage m -> Method from Notification
410 | method (MkNotificationMessage m _) = m
413 | params : {0 method : Method from Notification} -> NotificationMessage method -> MessageParams method
414 | params (MkNotificationMessage _ p) = p
418 | data RequestMessage : Method from Request -> Type where
419 | MkRequestMessage : (id : OneOf [Int, String])
420 | -> (method : Method from Request)
421 | -> (params : MessageParams method)
422 | -> RequestMessage method
425 | {method : Method from Request} -> ToJSON (RequestMessage method) where
426 | toJSON (MkRequestMessage id method params) =
427 | JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("method", toJSON method), ("params", toJSON @{findRequestImpl method} params)])
430 | FromJSON (
from ** method : Method from Request ** RequestMessage method)
where
431 | fromJSON (JObject arg) = do
432 | lookup "jsonrpc" arg >>= (guard . (== JString "2.0"))
433 | id <- lookup "id" arg >>= fromJSON
434 | (
from ** method)
<- lookup "method" arg >>= fromJSON {a = (
from ** Method from Request)
}
436 | Shutdown => do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
437 | pure (
from ** method ** MkRequestMessage id method (join params))
438 | WorkspaceSemanticTokensRefresh =>
439 | do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
440 | pure (
from ** method ** MkRequestMessage id method (join params))
441 | WorkspaceWorkspaceFolders =>
442 | do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
443 | pure (
from ** method ** MkRequestMessage id method (join params))
444 | WorkspaceCodeLensRefresh =>
445 | do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
446 | pure (
from ** method ** MkRequestMessage id method (join params))
447 | _ => do params <- lookup "params" arg >>= (fromJSON @{findParamsImpl method})
448 | pure (
from ** method ** MkRequestMessage id method params)
449 | fromJSON _ = neutral
451 | namespace RequestMessage
453 | id : RequestMessage m -> OneOf [Int, String]
454 | id (MkRequestMessage i _ _) = i
457 | method : {0 m : Method from Request} -> RequestMessage m -> Method from Request
458 | method (MkRequestMessage _ m _) = m
461 | params : {0 method : Method from Request} -> RequestMessage method -> MessageParams method
462 | params (MkRequestMessage _ _ p) = p
466 | Message : (type : MethodType) -> (Method from type -> Type)
467 | Message Notification = NotificationMessage
468 | Message Request = RequestMessage
471 | FromJSON (
from ** type ** method : Method from type ** Message type method)
where
473 | (fromJSON arg >>= \(
f ** m ** msg)
: (
from ** method : Method from Request ** RequestMessage method)
=> pure (
f ** _ ** m ** msg)
)
474 | <|> (fromJSON arg >>= \(
f ** m ** msg)
: (
from ** method : Method from Notification ** NotificationMessage method)
=> pure (
f ** _ ** m ** msg)
)
477 | namespace ErrorCodes
485 | | ServerNotInitialized
489 | | JSONRPCReserved Int
494 | ToJSON ErrorCodes where
495 | toJSON ParseError = JNumber (-
32700)
496 | toJSON InvalidRequest = JNumber (-
32600)
497 | toJSON MethodNotFound = JNumber (-
32601)
498 | toJSON InvalidParams = JNumber (-
32602)
499 | toJSON InternalError = JNumber (-
32603)
500 | toJSON ServerNotInitialized = JNumber (-
32002)
501 | toJSON UnknownErrorCode = JNumber (-
32001)
502 | toJSON ContentModified = JNumber (-
32801)
503 | toJSON RequestCancelled = JNumber (-
32800)
504 | toJSON (JSONRPCReserved code) = JNumber (cast code)
505 | toJSON (LSPReserved code) = JNumber (cast code)
506 | toJSON (Custom code) = JNumber (cast code)
509 | FromJSON ErrorCodes where
511 | fromJSON (JNumber code) =
512 | if code == (-
32700) then pure ParseError
513 | else if code == (-
32600) then pure InvalidRequest
514 | else if code == (-
32601) then pure MethodNotFound
515 | else if code == (-
32602) then pure InvalidParams
516 | else if code == (-
32603) then pure InternalError
517 | else if code == (-
32002) then pure ServerNotInitialized
518 | else if code == (-
32001) then pure UnknownErrorCode
519 | else if code == (-
32801) then pure ContentModified
520 | else if code == (-
32800) then pure RequestCancelled
521 | else if (-
32099) <= code && code <= (-
32000) then pure (JSONRPCReserved $
cast code)
522 | else if (-
32899) <= code && code <= (-
32800) then pure (LSPReserved $
cast code)
523 | else pure (Custom $
cast code)
524 | fromJSON _ = neutral
528 | record ResponseError where
529 | constructor MkResponseError
533 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{ResponseError
}
537 | data ResponseMessage : Method from type -> Type where
538 | Success : (id : OneOf [Int, String, Null]) -> (result : ResponseResult method) -> ResponseMessage method
539 | Failure : (id : OneOf [Int, String, Null]) -> (error : ResponseError) -> ResponseMessage method
542 | {method : Method from Request} -> ToJSON (ResponseMessage method) where
543 | toJSON (Success id result) =
544 | JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("result", toJSON @{findResultImpl method} result)])
545 | toJSON (Failure id error) =
546 | JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("error", toJSON error)])
549 | FromJSON (ResponseResult method) => FromJSON (ResponseMessage method) where
550 | fromJSON (JObject arg) = do
551 | lookup "jsonrpc" arg >>= (guard . (== JString "2.0"))
552 | id <- lookup "id" arg >>= fromJSON
553 | case lookup "result" arg of
554 | Just v => Success id <$> fromJSON v
555 | Nothing => Failure id <$> (lookup "error" arg >>= fromJSON)
556 | fromJSON _ = neutral
558 | namespace ResponseMessage
560 | id : ResponseMessage method -> OneOf [Int, String, Null]
561 | id (Success i _) = i
562 | id (Failure i _) = i
565 | getResponseId : RequestMessage method -> OneOf [Int, String, Null]
566 | getResponseId = extend . RequestMessage.id