feat: improve getCompletionKindForDecl

src/Lean/Declaration.lean

@@ -374,6 +374,10 @@ def isCtor : ConstantInfo → Bool
   | ctorInfo _ => true
   | _          => false
 
+def isInductive : ConstantInfo → Bool
+  | inductInfo _ => true
+  | _            => false
+
 @[extern "lean_instantiate_type_lparams"]
 constant instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr
 

src/Lean/Server/Completion.lean

@@ -85,10 +85,15 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
   let env ← getEnv
   if constInfo.isCtor then
     return CompletionItemKind.constructor
-  else if isStructure env constInfo.name then
-    return CompletionItemKind.struct
-  else if (← isEnumType constInfo.name) then
-    return CompletionItemKind.enum
+  else if constInfo.isInductive then
+    if (← isClass env constInfo.name) then
+      return CompletionItemKind.class
+    else if (← isEnumType constInfo.name) then
+      return CompletionItemKind.enum
+    else
+      return CompletionItemKind.struct
+  else if (← isProjectionFn constInfo.name) then
+    return CompletionItemKind.field
   else if (← whnf constInfo.type).isForall then
     return CompletionItemKind.function
   else
@@ -310,12 +315,7 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (hoverInfo : Hov
         if nameSet.contains typeName then
           unless (← isBlackListed c.name) do
             if (← isDotCompletionMethod typeName c) then
-              let kind :=
-                if (← isProjectionFn c.name) then
-                  CompletionItemKind.field
-                else
-                  CompletionItemKind.method
-              addCompletionItem c.name.getString! c.type expectedType? c.name (kind := kind)
+              addCompletionItem c.name.getString! c.type expectedType? c.name (kind := (← getCompletionKindForDecl c))
 
 private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option CompletionList) :=
   ctx.runMetaM {} do

tests/lean/interactive/533.lean.expected.out

@@ -1,22 +1,22 @@
 {"textDocument": {"uri": "file://533.lean"},
  "position": {"line": 1, "character": 10}}
 {"items":
- [{"label": "False", "kind": 21, "detail": "Prop"},
+ [{"label": "False", "kind": 22, "detail": "Prop"},
   {"label": "Fin", "kind": 22, "detail": "Nat → Type"},
   {"label": "Float", "kind": 22, "detail": "Type"},
   {"label": "FloatArray", "kind": 22, "detail": "Type"},
   {"label": "FloatSpec", "kind": 22, "detail": "Type 1"},
   {"label": "Foo", "kind": 6, "detail": "Sort ?u"},
   {"label": "ForIn",
-   "kind": 22,
+   "kind": 7,
    "detail":
    "(Type u₁ → Type u₂) → Type u → outParam (Type v) → Type (max (max (max u (u₁ + 1)) u₂) v)"},
-  {"label": "ForInStep", "kind": 3, "detail": "Type u → Type u"},
+  {"label": "ForInStep", "kind": 22, "detail": "Type u → Type u"},
   {"label": "ForM",
-   "kind": 22,
+   "kind": 7,
    "detail":
    "(Type u → Type v) → Type w₁ → outParam (Type w₂) → Type (max (max (max (u + 1) v) w₁) w₂)"},
   {"label": "Functor",
-   "kind": 22,
+   "kind": 7,
    "detail": "(Type u → Type v) → Type (max (u + 1) v)"}],
  "isIncomplete": true}

tests/lean/interactive/863.lean.expected.out

@@ -8,7 +8,7 @@
   {"label": "getReducibilityStatusImp",
    "kind": 3,
    "detail": "Environment → Name → ReducibilityStatus"},
-  {"label": "getRef", "kind": 3, "detail": "[self : MonadRef m] → m Syntax"},
+  {"label": "getRef", "kind": 5, "detail": "[self : MonadRef m] → m Syntax"},
   {"label": "getRegularInitFnNameFor?",
    "kind": 3,
    "detail": "Environment → Name → Option Name"},
@@ -26,7 +26,7 @@
   {"label": "getReducibilityStatusImp",
    "kind": 3,
    "detail": "Environment → Name → ReducibilityStatus"},
-  {"label": "getRef", "kind": 3, "detail": "[self : MonadRef m] → m Syntax"},
+  {"label": "getRef", "kind": 5, "detail": "[self : MonadRef m] → m Syntax"},
   {"label": "getRegularInitFnNameFor?",
    "kind": 3,
    "detail": "Environment → Name → Option Name"},

tests/lean/interactive/completion6.lean.expected.out

@@ -11,7 +11,7 @@
  "position": {"line": 21, "character": 4}}
 {"items":
  [{"label": "b1", "kind": 5, "detail": "C → String"},
-  {"label": "doubleF1", "kind": 2, "detail": "E → Nat"},
+  {"label": "doubleF1", "kind": 3, "detail": "E → Nat"},
   {"label": "f1", "kind": 5, "detail": "C → Nat"},
   {"label": "f2", "kind": 5, "detail": "C → Bool"},
   {"label": "f3", "kind": 5, "detail": "D → Bool"},

tests/lean/interactive/completion7.lean.expected.out

@@ -2,13 +2,13 @@
  "position": {"line": 0, "character": 10}}
 {"items":
  [{"label": "And", "kind": 22, "detail": "Prop → Prop → Prop"},
-  {"label": "AndOp", "kind": 22, "detail": "Type u → Type u"},
-  {"label": "AndThen", "kind": 22, "detail": "Type u → Type u"}],
+  {"label": "AndOp", "kind": 7, "detail": "Type u → Type u"},
+  {"label": "AndThen", "kind": 7, "detail": "Type u → Type u"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion7.lean"},
  "position": {"line": 2, "character": 11}}
 {"items":
  [{"label": "intro", "kind": 4, "detail": "a → b → a ∧ b"},
-  {"label": "left", "kind": 3, "detail": "a ∧ b → a"},
-  {"label": "right", "kind": 3, "detail": "a ∧ b → b"}],
+  {"label": "left", "kind": 5, "detail": "a ∧ b → a"},
+  {"label": "right", "kind": 5, "detail": "a ∧ b → b"}],
  "isIncomplete": true}

tests/lean/interactive/completionPrv.lean.expected.out

@@ -10,11 +10,11 @@
  "position": {"line": 21, "character": 5}}
 {"items":
  [{"label": "field1", "kind": 5, "detail": "S → Nat"},
-  {"label": "getInc", "kind": 2, "detail": "S → Nat"}],
+  {"label": "getInc", "kind": 3, "detail": "S → Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completionPrv.lean"},
  "position": {"line": 25, "character": 4}}
 {"items":
  [{"label": "field1", "kind": 5, "detail": "S → Nat"},
-  {"label": "getInc", "kind": 2, "detail": "S → Nat"}],
+  {"label": "getInc", "kind": 3, "detail": "S → Nat"}],
  "isIncomplete": true}