From 2594a8edadd163ba579fc4a7b5a989650f65edda Mon Sep 17 00:00:00 2001 From: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Date: Thu, 22 May 2025 13:58:47 +0200 Subject: [PATCH] fix: namespace completion to only use the short name (#8350) This PR changes namespace completion to use the same algorithm as declaration identifier completion, which makes it use the short name (last name component) for completions instead of the full name, avoiding namespace duplications. Closes #5654 --- .../Completion/CompletionCollectors.lean | 95 +++++++------------ .../Server/Completion/CompletionUtils.lean | 4 +- .../compNamespace.lean.expected.out | 2 +- 3 files changed, 37 insertions(+), 64 deletions(-) diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 806c1b924d..628801e9b4 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -209,43 +209,43 @@ section IdCompletionUtils (Name.mkStr p (s.extract 0 ⟨newLen - optDot - len⟩), newLen) (go id).1 - def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Bool := - if danglingDot then - if nsFragment != ns && nsFragment.isPrefixOf ns then - true - else - false - else - match ns, nsFragment with - | .str p₁ s₁, .str p₂ s₂ => - if p₁ == p₂ then s₂.charactersIn s₁ else false - | _, _ => false + def bestLabelForDecl? (ctx : ContextInfo) (declName : Name) (id : Name) (danglingDot : Bool) : + M (Option Name) := Prod.snd <$> StateT.run (s := none) do + let matchUsingNamespace (ns : Name) : StateT (Option Name) M Unit := do + let some label ← matchDecl? ns id danglingDot declName + | return + modify fun + | none => + some label + | some bestLabel => + -- for open namespaces `A` and `A.B` and a decl `A.B.c`, pick the decl `c` over `B.c` + if label.isSuffixOf bestLabel then + some label + else + some bestLabel + let rec visitNamespaces (ns : Name) : StateT (Option Name) M Unit := do + let Name.str p .. := ns + | return () + matchUsingNamespace ns + visitNamespaces p + -- use current namespace + visitNamespaces ctx.currNamespace + -- use open decls + for openDecl in ctx.openDecls do + let OpenDecl.simple ns exs := openDecl + | pure () + if exs.contains declName then + continue + matchUsingNamespace ns + matchUsingNamespace Name.anonymous def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M Unit := do let env ← getEnv - let add (ns : Name) (ns' : Name) : M Unit := - if danglingDot then - addNamespaceCompletionItem (ns.replacePrefix (ns' ++ id) Name.anonymous) - else - addNamespaceCompletionItem (ns.replacePrefix ns' Name.anonymous) env.getNamespaceSet |>.forM fun ns => do unless ns.isInternal || env.contains ns do -- Ignore internal and namespaces that are also declaration names - for openDecl in ctx.openDecls do - match openDecl with - | OpenDecl.simple ns' _ => - if matchNamespace ns (ns' ++ id) danglingDot then - add ns ns' - return () - | _ => pure () - -- use current namespace - let rec visitNamespaces (ns' : Name) : M Unit := do - if matchNamespace ns (ns' ++ id) danglingDot then - add ns ns' - else - match ns' with - | Name.str p .. => visitNamespaces p - | _ => return () - visitNamespaces ctx.currNamespace + let label? ← bestLabelForDecl? ctx ns id danglingDot + if let some bestLabel := label? then + addNamespaceCompletionItem bestLabel end IdCompletionUtils @@ -258,7 +258,7 @@ section DotCompletionUtils | _ => false if isConstOf then return true - let some e ← unfoldeDefinitionGuarded? e | return false + let some e ← unfoldDefinitionGuarded? e | return false isDefEqToAppOf e declName private def isDotCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool := @@ -356,34 +356,7 @@ private def idCompletionCore -- search for matches in the environment let env ← getEnv forEligibleDeclsWithCancellationM fun declName c => do - let bestMatch? ← (·.2) <$> StateT.run (s := none) do - let matchUsingNamespace (ns : Name) : StateT (Option Name) M Unit := do - let some label ← matchDecl? ns id danglingDot declName - | return - modify fun - | none => - some label - | some bestLabel => - -- for open namespaces `A` and `A.B` and a decl `A.B.c`, pick the decl `c` over `B.c` - if label.isSuffixOf bestLabel then - some label - else - some bestLabel - let rec visitNamespaces (ns : Name) : StateT (Option Name) M Unit := do - let Name.str p .. := ns - | return () - matchUsingNamespace ns - visitNamespaces p - -- use current namespace - visitNamespaces ctx.currNamespace - -- use open decls - for openDecl in ctx.openDecls do - let OpenDecl.simple ns exs := openDecl - | pure () - if exs.contains declName then - continue - matchUsingNamespace ns - matchUsingNamespace Name.anonymous + let bestMatch? ← bestLabelForDecl? ctx declName id danglingDot if let some bestLabel := bestMatch? then addUnresolvedCompletionItem bestLabel (.const declName) (← getCompletionKindForDecl c) RequestCancellation.check diff --git a/src/Lean/Server/Completion/CompletionUtils.lean b/src/Lean/Server/Completion/CompletionUtils.lean index 5eb6e6213a..ad8f06173e 100644 --- a/src/Lean/Server/Completion/CompletionUtils.lean +++ b/src/Lean/Server/Completion/CompletionUtils.lean @@ -66,7 +66,7 @@ where else shortenIn id contextNamespace.getPrefix -def unfoldeDefinitionGuarded? (e : Expr) : MetaM (Option Expr) := +def unfoldDefinitionGuarded? (e : Expr) : MetaM (Option Expr) := try Lean.Meta.unfoldDefinition? e catch _ => pure none partial def getDotCompletionTypeNames (type : Expr) : MetaM (Array Name) := @@ -78,7 +78,7 @@ where if isStructure (← getEnv) typeName then for parentName in (← getAllParentStructures typeName) do modify fun s => s.push parentName - let some type ← unfoldeDefinitionGuarded? type | return () + let some type ← unfoldDefinitionGuarded? type | return () visit type end Lean.Server.Completion diff --git a/tests/lean/interactive/compNamespace.lean.expected.out b/tests/lean/interactive/compNamespace.lean.expected.out index b7f37121bd..de9325d198 100644 --- a/tests/lean/interactive/compNamespace.lean.expected.out +++ b/tests/lean/interactive/compNamespace.lean.expected.out @@ -37,7 +37,7 @@ {"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 16, "character": 16}} {"items": - [{"label": "Foo.LongNamespaceExample", + [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace", "data":