diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index b2fac12e63..15fe2aed0c 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -69,7 +69,7 @@ private def sortCompletionItems (items : Array (CompletionItem × Float)) : Arra private def mkCompletionItem (label : Name) (type : Expr) (docString? : Option String) (kind : CompletionItemKind) : MetaM CompletionItem := do let doc? := docString?.map fun docString => { value := docString, kind := MarkupKind.markdown : MarkupContent } let detail ← consumeImplicitPrefix type fun type => return toString (← Meta.ppExpr type) - return { label := label.getString!, detail? := detail, documentation? := doc?, kind? := kind } + return { label := label.toString, detail? := detail, documentation? := doc?, kind? := kind } structure State where itemsMain : Array (CompletionItem × Float) := #[] @@ -148,24 +148,23 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : | return none if !ns.isPrefixOf declName then return none - else - let declName := declName.replacePrefix ns Name.anonymous - if id.isPrefixOf declName && danglingDot then + let declName := declName.replacePrefix ns Name.anonymous + if danglingDot then + -- If the input is `id.` and `declName` is of the form `id.atomic`, complete with `atomicName` + if id.isPrefixOf declName then let declName := declName.replacePrefix id Name.anonymous if declName.isAtomic && !declName.isAnonymous then return some (declName, 1) - else - return none - else if !danglingDot then - match id, declName with - | .str p₁ s₁, .str p₂ s₂ => - if p₁ == p₂ then - return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (s₂, ·) - else - return none - | _, _ => return none - else - return none + else if let (.str p₁ s₁, .str p₂ s₂) := (id, declName) then + if p₁ == p₂ then + -- If the namespaces agree, fuzzy-match on the trailing part + return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (s₂, ·) + else if p₁.isAnonymous then + -- If `id` is namespace-less, also fuzzy-match declaration names in arbitrary namespaces + -- (but don't match the namespace itself). + -- Penalize score by component length of added namespace. + return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (declName, · / (p₂.getNumParts + 1).toFloat) + return none /-- Truncate the given identifier and make sure it has length `≤ newLength`. @@ -254,8 +253,6 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI return true else return false - if (← matchUsingNamespace Name.anonymous) then - return () -- use current namespace let rec visitNamespaces (ns : Name) : M Bool := do match ns with @@ -271,6 +268,8 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI if (← matchUsingNamespace ns) then return () | _ => pure () + if (← matchUsingNamespace Name.anonymous) then + return () -- Recall that aliases may not be atomic and include the namespace where they were created. let matchAlias (ns : Name) (alias : Name) : Option Float := if ns.isPrefixOf alias then @@ -281,14 +280,14 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do declNames.forM fun declName => do unless (← isBlackListed declName) do - addCompletionItemForDecl alias declName expectedType? score - -- search explicitily open `ids` + addCompletionItemForDecl alias.getString! declName expectedType? score + -- search explicitly open `ids` for openDecl in ctx.openDecls do match openDecl with | OpenDecl.explicit openedId resolvedId => unless (← isBlackListed resolvedId) do if let some score := matchAtomic id openedId then - addCompletionItemForDecl openedId resolvedId expectedType? score + addCompletionItemForDecl openedId.getString! resolvedId expectedType? score | OpenDecl.simple ns _ => getAliasState env |>.forM fun alias declNames => do if let some score := matchAlias ns alias then diff --git a/tests/lean/interactive/1659.lean b/tests/lean/interactive/1659.lean new file mode 100644 index 0000000000..852561239f --- /dev/null +++ b/tests/lean/interactive/1659.lean @@ -0,0 +1,35 @@ +prelude + +/-! Completing declaration names in arbitrary namespaces -/ + +axiom Lean.Elab.Term.elabTermEnsuringType : Type +axiom Lean.Elab.Tactic.elabTermEnsuringType : Type + +-- adding full namespace + +#check elabTermEnsuring + --^ textDocument/completion + +-- adding partial namespace + +open Lean.Elab in +#check elabTermEnsuring + --^ textDocument/completion + +-- direct + indirect match + +open Lean.Elab.Term in +#check elabTermEnsuring + --^ textDocument/completion + +-- same, on the top level + +axiom elabTermEnsuringType : Type +#check elabTermEnsuring + --^ textDocument/completion + +-- prioritize smaller prefixes + +axiom Lean.Elab.elabTermEnsuringType : Type +#check elabTermEnsuring + --^ textDocument/completion diff --git a/tests/lean/interactive/1659.lean.expected.out b/tests/lean/interactive/1659.lean.expected.out new file mode 100644 index 0000000000..c2fe11449b --- /dev/null +++ b/tests/lean/interactive/1659.lean.expected.out @@ -0,0 +1,47 @@ +{"textDocument": {"uri": "file://1659.lean"}, + "position": {"line": 9, "character": 23}} +{"items": + [{"label": "Lean.Elab.Tactic.elabTermEnsuringType", + "kind": 21, + "detail": "Type"}, + {"label": "Lean.Elab.Term.elabTermEnsuringType", + "kind": 21, + "detail": "Type"}], + "isIncomplete": true} +{"textDocument": {"uri": "file://1659.lean"}, + "position": {"line": 15, "character": 23}} +{"items": + [{"label": "Tactic.elabTermEnsuringType", "kind": 21, "detail": "Type"}, + {"label": "Term.elabTermEnsuringType", "kind": 21, "detail": "Type"}], + "isIncomplete": true} +{"textDocument": {"uri": "file://1659.lean"}, + "position": {"line": 21, "character": 23}} +{"items": + [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, + {"label": "Lean.Elab.Tactic.elabTermEnsuringType", + "kind": 21, + "detail": "Type"}], + "isIncomplete": true} +{"textDocument": {"uri": "file://1659.lean"}, + "position": {"line": 27, "character": 23}} +{"items": + [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, + {"label": "Lean.Elab.Tactic.elabTermEnsuringType", + "kind": 21, + "detail": "Type"}, + {"label": "Lean.Elab.Term.elabTermEnsuringType", + "kind": 21, + "detail": "Type"}], + "isIncomplete": true} +{"textDocument": {"uri": "file://1659.lean"}, + "position": {"line": 33, "character": 23}} +{"items": + [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, + {"label": "Lean.Elab.elabTermEnsuringType", "kind": 21, "detail": "Type"}, + {"label": "Lean.Elab.Tactic.elabTermEnsuringType", + "kind": 21, + "detail": "Type"}, + {"label": "Lean.Elab.Term.elabTermEnsuringType", + "kind": 21, + "detail": "Type"}], + "isIncomplete": true} diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out index bc2651a518..0dc92d70df 100644 --- a/tests/lean/interactive/863.lean.expected.out +++ b/tests/lean/interactive/863.lean.expected.out @@ -1,10 +1,16 @@ {"textDocument": {"uri": "file://863.lean"}, "position": {"line": 9, "character": 12}} {"items": - [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}], + [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}, + {"label": "MonadRef.getRef", + "kind": 5, + "detail": "[self : MonadRef] → Type"}], "isIncomplete": true} {"textDocument": {"uri": "file://863.lean"}, "position": {"line": 13, "character": 12}} {"items": - [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}], + [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}, + {"label": "MonadRef.getRef", + "kind": 5, + "detail": "[self : MonadRef] → Type"}], "isIncomplete": true}