feat: auto-complete declaration names in arbitrary namespaces

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

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

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}

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}