0 | module Language.LSP.Message.Method

  2 | import public Data.DPair

  3 | import Language.JSON

  4 | import Language.LSP.Message.Derive

  5 | import Language.LSP.Message.Utils

  6 | import Language.Reflection

  8 | %language ElabReflection

  9 | %default total

 11 | public export

 12 | data MethodFrom = Client | Server

 14 | public export

 15 | data MethodType = Notification | Request

 17 | public export

 18 | data Method : MethodFrom -> MethodType -> Type where

 19 |   Initialize                          : Method Client Request

 20 |   Initialized                         : Method Client Notification

 21 |   Shutdown                            : Method Client Request

 22 |   Exit                                : Method Client Notification

 23 |   SetTrace                            : Method Client Notification

 24 |   WindowWorkDoneProgressCancel        : Method Client Notification

 25 |   WorkspaceDidChangeWorkspaceFolders  : Method Client Notification

 26 |   WorkspaceDidChangeConfiguration     : Method Client Notification

 27 |   WorkspaceDidChangeWatchedFiles      : Method Client Notification

 28 |   WorkspaceSymbol                     : Method Client Request

 29 |   WorkspaceExecuteCommand             : Method Client Request

 30 |   WorkspaceWillCreateFiles            : Method Client Request

 31 |   TextDocumentDidOpen                 : Method Client Notification

 32 |   TextDocumentDidChange               : Method Client Notification

 33 |   TextDocumentWillSave                : Method Client Notification

 34 |   TextDocumentWillSaveWaitUntil       : Method Client Request

 35 |   TextDocumentDidSave                 : Method Client Notification

 36 |   TextDocumentDidClose                : Method Client Notification

 37 |   TextDocumentCompletion              : Method Client Request

 38 |   CompletionItemResolve               : Method Client Request

 39 |   TextDocumentHover                   : Method Client Request

 40 |   TextDocumentSignatureHelp           : Method Client Request

 41 |   TextDocumentDeclaration             : Method Client Request

 42 |   TextDocumentDefinition              : Method Client Request

 43 |   TextDocumentTypeDefinition          : Method Client Request

 44 |   TextDocumentImplementation          : Method Client Request

 45 |   TextDocumentReferences              : Method Client Request

 46 |   TextDocumentDocumentHighlight       : Method Client Request

 47 |   TextDocumentDocumentSymbol          : Method Client Request

 48 |   TextDocumentCodeAction              : Method Client Request

 49 |   CodeActionResolve                   : Method Client Request

 50 |   TextDocumentCodeLens                : Method Client Request

 51 |   CodeLensResolve                     : Method Client Request

 52 |   TextDocumentDocumentLink            : Method Client Request

 53 |   DocumentLinkResolve                 : Method Client Request

 54 |   TextDocumentDocumentColor           : Method Client Request

 55 |   TextDocumentFormatting              : Method Client Request

 56 |   TextDocumentRangeFormatting         : Method Client Request

 57 |   TextDocumentOnTypeFormatting        : Method Client Request

 58 |   TextDocumentRename                  : Method Client Request

 59 |   TextDocumentPrepareRename           : Method Client Request

 60 |   TextDocumentFoldingRange            : Method Client Request

 61 |   TextDocumentSelectionRange          : Method Client Request

 62 |   TextDocumentPrepareCallHierarchy    : Method Client Request

 63 |   CallHierarchyIncomingCalls          : Method Client Request

 64 |   CallHierarchyOutgoingCalls          : Method Client Request

 65 |   TextDocumentSemanticTokensFull      : Method Client Request

 66 |   TextDocumentSemanticTokensFullDelta : Method Client Request

 67 |   TextDocumentSemanticTokensRange     : Method Client Request

 68 |   TextDocumentLinkedEditingRange      : Method Client Request

 69 |   TextDocumentMoniker                 : Method Client Request

 71 |   LogTrace                            : Method Server Notification

 72 |   WindowShowMessage                   : Method Server Notification

 73 |   WindowShowMessageRequest            : Method Server Request

 74 |   WindowShowDocument                  : Method Server Request

 75 |   WindowLogMessage                    : Method Server Notification

 76 |   WindowWorkDoneProgressCreate        : Method Server Request

 77 |   TelemetryEvent                      : Method Server Notification

 78 |   ClientRegisterCapability            : Method Server Request

 79 |   ClientUnregisterCapability          : Method Server Request

 80 |   WorkspaceWorkspaceFolders           : Method Server Request

 81 |   WorkspaceConfiguration              : Method Server Request

 82 |   WorkspaceApplyEdit                  : Method Server Request

 83 |   TextDocumentPublishDiagnostics      : Method Server Notification

 84 |   WorkspaceCodeLensRefresh            : Method Server Request

 85 |   WorkspaceSemanticTokensRefresh      : Method Server Request

 87 |   CancelRequest                       : Method from   Notification

 88 |   Progress                            : Method from   Notification

 91 | methodType : Method type from -> MethodType

 92 | methodType Initialize = Request

 93 | methodType Initialized = Notification

 94 | methodType Shutdown = Request

 95 | methodType Exit = Notification

 96 | methodType SetTrace = Notification

 97 | methodType WindowWorkDoneProgressCancel = Notification

 98 | methodType WorkspaceDidChangeWorkspaceFolders = Notification

 99 | methodType WorkspaceDidChangeConfiguration = Notification

