From b2190da4687d461a90b0555c42908506aad823a6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Apr 2021 19:38:56 -0700
Subject: [PATCH] feat: add `Macro.resolveGlobalName` and
 `Macro.resolveNamespace?`

---
 src/Init/Prelude.lean                         | 14 +++++++++++---
 src/Lean/Elab/Util.lean                       |  3 +++
 tests/lean/macroResolveName.lean              | 11 +++++++++++
 tests/lean/macroResolveName.lean.expected.out |  2 ++
 4 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/macroResolveName.lean
 create mode 100644 tests/lean/macroResolveName.lean.expected.out

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e717105160..cfe7db524f 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2091,9 +2091,11 @@ instance : MonadQuotation MacroM where
   withFreshMacroScope   := Macro.withFreshMacroScope
 
 structure Methods where
-  expandMacro?     : Syntax → MacroM (Option Syntax)
-  getCurrNamespace : MacroM Name
-  hasDecl          : Name → MacroM Bool
+  expandMacro?      : Syntax → MacroM (Option Syntax)
+  getCurrNamespace  : MacroM Name
+  hasDecl           : Name → MacroM Bool
+  resolveNamespace? : Name → MacroM (Option Name)
+  resolveGlobalName : Name → MacroM (List (Prod Name (List String)))
   deriving Inhabited
 
 unsafe def mkMethodsImp (methods : Methods) : MethodsRef :=
@@ -2118,6 +2120,12 @@ def hasDecl (declName : Name) : MacroM Bool := do
 def getCurrNamespace : MacroM Name := do
   (← getMethods).getCurrNamespace
 
+def resolveNamespace? (n : Name) : MacroM (Option Name) := do
+  (← getMethods).resolveNamespace? n
+
+def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
+  (← getMethods).resolveGlobalName n
+
 def trace (clsName : Name) (msg : String) : MacroM Unit := do
   modify fun s => { s with traceMsgs := List.cons (Prod.mk clsName msg) s.traceMsgs }
 
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 3f172bca5f..963ee5759a 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -157,10 +157,13 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
 @[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : MacroM α) : m α := do
   let env  ← getEnv
   let currNamespace ← getCurrNamespace
+  let openDecls ← getOpenDecls
   let methods := Macro.mkMethods {
     expandMacro?     := expandMacro? env
     hasDecl          := fun declName => return env.contains declName
     getCurrNamespace := return currNamespace
+    resolveNamespace? := fun n => return ResolveName.resolveNamespace? env currNamespace openDecls n
+    resolveGlobalName := fun n => return ResolveName.resolveGlobalName env currNamespace openDecls n
   }
   match x { methods        := methods
             ref            := ← getRef
diff --git a/tests/lean/macroResolveName.lean b/tests/lean/macroResolveName.lean
new file mode 100644
index 0000000000..546b3c21e5
--- /dev/null
+++ b/tests/lean/macroResolveName.lean
@@ -0,0 +1,11 @@
+open Lean in
+macro "resolveN" x:ident : term =>
+  return quote (← Macro.resolveNamespace? x.getId)
+
+open Lean in #check resolveN Macro
+
+open Lean in
+macro "resolve" x:ident : term =>
+  return quote (← Macro.resolveGlobalName x.getId)
+
+open Nat in #check resolve succ
diff --git a/tests/lean/macroResolveName.lean.expected.out b/tests/lean/macroResolveName.lean.expected.out
new file mode 100644
index 0000000000..6eabb8be22
--- /dev/null
+++ b/tests/lean/macroResolveName.lean.expected.out
@@ -0,0 +1,2 @@
+some (Name.mkStr (Name.mkStr Name.anonymous "Lean") "Macro") : Option Name
+[(Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Nat") "succ", [])] : List (Lean.Name × List ?m)