From a0a4b9faecbf15d5cd6315ed12ebdd5f6a661cd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Apr 2021 11:38:36 -0700 Subject: [PATCH] fix: filter declarations that are not valid dot methods --- src/Lean/Server/Completion.lean | 13 ++++++++++-- .../interactive/completion.lean.expected.out | 20 ++++--------------- .../interactive/completion3.lean.expected.out | 4 ---- .../interactive/completion4.lean.expected.out | 10 +--------- .../interactive/completion5.lean.expected.out | 3 +-- .../editCompletion.lean.expected.out | 5 +---- 6 files changed, 18 insertions(+), 37 deletions(-) diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index c77b92bc87..caf752543f 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -176,23 +176,32 @@ private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (stx : Syntax runM ctx lctx do idCompletionCore ctx stx expectedType? +private def isDotCompletionMethod (info : ConstantInfo) : MetaM Bool := + forallTelescopeReducing info.type fun xs _ => do + for x in xs do + let localDecl ← getLocalDecl x.fvarId! + if localDecl.type.getAppFn.isConstOf info.name.getPrefix then + return true + return false + private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? : Option Expr) : IO (Option CompletionList) := runM ctx info.lctx do let name? ← try let type ← instantiateMVars (← inferType info.expr) + -- dbg_trace "dot >> {info.stx}, {info.expr} : {type}, {info.stx.isIdent}" match type.getAppFn with | Expr.const name .. => pure (some name) | _ => pure none catch _ => pure none - -- dbg_trace "dot >> {info.stx}, {info.expr} : {type}, {info.stx.isIdent}" match name? with | some name => (← getEnv).constants.forM fun declName c => do if declName.getPrefix == name then unless (← isBlackListed c.name) do - addCompletionItem c.name.getString! c.type expectedType? + if (← isDotCompletionMethod c) then + addCompletionItem c.name.getString! c.type expectedType? | _ => if info.stx.isIdent then idCompletionCore ctx info.stx expectedType? diff --git a/tests/lean/interactive/completion.lean.expected.out b/tests/lean/interactive/completion.lean.expected.out index 671ed4ed66..58a45e104d 100644 --- a/tests/lean/interactive/completion.lean.expected.out +++ b/tests/lean/interactive/completion.lean.expected.out @@ -1,24 +1,12 @@ {"textDocument": {"uri": "file://completion.lean"}, "position": {"line": 3, "character": 22}} -{"items": - [{"label": "foo", "detail": "Foo → Nat"}, - {"label": "mk", "detail": "Nat → Foo"}], - "isIncomplete": true} +{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion.lean"}, "position": {"line": 5, "character": 23}} -{"items": - [{"label": "foo", "detail": "Foo → Nat"}, - {"label": "mk", "detail": "Nat → Foo"}], - "isIncomplete": true} +{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion.lean"}, "position": {"line": 7, "character": 28}} -{"items": - [{"label": "foo", "detail": "Foo → Nat"}, - {"label": "mk", "detail": "Nat → Foo"}], - "isIncomplete": true} +{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion.lean"}, "position": {"line": 9, "character": 29}} -{"items": - [{"label": "foo", "detail": "Foo → Nat"}, - {"label": "mk", "detail": "Nat → Foo"}], - "isIncomplete": true} +{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion3.lean.expected.out b/tests/lean/interactive/completion3.lean.expected.out index 6aeffd3c63..047437997c 100644 --- a/tests/lean/interactive/completion3.lean.expected.out +++ b/tests/lean/interactive/completion3.lean.expected.out @@ -2,7 +2,6 @@ "position": {"line": 7, "character": 9}} {"items": [{"label": "b", "detail": "S → Bool"}, - {"label": "mk", "detail": "Nat → String → Bool → S"}, {"label": "x", "detail": "S → Nat"}, {"label": "y", "detail": "S → String"}], "isIncomplete": true} @@ -10,7 +9,6 @@ "position": {"line": 12, "character": 5}} {"items": [{"label": "b", "detail": "S → Bool"}, - {"label": "mk", "detail": "Nat → String → Bool → S"}, {"label": "x", "detail": "S → Nat"}, {"label": "y", "detail": "S → String"}], "isIncomplete": true} @@ -18,7 +16,6 @@ "position": {"line": 16, "character": 5}} {"items": [{"label": "b", "detail": "S → Bool"}, - {"label": "mk", "detail": "Nat → String → Bool → S"}, {"label": "x", "detail": "S → Nat"}, {"label": "y", "detail": "S → String"}], "isIncomplete": true} @@ -27,6 +24,5 @@ {"items": [{"label": "x", "detail": "S → Nat"}, {"label": "b", "detail": "S → Bool"}, - {"label": "mk", "detail": "Nat → String → Bool → S"}, {"label": "y", "detail": "S → String"}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion4.lean.expected.out b/tests/lean/interactive/completion4.lean.expected.out index 4ceca263c5..2afcabafdf 100644 --- a/tests/lean/interactive/completion4.lean.expected.out +++ b/tests/lean/interactive/completion4.lean.expected.out @@ -3,8 +3,6 @@ {"items": [{"label": "fn1", "detail": "S → Nat → IO Unit"}, {"label": "fn2", "detail": "S → Bool → IO Unit"}, - {"label": "mk", - "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"}, {"label": "pred", "detail": "S → String → Bool"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion4.lean"}, @@ -12,8 +10,6 @@ {"items": [{"label": "fn1", "detail": "S → Nat → IO Unit"}, {"label": "fn2", "detail": "S → Bool → IO Unit"}, - {"label": "mk", - "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"}, {"label": "pred", "detail": "S → String → Bool"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion4.lean"}, @@ -21,16 +17,12 @@ {"items": [{"label": "fn1", "detail": "S → Nat → IO Unit"}, {"label": "fn2", "detail": "S → Bool → IO Unit"}, - {"label": "mk", - "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"}, {"label": "pred", "detail": "S → String → Bool"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion4.lean"}, "position": {"line": 20, "character": 21}} {"items": - [{"label": "mk", - "detail": "(Nat → IO Unit) → (Bool → IO Unit) → (String → Bool) → S"}, - {"label": "fn1", "detail": "S → Nat → IO Unit"}, + [{"label": "fn1", "detail": "S → Nat → IO Unit"}, {"label": "fn2", "detail": "S → Bool → IO Unit"}, {"label": "pred", "detail": "S → String → Bool"}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion5.lean.expected.out b/tests/lean/interactive/completion5.lean.expected.out index c3f14336b9..f045f3d5bd 100644 --- a/tests/lean/interactive/completion5.lean.expected.out +++ b/tests/lean/interactive/completion5.lean.expected.out @@ -1,8 +1,7 @@ {"textDocument": {"uri": "file://completion5.lean"}, "position": {"line": 9, "character": 15}} {"items": - [{"label": "mk", "detail": "Nat → Bool → String → C"}, - {"label": "b1", "detail": "C → String"}, + [{"label": "b1", "detail": "C → String"}, {"label": "f1", "detail": "C → Nat"}, {"label": "f2", "detail": "C → Bool"}], "isIncomplete": true} diff --git a/tests/lean/interactive/editCompletion.lean.expected.out b/tests/lean/interactive/editCompletion.lean.expected.out index bdde565cc8..01166e596b 100644 --- a/tests/lean/interactive/editCompletion.lean.expected.out +++ b/tests/lean/interactive/editCompletion.lean.expected.out @@ -6,7 +6,4 @@ "end": {"line": 3, "character": 22}}}]} {"textDocument": {"uri": "file://editCompletion.lean"}, "position": {"line": 3, "character": 22}} -{"items": - [{"label": "foo", "detail": "Foo → Nat"}, - {"label": "mk", "detail": "Nat → Foo"}], - "isIncomplete": true} +{"items": [{"label": "foo", "detail": "Foo → Nat"}], "isIncomplete": true}