feat: add Macro.resolveGlobalName and Macro.resolveNamespace?

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 }
 

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

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

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)