100 | methodType WorkspaceDidChangeWatchedFiles = Notification

101 | methodType WorkspaceSymbol = Request

102 | methodType WorkspaceExecuteCommand = Request

103 | methodType WorkspaceWillCreateFiles = Request

104 | methodType TextDocumentDidOpen = Notification

105 | methodType TextDocumentDidChange = Notification

106 | methodType TextDocumentWillSave = Notification

107 | methodType TextDocumentWillSaveWaitUntil = Request

108 | methodType TextDocumentDidSave = Notification

109 | methodType TextDocumentDidClose = Notification

110 | methodType CompletionItemResolve = Request

111 | methodType TextDocumentHover = Request

112 | methodType TextDocumentSignatureHelp = Request

113 | methodType TextDocumentDeclaration = Request

114 | methodType TextDocumentDefinition = Request

115 | methodType TextDocumentTypeDefinition = Request

116 | methodType TextDocumentImplementation = Request

117 | methodType TextDocumentReferences = Request

118 | methodType TextDocumentDocumentHighlight = Request

119 | methodType TextDocumentDocumentSymbol = Request

120 | methodType TextDocumentCodeAction = Request

121 | methodType CodeActionResolve = Request

122 | methodType TextDocumentCodeLens = Request

123 | methodType CodeLensResolve = Request

124 | methodType TextDocumentDocumentLink = Request

125 | methodType DocumentLinkResolve = Request

126 | methodType TextDocumentDocumentColor = Request

127 | methodType TextDocumentFormatting = Request

128 | methodType TextDocumentRangeFormatting = Request

129 | methodType TextDocumentOnTypeFormatting = Request

130 | methodType TextDocumentRename = Request

131 | methodType TextDocumentPrepareRename = Request

132 | methodType TextDocumentFoldingRange = Request

133 | methodType TextDocumentSelectionRange = Request

134 | methodType TextDocumentPrepareCallHierarchy = Request

135 | methodType CallHierarchyIncomingCalls = Request

136 | methodType CallHierarchyOutgoingCalls = Request

137 | methodType TextDocumentSemanticTokensFull = Request

138 | methodType TextDocumentSemanticTokensFullDelta = Request

139 | methodType TextDocumentSemanticTokensRange = Request

140 | methodType WorkspaceSemanticTokensRefresh = Request

141 | methodType TextDocumentLinkedEditingRange = Request

