/
Basic.lean
168 lines (141 loc) · 7.32 KB
/
Basic.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
/-
Copyright (c) 2022 E.W.Ayers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: E.W.Ayers
-/
prelude
import Lean.Server.FileWorker.RequestHandling
import Lean.Server.InfoUtils
namespace Lean.Server
open Lsp
open RequestM
open Snapshots
/-- A code action optionally supporting a lazy code action computation that is only run when the user clicks on
the code action in the editor.
If you want to use the lazy feature, make sure that the `edit?` field on the `eager` code action result is `none`.
-/
structure LazyCodeAction where
/-- This is the initial code action that is sent to the server, to implement -/
eager : CodeAction
lazy? : Option (IO CodeAction) := none
/-- Passed as the `data?` field of `Lsp.CodeAction` to recover the context of the code action. -/
structure CodeActionResolveData where
params : CodeActionParams
/-- Name of CodeActionProvider that produced this request. -/
providerName : Name
/-- Index in the list of code action that the given provider generated. -/
providerResultIndex : Nat
deriving ToJson, FromJson
def CodeAction.getFileSource! (ca : CodeAction) : DocumentUri :=
let r : Except String DocumentUri := do
let some data := ca.data?
| throw s!"no data param on code action {ca.title}"
let data : CodeActionResolveData ← fromJson? data
return data.params.textDocument.uri
match r with
| Except.ok uri => uri
| Except.error e => panic! e
instance : FileSource CodeAction where
fileSource x := CodeAction.getFileSource! x
instance : Coe CodeAction LazyCodeAction where
coe c := { eager := c }
/-- A code action provider is a function for providing LSP code actions for an editor.
You can register them with the `@[code_action_provider]` attribute.
This is a low-level interface for making LSP code actions.
This interface can be used to implement the following applications:
- refactoring code: adding underscores to unused variables,
- suggesting imports
- document-level refactoring: removing unused imports, sorting imports, formatting.
- Helper suggestions for working with type holes (`_`)
- Helper suggestions for tactics.
When implementing your own `CodeActionProvider`, we assume that no long-running computations are allowed.
If you need to create a code-action with a long-running computation, you can use the `lazy?` field on `LazyCodeAction`
to perform the computation after the user has clicked on the code action in their editor.
-/
def CodeActionProvider := CodeActionParams → Snapshot → RequestM (Array LazyCodeAction)
deriving instance Inhabited for CodeActionProvider
private builtin_initialize builtinCodeActionProviders : IO.Ref (NameMap CodeActionProvider) ←
IO.mkRef ∅
def addBuiltinCodeActionProvider (decl : Name) (provider : CodeActionProvider) : IO Unit :=
builtinCodeActionProviders.modify (·.insert decl provider)
builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
addEntryFn := fun s n => s.insert n
toArrayFn := fun es => es.toArray.qsort Name.quickLt
}
builtin_initialize
let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
name
descr := (if builtin then "(builtin) " else "") ++
"Use to decorate methods for suggesting code actions. This is a low-level interface for making code actions."
applicationTime := .afterCompilation
add := fun decl stx kind => do
Attribute.Builtin.ensureNoArgs stx
unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
unless (← getConstInfo decl).type.isConstOf ``CodeActionProvider do
throwError "invalid attribute '{name}', must be of type `Lean.Server.CodeActionProvider`"
let env ← getEnv
if builtin then
let h := mkConst decl
declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinCodeActionProvider) (toExpr decl) h
else
setEnv <| codeActionProviderExt.addEntry env decl
}
mkAttr true `builtin_code_action_provider
mkAttr false `code_action_provider
private unsafe def evalCodeActionProviderUnsafe [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider := do
evalConstCheck CodeActionProvider ``CodeActionProvider declName
/-- Get a `CodeActionProvider` from a declaration name. -/
@[implemented_by evalCodeActionProviderUnsafe]
private opaque evalCodeActionProvider [MonadEnv M] [MonadOptions M] [MonadError M] [Monad M] (declName : Name) : M CodeActionProvider
/-- Handles a `textDocument/codeAction` request.
This is implemented by calling all of the registered `CodeActionProvider` functions.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_codeAction). -/
def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array CodeAction)) := do
let doc ← readDoc
let pos := doc.meta.text.lspPosToUtf8Pos params.range.end
withWaitFindSnap doc (fun s => s.endPos ≥ pos)
(notFoundX := return #[])
fun snap => do
let caps ← RequestM.runCoreM snap do
let env ← getEnv
let names := codeActionProviderExt.getState env |>.toArray
let caps ← names.mapM evalCodeActionProvider
return (← builtinCodeActionProviders.get).toList.toArray ++ Array.zip names caps
caps.concatMapM fun (providerName, cap) => do
let cas ← cap params snap
cas.mapIdxM fun i lca => do
if lca.lazy?.isNone then return lca.eager
let data : CodeActionResolveData := {
params, providerName, providerResultIndex := i
}
let j : Json := toJson data
let ca := { lca.eager with data? := some j }
return ca
builtin_initialize
registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction
/-- Handler for `"codeAction/resolve"`.
[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeAction_resolve)
-/
def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAction) := do
let doc ← readDoc
let some data := param.data?
| throw (RequestError.invalidParams "Expected a data field on CodeAction.")
let data : CodeActionResolveData ← liftExcept <| Except.mapError RequestError.invalidParams <| fromJson? data
let pos := doc.meta.text.lspPosToUtf8Pos data.params.range.end
withWaitFindSnap doc (fun s => s.endPos ≥ pos)
(notFoundX := throw <| RequestError.internalError "snapshot not found")
fun snap => do
let cap ← match (← builtinCodeActionProviders.get).find? data.providerName with
| some cap => pure cap
| none => RequestM.runCoreM snap <| evalCodeActionProvider data.providerName
let cas ← cap data.params snap
let some ca := cas[data.providerResultIndex]?
| throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."
let some lazy := ca.lazy?
| throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve."
let r ← liftM lazy
return r
builtin_initialize
registerLspRequestHandler "codeAction/resolve" CodeAction CodeAction handleCodeActionResolve
end Lean.Server