From 47c2d335d46ccbd2b317a2e475f701a44b52abb8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Dec 2021 12:12:30 -0800
Subject: [PATCH] fix: completion for aliases

closes #863
---
 src/Lean/ResolveName.lean                    |  3 ++-
 src/Lean/Server/Completion.lean              | 28 +++++++++++++++-----
 tests/lean/interactive/863.lean              | 10 +++++++
 tests/lean/interactive/863.lean.expected.out | 26 ++++++++++++++++++
 4 files changed, 60 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/interactive/863.lean
 create mode 100644 tests/lean/interactive/863.lean.expected.out

diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index 4ebd91b465..62818f0046 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -11,7 +11,8 @@ import Lean.Exception
 namespace Lean
 /-!
   We use aliases to implement the `export <id> (<id>+)` command.
-  An `export A (x)` in the namespace `B` produces an alias `B.x ~> A.x`. -/
+  An `export A (x)` in the namespace `B` produces an alias `B.x ~> A.x`.
+-/
 
 abbrev AliasState := SMap Name (List Name)
 abbrev AliasEntry := Name × Name
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index f53f54233d..fd33db2bb3 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -92,7 +92,7 @@ private def runM (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) : IO (Op
     | (some _, s) =>
       return some { items := sortCompletionItems s.itemsMain ++ sortCompletionItems s.itemsOther, isIncomplete := true }
 
-private def matchAtomic (id: Name) (declName : Name) : Bool :=
+private def matchAtomic (id : Name) (declName : Name) : Bool :=
   match id, declName with
   | Name.str Name.anonymous s₁ _, Name.str Name.anonymous s₂ _ => s₁.isPrefixOf s₂
   | _, _ => false
@@ -172,6 +172,14 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (danglingDot : Bool
             if (← matchUsingNamespace ns) then
               return ()
         | _ => pure ()
+  -- Recall that aliases may not be atomic and include the namespace where they were created.
+  let matchAlias (ns : Name) (alias : Name) : Bool :=
+    ns.isPrefixOf alias && matchAtomic id (alias.replacePrefix ns Name.anonymous)
+  -- Auxiliary function for `alias`
+  let addAlias (alias : Name) (declNames : List Name) : M Unit := do
+    declNames.forM fun declName => do
+      unless (← isBlackListed declName) do
+        addCompletionItemForDecl alias declName expectedType?
   -- search explicitily open `ids`
   for openDecl in ctx.openDecls do
     match openDecl with
@@ -179,13 +187,21 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (danglingDot : Bool
       unless (← isBlackListed resolvedId) do
         if matchAtomic id openedId then
           addCompletionItemForDecl openedId resolvedId expectedType?
-    | _ => pure ()
+    | OpenDecl.simple ns except =>
+      getAliasState env |>.forM fun alias declNames => do
+        if matchAlias ns alias then
+          addAlias alias declNames
   -- search for aliases
   getAliasState env |>.forM fun alias declNames => do
-    if matchAtomic id alias then
-      declNames.forM fun declName => do
-        unless (← isBlackListed declName) do
-          addCompletionItemForDecl alias declName expectedType?
+    -- use current namespace
+    let rec searchAlias (ns : Name) : M Unit := do
+      if matchAlias ns alias then
+        addAlias alias declNames
+      else
+        match ns with
+        | Name.str p ..  => searchAlias p
+        | _ => return ()
+    searchAlias ctx.currNamespace
   -- TODO search macros
   -- TODO search namespaces
 
diff --git a/tests/lean/interactive/863.lean b/tests/lean/interactive/863.lean
new file mode 100644
index 0000000000..88a41eeb71
--- /dev/null
+++ b/tests/lean/interactive/863.lean
@@ -0,0 +1,10 @@
+import Lean
+
+open Lean in
+#check getRe
+          --^ textDocument/completion
+
+namespace Lean
+#check getRe
+          --^ textDocument/completion
+end Lean
diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out
new file mode 100644
index 0000000000..8b9ef52e53
--- /dev/null
+++ b/tests/lean/interactive/863.lean.expected.out
@@ -0,0 +1,26 @@
+{"textDocument": {"uri": "file://863.lean"},
+ "position": {"line": 3, "character": 12}}
+{"items":
+ [{"label": "getReducibilityStatus",
+   "detail":
+   "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},
+  {"label": "getReducibilityStatusImp",
+   "detail": "Environment → Name → ReducibilityStatus"},
+  {"label": "getRef", "detail": "[self : MonadRef m] → m Syntax"},
+  {"label": "getRegularInitFnNameFor?",
+   "detail": "Environment → Name → Option Name"},
+  {"label": "getRevAliases", "detail": "Environment → Name → List Name"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://863.lean"},
+ "position": {"line": 7, "character": 12}}
+{"items":
+ [{"label": "getReducibilityStatus",
+   "detail":
+   "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},
+  {"label": "getReducibilityStatusImp",
+   "detail": "Environment → Name → ReducibilityStatus"},
+  {"label": "getRef", "detail": "[self : MonadRef m] → m Syntax"},
+  {"label": "getRegularInitFnNameFor?",
+   "detail": "Environment → Name → Option Name"},
+  {"label": "getRevAliases", "detail": "Environment → Name → List Name"}],
+ "isIncomplete": true}