142 | methodType TextDocumentMoniker = Request

143 | methodType LogTrace = Notification

144 | methodType WindowShowMessage = Notification

145 | methodType WindowShowMessageRequest = Request

146 | methodType WindowShowDocument = Request

147 | methodType WindowLogMessage = Notification

148 | methodType WindowWorkDoneProgressCreate = Request

149 | methodType TelemetryEvent = Notification

150 | methodType ClientRegisterCapability = Request

151 | methodType ClientUnregisterCapability = Request

152 | methodType WorkspaceWorkspaceFolders = Request

153 | methodType WorkspaceConfiguration = Request

154 | methodType WorkspaceApplyEdit = Request

155 | methodType TextDocumentPublishDiagnostics = Notification

156 | methodType TextDocumentCompletion = Request

157 | methodType WorkspaceCodeLensRefresh = Request

158 | methodType CancelRequest = Notification

159 | methodType Progress = Notification

162 | ToJSON (Method type from) where

163 |   toJSON Initialize                          = JString "initialize"

164 |   toJSON Initialized                         = JString "initialized"

165 |   toJSON Shutdown                            = JString "shutdown"

166 |   toJSON Exit                                = JString "exit"

167 |   toJSON SetTrace                            = JString "$/setTrace"

168 |   toJSON WindowWorkDoneProgressCancel        = JString "window/workDoneProgress/cancel"

169 |   toJSON WorkspaceDidChangeWorkspaceFolders  = JString "workspace/didChangeWorkspaceFolders"

170 |   toJSON WorkspaceDidChangeConfiguration     = JString "workspace/didChangeConfiguration"

171 |   toJSON WorkspaceDidChangeWatchedFiles      = JString "workspace/didChangeWatchedFiles"

172 |   toJSON WorkspaceSymbol                     = JString "workspace/symbol"

173 |   toJSON WorkspaceExecuteCommand             = JString "workspace/executeCommand"

174 |   toJSON WorkspaceWillCreateFiles            = JString "workspace/willCreateFiles"

175 |   toJSON TextDocumentDidOpen                 = JString "textDocument/didOpen"

176 |   toJSON TextDocumentDidChange               = JString "textDocument/didChange"

177 |   toJSON TextDocumentWillSave                = JString "textDocument/willSave"

178 |   toJSON TextDocumentWillSaveWaitUntil       = JString "textDocument/willSaveWaitUntil"

179 |   toJSON TextDocumentDidSave                 = JString "textDocument/didSave"

180 |   toJSON TextDocumentDidClose                = JString "textDocument/didClose"

181 |   toJSON CompletionItemResolve               = JString "completionItem/resolve"

182 |   toJSON TextDocumentHover                   = JString "textDocument/hover"

183 |   toJSON TextDocumentSignatureHelp           = JString "textDocument/signatureHelp"

184 |   toJSON TextDocumentDeclaration             = JString "textDocument/declaration"

185 |   toJSON TextDocumentDefinition              = JString "textDocument/definition"

186 |   toJSON TextDocumentTypeDefinition          = JString "textDocument/typeDefinition"

187 |   toJSON TextDocumentImplementation          = JString "textDocument/implementation"

188 |   toJSON TextDocumentReferences              = JString "textDocument/references"

189 |   toJSON TextDocumentDocumentHighlight       = JString "textDocument/documentHighlight"

190 |   toJSON TextDocumentDocumentSymbol          = JString "textDocument/documentSymbol"

191 |   toJSON TextDocumentCodeAction              = JString "textDocument/codeAction"

192 |   toJSON CodeActionResolve                   = JString "codeAction/resolve"

193 |   toJSON TextDocumentCodeLens                = JString "textDocument/codeLens"

194 |   toJSON CodeLensResolve                     = JString "codeLens/resolve"

195 |   toJSON TextDocumentDocumentLink            = JString "textDocument/documentLink"

