feat: CodeActionProvider

This is a low-level system for registering LSP code actions.
Developers can register their own code actions.
In future commits I am going to add features on top of this.

src/Lean/Data/Lsp/Basic.lean

@@ -244,6 +244,9 @@ instance : Append WorkspaceEdit where
 def ofTextDocumentEdit (e : TextDocumentEdit) : WorkspaceEdit :=
   { documentChanges := #[DocumentChange.edit e]}
 
+def ofTextEdit (uri : DocumentUri) (te : TextEdit) : WorkspaceEdit :=
+  { changes := RBMap.empty.insert uri #[te]}
+
 end WorkspaceEdit
 
 /-- An item to transfer a text document from the client to the server.

src/Lean/Data/Lsp/CodeActions.lean

@@ -65,7 +65,7 @@ structure CodeActionContext where
     the error state of the resource. The primary parameter
     to compute code actions is the provided range.
   -/
-  diagnostics : Array Diagnostic
+  diagnostics : Array Diagnostic := #[]
   /-- Requested kind of actions to return.
 
     Actions not of this kind are filtered out by the client before being
@@ -80,7 +80,7 @@ structure CodeActionContext where
 structure CodeActionParams extends WorkDoneProgressParams, PartialResultParams where
   textDocument : TextDocumentIdentifier
   range        : Range
-  context      : CodeActionContext
+  context      : CodeActionContext := {}
   deriving FromJson, ToJson
 
 /-- If the code action is disabled, this type gives the reson why. -/
@@ -130,7 +130,7 @@ structure CodeAction extends WorkDoneProgressParams, PartialResultParams where
   /-- A data entry field that is preserved on a code action between a `textDocument/codeAction` and a `codeAction/resolve` request.
   In particular, for Lean-created commands we expect `data` to have a `uri : DocumentUri` field so that `FileSource` can be implemented.
    -/
-  data?        : Option CodeActionData := none
+  data         : CodeActionData
   deriving ToJson, FromJson
 
 structure ResolveSupport where

src/Lean/Server.lean

@@ -7,3 +7,4 @@ Authors: Marc Huisinga, Wojciech Nawrocki
 import Lean.Server.Watchdog
 import Lean.Server.FileWorker
 import Lean.Server.Rpc
+import Lean.Server.CodeActions

src/Lean/Server/CodeActions.lean

@@ -0,0 +1,88 @@
+/-
+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
+-/
+
+import Lean.Server.FileWorker.RequestHandling
+import Lean.Server.InfoUtils
+
+namespace Lean.Server
+
+open Lsp
+open RequestM
+open Snapshots
+
+/-- A code action provider is a function for getting LSP code actions for vscode. You can register them with the `@[codeActionProvider]` 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, we suggest the following approach:
+
+Wrap the long-running computation in a tactic or macro which itself suggests a code action.
+   This means that the long-running computation will be handled in the normal document processing thread.
+   For example, suppose that you want to run some machine learning to suggest the next lemma to use.
+   Rather than run the heavy ML computation in the CodeActionProvider, you could suggest a `by try-ml` tactic. Which once elaborated by Lean will suggest a new lemma.
+ -/
+def CodeActionProvider := CodeActionParams → RequestM (RequestTask (Array CodeAction))
+deriving instance Inhabited for CodeActionProvider
+
+def CodeActionResolver := CodeAction → RequestM (RequestTask CodeAction)
+deriving instance Inhabited for CodeActionResolver
+
+builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
+  name := `codeActionProviderExt,
+  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 registerBuiltinAttribute {
+  name := `codeActionProvider
+  descr := "Use to decorate methods for suggesting code actions."
+  add := fun src _stx _kind => do
+    -- [todo] assert src is a CodeActionProvider
+    modifyEnv (codeActionProviderExt.addEntry · src)
+}
+
+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. -/
+@[implementedBy 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 polling 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
+  bindWaitFindSnap doc (fun s => s.endPos ≥ pos)
+    (notFoundX := return RequestTask.pure #[])
+    fun snap => do
+      let caps ← RequestM.runCoreM snap (do
+        let env ← getEnv
+        let names := codeActionProviderExt.getState env
+        names.foldM (fun b n => b.push <$> evalCodeActionProvider n ) #[]
+      )
+      have : Monad Task := {bind := Task.bind, pure := Task.pure}
+      have : Monad RequestTask := show Monad (ExceptT _ Task) by infer_instance
+      let tasks : Array (RequestTask _) ← caps.mapM (· <| params)
+      let task := tasks.concatMapM id
+      return task
+
+builtin_initialize
+  registerLspRequestHandler "textDocument/codeAction" CodeActionParams (Array CodeAction) handleCodeAction
+
+end Lean.Server

src/Lean/Server/Watchdog.lean

@@ -690,6 +690,7 @@ def mkLeanServerCapabilities : ServerCapabilities := {
     full  := true
     range := true
   }
+  codeActionProvider? := some {  }
 }
 
 def initAndRunWatchdogAux : ServerM Unit := do

tests/lean/interactive/codeaction.lean

@@ -0,0 +1,21 @@
+import Lean
+
+open Lean Server Lsp
+
+@[codeActionProvider]
+def helloProvider : CodeActionProvider := fun (params : CodeActionParams) => do
+  let uri := params.textDocument.uri
+  return RequestTask.pure #[{
+    title := "hello world",
+    kind? := "quickfix",
+    edit? := WorkspaceEdit.ofTextEdit uri {
+      range := params.range,
+      newText := "hello!!!",
+    },
+    data := {uri}
+  }]
+
+theorem asdf : (x : Nat) → x = x := by
+  intro x
+  --^ codeAction
+  rfl

tests/lean/interactive/codeaction.lean.expected.out

@@ -0,0 +1,12 @@
+{"title": "hello world",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges": [],
+  "changes":
+  {"file://codeaction.lean":
+   [{"range":
+     {"start": {"line": 18, "character": 4},
+      "end": {"line": 18, "character": 4}},
+     "newText": "hello!!!"}]},
+  "changeAnnotations": {}},
+ "data": {"uri": "file://codeaction.lean"}}

tests/lean/interactive/run.lean

@@ -107,6 +107,16 @@ partial def main (args : List String) : IO Unit := do
           for diag in diags do
             IO.eprintln (toJson diag.param)
           requestNo := requestNo + 1
+        | "codeAction" =>
+          let params : CodeActionParams := {
+            textDocument := {uri := uri},
+            range := ⟨pos, pos⟩
+          }
+          Ipc.writeRequest ⟨requestNo, "textDocument/codeAction", params⟩
+          let r ← Ipc.readResponseAs requestNo (Array Json)
+          for x in r.result do
+            IO.eprintln x
+          requestNo := requestNo + 1
         | "goals" =>
           if rpcSessionId.isNone then
             Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