From 653b6846510ae96434eb13aa2a5f203bdb59d68e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Dec 2021 12:57:09 -0800 Subject: [PATCH] feat: improve `getCompletionKindForDecl` --- src/Lean/Declaration.lean | 4 ++++ src/Lean/Server/Completion.lean | 20 +++++++++---------- tests/lean/interactive/533.lean.expected.out | 10 +++++----- tests/lean/interactive/863.lean.expected.out | 4 ++-- .../interactive/completion6.lean.expected.out | 2 +- .../interactive/completion7.lean.expected.out | 8 ++++---- .../completionPrv.lean.expected.out | 4 ++-- 7 files changed, 28 insertions(+), 24 deletions(-) diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index bdf328aeb5..d01bc64e40 100644 --- a/src/Lean/Declaration.lean +++ b/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 diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 17f59007d5..736b9d53ac 100644 --- a/src/Lean/Server/Completion.lean +++ b/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 diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index 5bca40e81b..24a8bcc14e 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/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} diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out index 95fadddb65..7f3018baed 100644 --- a/tests/lean/interactive/863.lean.expected.out +++ b/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"}, diff --git a/tests/lean/interactive/completion6.lean.expected.out b/tests/lean/interactive/completion6.lean.expected.out index 0bed208ede..d3976fb926 100644 --- a/tests/lean/interactive/completion6.lean.expected.out +++ b/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"}, diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index 77e5278c67..25f83ae60a 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/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} diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out index c43885f0fe..fa49a1af16 100644 --- a/tests/lean/interactive/completionPrv.lean.expected.out +++ b/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}