196 |   toJSON DocumentLinkResolve                 = JString "documentLink/resolve"

197 |   toJSON TextDocumentDocumentColor           = JString "textDocument/documentColor"

198 |   toJSON TextDocumentFormatting              = JString "textDocument/formatting"

199 |   toJSON TextDocumentRangeFormatting         = JString "textDocument/rangeFormatting"

200 |   toJSON TextDocumentOnTypeFormatting        = JString "textDocument/onTypeFormatting"

201 |   toJSON TextDocumentRename                  = JString "textDocument/rename"

202 |   toJSON TextDocumentPrepareRename           = JString "textDocument/prepareRename"

203 |   toJSON TextDocumentFoldingRange            = JString "textDocument/foldingRange"

204 |   toJSON TextDocumentSelectionRange          = JString "textDocument/selectionRange"

205 |   toJSON TextDocumentPrepareCallHierarchy    = JString "textDocument/prepareCallHierarchy"

206 |   toJSON CallHierarchyIncomingCalls          = JString "callHierarchy/incomingCalls"

207 |   toJSON CallHierarchyOutgoingCalls          = JString "callHierarchy/outgoingCalls"

208 |   toJSON TextDocumentSemanticTokensFull      = JString "textDocument/semanticTokens/full"

209 |   toJSON TextDocumentSemanticTokensFullDelta = JString "textDocument/semanticTokens/full/delta"

210 |   toJSON TextDocumentSemanticTokensRange     = JString "textDocument/semanticTokens/range"

211 |   toJSON WorkspaceSemanticTokensRefresh      = JString "workspace/semanticTokens/refresh"

212 |   toJSON TextDocumentLinkedEditingRange      = JString "textDocument/linkedEditingRange"

213 |   toJSON TextDocumentMoniker                 = JString "textDocument/moniker"

214 |   toJSON LogTrace                            = JString "$/logTrace"

215 |   toJSON WindowShowMessage                   = JString "window/showMessage"

216 |   toJSON WindowShowMessageRequest            = JString "window/showMessageRequest"

217 |   toJSON WindowShowDocument                  = JString "window/showDocument"

218 |   toJSON WindowLogMessage                    = JString "window/logMessage"

219 |   toJSON WindowWorkDoneProgressCreate        = JString "window/workDoneProgress/create"

220 |   toJSON TelemetryEvent                      = JString "telemetry/event"

221 |   toJSON ClientRegisterCapability            = JString "client/registerCapability"

222 |   toJSON ClientUnregisterCapability          = JString "client/unregisterCapability"

223 |   toJSON WorkspaceWorkspaceFolders           = JString "workspace/workspaceFolders"

224 |   toJSON WorkspaceConfiguration              = JString "workspace/configuration"

225 |   toJSON WorkspaceApplyEdit                  = JString "workspace/applyEdit"

226 |   toJSON TextDocumentPublishDiagnostics      = JString "textDocument/publishDiagnostics"

227 |   toJSON TextDocumentCompletion              = JString "textDocument/completion"

228 |   toJSON WorkspaceCodeLensRefresh            = JString "workspace/codeLens/refresh"

229 |   toJSON CancelRequest                       = JString "$/cancelRequest"

230 |   toJSON Progress                            = JString "$/progress"

233 | FromJSON (Method Client Notification) where

234 |   fromJSON (JString "initialized")                         = pure Initialized

235 |   fromJSON (JString "exit")                                = pure Exit

236 |   fromJSON (JString "$/setTrace")                          = pure SetTrace

237 |   fromJSON (JString "window/workDoneProgress/cancel")      = pure WindowWorkDoneProgressCancel

238 |   fromJSON (JString "workspace/didChangeWorkspaceFolders") = pure WorkspaceDidChangeWorkspaceFolders

239 |   fromJSON (JString "workspace/didChangeConfiguration")    = pure WorkspaceDidChangeConfiguration

