From 68120b24b8f88bfd0e08bacd576a7ea5582beec3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 28 Oct 2021 08:13:44 -0700
Subject: [PATCH] feat: add docstring to `CompletionItem`

closes #746
---
 src/Lean/Server/Completion.lean                | 18 ++++++++++--------
 .../lean/interactive/completionDocString.lean  |  2 ++
 .../completionDocString.lean.expected.out      | 10 ++++++++++
 3 files changed, 22 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/interactive/completionDocString.lean
 create mode 100644 tests/lean/interactive/completionDocString.lean.expected.out

diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 25f369dfc4..f4bc7d5c83 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -62,9 +62,10 @@ private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM
 private def sortCompletionItems (items : Array CompletionItem) : Array CompletionItem :=
   items.qsort fun i1 i2 => i1.label < i2.label
 
-private def mkCompletionItem (label : Name) (type : Expr) : MetaM CompletionItem := do
+private def mkCompletionItem (label : Name) (type : Expr) (docString? : Option String) : MetaM CompletionItem := do
+  let doc? := docString?.map fun docString => { value := docString, kind := MarkupKind.markdown : MarkupContent }
   let detail ← Meta.ppExpr (← consumeImplicitPrefix type)
-  return { label := label.getString!, detail? := some (toString detail), documentation? := none }
+  return { label := label.getString!, detail? := some (toString detail), documentation? := doc? }
 
 structure State where
   itemsMain  : Array CompletionItem := #[]
@@ -72,8 +73,9 @@ structure State where
 
 abbrev M := OptionT $ StateRefT State MetaM
 
-private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Option Expr) : M Unit := do
-  let item ← mkCompletionItem label type
+private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Option Expr) (declName? : Option Name) : M Unit := do
+  let docString? := if let some declName := declName? then findDocString? (← getEnv) declName else none
+  let item ← mkCompletionItem label type docString?
   if (← isTypeApplicable  type expectedType?) then
     modify fun s => { s with itemsMain := s.itemsMain.push item }
   else
@@ -81,7 +83,7 @@ private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Opti
 
 private def addCompletionItemForDecl (label : Name) (declName : Name) (expectedType? : Option Expr) : M Unit := do
   if let some c ← (← getEnv).find? declName then
-    addCompletionItem label c.type expectedType?
+    addCompletionItem label c.type expectedType? (some declName)
 
 private def runM (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) : IO (Option CompletionList) :=
   ctx.runMetaM lctx do
@@ -141,7 +143,7 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (danglingDot : Bool
     -- search for matches in the local context
     for localDecl in (← getLCtx) do
       if matchAtomic id localDecl.userName then
-        addCompletionItem localDecl.userName localDecl.type expectedType?
+        addCompletionItem localDecl.userName localDecl.type expectedType? none
   -- search for matches in the environment
   let env ← getEnv
   env.constants.forM fun declName c => do
@@ -149,7 +151,7 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (danglingDot : Bool
       let matchUsingNamespace (ns : Name): M Bool := do
         if let some label ← matchDecl? ns id danglingDot declName then
           -- dbg_trace "matched with {id}, {declName}, {label}"
-          addCompletionItem label c.type expectedType?
+          addCompletionItem label c.type expectedType? declName
           return true
         else
           return false
@@ -240,7 +242,7 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? :
         if nameSet.contains typeName then
           unless (← isBlackListed c.name) do
             if (← isDotCompletionMethod typeName c) then
-              addCompletionItem c.name.getString! c.type expectedType?
+              addCompletionItem c.name.getString! c.type expectedType? c.name
 
 private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option CompletionList) :=
   ctx.runMetaM {} do
diff --git a/tests/lean/interactive/completionDocString.lean b/tests/lean/interactive/completionDocString.lean
new file mode 100644
index 0000000000..51b7de4e46
--- /dev/null
+++ b/tests/lean/interactive/completionDocString.lean
@@ -0,0 +1,2 @@
+#eval Array.insertAt
+                  --^ textDocument/completion
diff --git a/tests/lean/interactive/completionDocString.lean.expected.out b/tests/lean/interactive/completionDocString.lean.expected.out
new file mode 100644
index 0000000000..c6a81973df
--- /dev/null
+++ b/tests/lean/interactive/completionDocString.lean.expected.out
@@ -0,0 +1,10 @@
+{"textDocument": {"uri": "file://completionDocString.lean"},
+ "position": {"line": 0, "character": 20}}
+{"items":
+ [{"label": "insertAt",
+   "documentation":
+   {"value": "Insert element `a` at position `i`.\n  Pre: `i < as.size` ",
+    "kind": "markdown"},
+   "detail": "Array ?α → Nat → ?α → Array ?α"},
+  {"label": "insertAtAux", "detail": "Nat → Array ?α → Nat → Array ?α"}],
+ "isIncomplete": true}