From e37fbfd2c2313ef534b68580e107ee9fa63a4605 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Thu, 15 May 2025 11:30:28 +0200 Subject: [PATCH 1/5] fix namespace completion --- .../Completion/CompletionCollectors.lean | 83 ++++++++----------- .../namespaceCompletion.expected.out | 13 +++ .../lean/interactive/namespaceCompletion.lean | 12 +++ 3 files changed, 59 insertions(+), 49 deletions(-) create mode 100644 tests/lean/interactive/namespaceCompletion.expected.out create mode 100644 tests/lean/interactive/namespaceCompletion.lean diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 806c1b924de9..16eda53dd16e 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -221,31 +221,43 @@ section IdCompletionUtils 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 @@ -356,34 +368,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/tests/lean/interactive/namespaceCompletion.expected.out b/tests/lean/interactive/namespaceCompletion.expected.out new file mode 100644 index 000000000000..798dbf7096dd --- /dev/null +++ b/tests/lean/interactive/namespaceCompletion.expected.out @@ -0,0 +1,13 @@ +{"textDocument": {"uri": "file:///lean\\interactive\\namespaceCompletion.lean"}, + "position": {"line": 10, "character": 14}} +{"items": + [{"label": "Inner", + "kind": 9, + "detail": "namespace", + "data": + {"params": + {"textDocument": + {"uri": "file:///lean\\interactive\\namespaceCompletion.lean"}, + "position": {"line": 10, "character": 14}}, + "cPos": 0}}], + "isIncomplete": false} diff --git a/tests/lean/interactive/namespaceCompletion.lean b/tests/lean/interactive/namespaceCompletion.lean new file mode 100644 index 000000000000..80be207e3f63 --- /dev/null +++ b/tests/lean/interactive/namespaceCompletion.lean @@ -0,0 +1,12 @@ +prelude + +namespace Outer + +namespace Inner + +end Inner + +end Outer + +#print Outer.I + --^ textDocument/completion From 907acd56ea380f85d06434752f5f57ae18d5d104 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Thu, 15 May 2025 11:34:43 +0200 Subject: [PATCH 2/5] retrigger ci From 1af9f402a8037361ab498e68931a4bc2683ed89a Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Thu, 15 May 2025 12:16:20 +0200 Subject: [PATCH 3/5] fix tests --- tests/lean/interactive/compNamespace.lean.expected.out | 2 +- ...etion.expected.out => namespaceCompletion.lean.expected.out} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename tests/lean/interactive/{namespaceCompletion.expected.out => namespaceCompletion.lean.expected.out} (100%) diff --git a/tests/lean/interactive/compNamespace.lean.expected.out b/tests/lean/interactive/compNamespace.lean.expected.out index b7f37121bd4b..de9325d19806 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": diff --git a/tests/lean/interactive/namespaceCompletion.expected.out b/tests/lean/interactive/namespaceCompletion.lean.expected.out similarity index 100% rename from tests/lean/interactive/namespaceCompletion.expected.out rename to tests/lean/interactive/namespaceCompletion.lean.expected.out From 01d67526a51d0f1ee44e502bca02d490eec2c0d7 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Thu, 15 May 2025 12:51:01 +0200 Subject: [PATCH 4/5] remove unnecessary tests --- tests/lean/interactive/namespaceCompletion.lean | 12 ------------ .../namespaceCompletion.lean.expected.out | 13 ------------- 2 files changed, 25 deletions(-) delete mode 100644 tests/lean/interactive/namespaceCompletion.lean delete mode 100644 tests/lean/interactive/namespaceCompletion.lean.expected.out diff --git a/tests/lean/interactive/namespaceCompletion.lean b/tests/lean/interactive/namespaceCompletion.lean deleted file mode 100644 index 80be207e3f63..000000000000 --- a/tests/lean/interactive/namespaceCompletion.lean +++ /dev/null @@ -1,12 +0,0 @@ -prelude - -namespace Outer - -namespace Inner - -end Inner - -end Outer - -#print Outer.I - --^ textDocument/completion diff --git a/tests/lean/interactive/namespaceCompletion.lean.expected.out b/tests/lean/interactive/namespaceCompletion.lean.expected.out deleted file mode 100644 index 798dbf7096dd..000000000000 --- a/tests/lean/interactive/namespaceCompletion.lean.expected.out +++ /dev/null @@ -1,13 +0,0 @@ -{"textDocument": {"uri": "file:///lean\\interactive\\namespaceCompletion.lean"}, - "position": {"line": 10, "character": 14}} -{"items": - [{"label": "Inner", - "kind": 9, - "detail": "namespace", - "data": - {"params": - {"textDocument": - {"uri": "file:///lean\\interactive\\namespaceCompletion.lean"}, - "position": {"line": 10, "character": 14}}, - "cPos": 0}}], - "isIncomplete": false} From 2460fe05a6b44dd61f0a54b2b70a001a0ac23dd3 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Mon, 19 May 2025 20:42:48 +0200 Subject: [PATCH 5/5] remove dead code --- .../Server/Completion/CompletionCollectors.lean | 14 +------------- src/Lean/Server/Completion/CompletionUtils.lean | 4 ++-- 2 files changed, 3 insertions(+), 15 deletions(-) diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 16eda53dd16e..628801e9b497 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -209,18 +209,6 @@ 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 @@ -270,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 := diff --git a/src/Lean/Server/Completion/CompletionUtils.lean b/src/Lean/Server/Completion/CompletionUtils.lean index 5eb6e6213a23..ad8f06173ef6 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