240 |   fromJSON (JString "workspace/didChangeWatchedFiles")     = pure WorkspaceDidChangeWatchedFiles

241 |   fromJSON (JString "textDocument/didOpen")                = pure TextDocumentDidOpen

242 |   fromJSON (JString "textDocument/didChange")              = pure TextDocumentDidChange

243 |   fromJSON (JString "textDocument/willSave")               = pure TextDocumentWillSave

244 |   fromJSON (JString "textDocument/didSave")                = pure TextDocumentDidSave

245 |   fromJSON (JString "textDocument/didClose")               = pure TextDocumentDidClose

246 |   fromJSON (JString "$/cancelRequest")                     = pure CancelRequest

247 |   fromJSON (JString "$/progress")                          = pure Progress

248 |   fromJSON _ = neutral

251 | FromJSON (Method Client Request) where

252 |   fromJSON (JString "initialize")                             = pure Initialize

253 |   fromJSON (JString "shutdown")                               = pure Shutdown

254 |   fromJSON (JString "workspace/symbol")                       = pure WorkspaceSymbol

255 |   fromJSON (JString "workspace/executeCommand")               = pure WorkspaceExecuteCommand

256 |   fromJSON (JString "workspace/willCreateFiles")              = pure WorkspaceWillCreateFiles

257 |   fromJSON (JString "textDocument/willSaveWaitUntil")         = pure TextDocumentWillSaveWaitUntil

258 |   fromJSON (JString "textDocument/completion")                = pure TextDocumentCompletion

259 |   fromJSON (JString "completionItem/resolve")                 = pure CompletionItemResolve

260 |   fromJSON (JString "textDocument/hover")                     = pure TextDocumentHover

261 |   fromJSON (JString "textDocument/signatureHelp")             = pure TextDocumentSignatureHelp

262 |   fromJSON (JString "textDocument/declaration")               = pure TextDocumentDeclaration

263 |   fromJSON (JString "textDocument/definition")                = pure TextDocumentDefinition

264 |   fromJSON (JString "textDocument/typeDefinition")            = pure TextDocumentTypeDefinition

265 |   fromJSON (JString "textDocument/implementation")            = pure TextDocumentImplementation

266 |   fromJSON (JString "textDocument/references")                = pure TextDocumentReferences

267 |   fromJSON (JString "textDocument/documentHighlight")         = pure TextDocumentDocumentHighlight

268 |   fromJSON (JString "textDocument/documentSymbol")            = pure TextDocumentDocumentSymbol

269 |   fromJSON (JString "textDocument/codeAction")                = pure TextDocumentCodeAction

270 |   fromJSON (JString "codeAction/resolve")                     = pure CodeActionResolve

271 |   fromJSON (JString "textDocument/codeLens")                  = pure TextDocumentCodeLens

272 |   fromJSON (JString "codeLens/resolve")                       = pure CodeLensResolve

273 |   fromJSON (JString "textDocument/documentLink")              = pure TextDocumentDocumentLink

274 |   fromJSON (JString "documentLink/resolve")                   = pure DocumentLinkResolve

275 |   fromJSON (JString "textDocument/documentColor")             = pure TextDocumentDocumentColor

276 |   fromJSON (JString "textDocument/formatting")                = pure TextDocumentFormatting

277 |   fromJSON (JString "textDocument/rangeFormatting")           = pure TextDocumentRangeFormatting

278 |   fromJSON (JString "textDocument/onTypeFormatting")          = pure TextDocumentOnTypeFormatting

279 |   fromJSON (JString "textDocument/rename")                    = pure TextDocumentRename

280 |   fromJSON (JString "textDocument/prepareRename")             = pure TextDocumentPrepareRename

281 |   fromJSON (JString "textDocument/foldingRange")              = pure TextDocumentFoldingRange

282 |   fromJSON (JString "textDocument/selectionRange")            = pure TextDocumentSelectionRange

283 |   fromJSON (JString "textDocument/prepareCallHierarchy")      = pure TextDocumentPrepareCallHierarchy

284 |   fromJSON (JString "callHierarchy/incomingCalls")            = pure CallHierarchyIncomingCalls

285 |   fromJSON (JString "callHierarchy/outgoingCalls")            = pure CallHierarchyOutgoingCalls

286 |   fromJSON (JString "textDocument/semanticTokens/full")       = pure TextDocumentSemanticTokensFull

287 |   fromJSON (JString "textDocument/semanticTokens/full/delta") = pure TextDocumentSemanticTokensFullDelta

288 |   fromJSON (JString "textDocument/semanticTokens/range")      = pure TextDocumentSemanticTokensRange

289 |   fromJSON (JString "textDocument/linkedEditingRange")        = pure TextDocumentLinkedEditingRange

290 |   fromJSON (JString "textDocument/moniker")                   = pure TextDocumentMoniker

291 |   fromJSON _ = neutral

294 | FromJSON (Method Server Notification) where

295 |   fromJSON (JString "$/logTrace")                      = pure LogTrace

296 |   fromJSON (JString "window/showMessage")              = pure WindowShowMessage

297 |   fromJSON (JString "window/logMessage")               = pure WindowLogMessage

298 |   fromJSON (JString "telemetry/event")                 = pure TelemetryEvent

299 |   fromJSON (JString "textDocument/publishDiagnostics") = pure TextDocumentPublishDiagnostics

300 |   fromJSON (JString "$/cancelRequest")                 = pure CancelRequest

301 |   fromJSON (JString "$/progress")                      = pure Progress

302 |   fromJSON _ = neutral

305 | FromJSON (Method Server Request) where

306 |   fromJSON (JString "window/showMessageRequest")        = pure WindowShowMessageRequest

307 |   fromJSON (JString "window/showDocument")              = pure WindowShowDocument

308 |   fromJSON (JString "window/workDoneProgress/create")   = pure WindowWorkDoneProgressCreate

309 |   fromJSON (JString "client/registerCapability")        = pure ClientRegisterCapability

310 |   fromJSON (JString "client/unregisterCapability")      = pure ClientUnregisterCapability

311 |   fromJSON (JString "workspace/workspaceFolders")       = pure WorkspaceWorkspaceFolders

312 |   fromJSON (JString "workspace/configuration")          = pure WorkspaceConfiguration

313 |   fromJSON (JString "workspace/applyEdit")              = pure WorkspaceApplyEdit

314 |   fromJSON (JString "workspace/codeLens/refresh")       = pure WorkspaceCodeLensRefresh

315 |   fromJSON (JString "workspace/semanticTokens/refresh") = pure WorkspaceSemanticTokensRefresh

316 |   fromJSON _ = neutral

319 | FromJSON (from ** Method from Notification) where

320 |   fromJSON arg =

321 |     (fromJSON arg >>= \meth : Method Client Notification => pure (_ ** meth))

322 |       <|> (fromJSON arg >>= \meth : Method Server Notification => pure (_ ** meth))

325 | FromJSON (from ** Method from Request) where

326 |   fromJSON arg =

327 |     (fromJSON arg >>= \meth : Method Client Request => pure (_ ** meth))

328 |       <|> (fromJSON arg >>= \meth : Method Server Request => pure (_ ** meth))

331 | FromJSON (from ** type ** Method from type) where

332 |   fromJSON arg =

333 |     (fromJSON arg >>= \meth : Method Client Notification => pure (_ ** _ ** meth))

334 |       <|> (fromJSON arg >>= \meth : Method Client Request => pure (_ ** _ ** meth))

335 |       <|> (fromJSON arg >>= \meth : Method Server Notification => pure (_ ** _ ** meth))

336 |       <|> (fromJSON arg >>= \meth : Method Server Request => pure (_ ** _ ** meth))