chore: add Macro.Methods

src/Init/Prelude.lean

@@ -2024,14 +2024,14 @@ def maxRecDepthErrorMessage : String :=
 namespace Macro
 
 /- References -/
-constant MacroEnvPointed : PointedType.{0}
+constant MethodsRefPointed : PointedType.{0}
 
-def MacroEnv : Type := MacroEnvPointed.type
-instance : Inhabited MacroEnv where
-  default := MacroEnvPointed.val
+def MethodsRef : Type := MethodsRefPointed.type
+instance : Inhabited MethodsRef where
+  default := MethodsRefPointed.val
 
 structure Context where
-  macroEnv       : MacroEnv
+  methods        : MethodsRef
   mainModule     : Name
   currMacroScope : MacroScope
   currRecDepth   : Nat := 0
@@ -2087,25 +2087,24 @@ instance : MonadQuotation MacroM where
   getMainModule     ctx := pure ctx.mainModule
   withFreshMacroScope   := Macro.withFreshMacroScope
 
-unsafe def mkMacroEnvImp (expandMacro? : Syntax → MacroM (Option Syntax)) : MacroEnv :=
-  unsafeCast expandMacro?
+structure Methods where
+  expandMacro? : Syntax → MacroM (Option Syntax)
+  deriving Inhabited
 
-@[implementedBy mkMacroEnvImp]
-constant mkMacroEnv (expandMacro? : Syntax → MacroM (Option Syntax)) : MacroEnv
+unsafe def mkMethodsImp (descr : Methods) : MethodsRef :=
+  unsafeCast descr
 
-def expandMacroNotAvailable? (stx : Syntax) : MacroM (Option Syntax) :=
-  throwErrorAt stx "expandMacro has not been set"
+@[implementedBy mkMethodsImp]
+constant mkMethods (descr : Methods) : MethodsRef
 
-def mkMacroEnvSimple : MacroEnv :=
-  mkMacroEnv expandMacroNotAvailable?
+unsafe def getMethodsImp : MacroM Methods :=
+  bind read fun ctx => pure (unsafeCast (ctx.methods))
 
-unsafe def expandMacro?Imp (stx : Syntax) : MacroM (Option Syntax) :=
-  bind read fun ctx =>
-  let f : Syntax → MacroM (Option Syntax) := unsafeCast (ctx.macroEnv)
-  f stx
+@[implementedBy getMethodsImp] constant getMethods : MacroM Methods
 
 /-- `expandMacro? stx` return `some stxNew` if `stx` is a macro, and `stxNew` is its expansion. -/
-@[implementedBy expandMacro?Imp] constant expandMacro? : Syntax → MacroM (Option Syntax)
+def expandMacro? (stx : Syntax) : MacroM (Option Syntax) := do
+  (← getMethods).expandMacro? stx
 
 end Macro
 

src/Lean/Elab/Util.lean

@@ -156,7 +156,7 @@ 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] (x : MacroM α) : m α := do
   let env  ← getEnv
-  match x { macroEnv       := Macro.mkMacroEnv (expandMacro? env),
+  match x { methods        := Macro.mkMethods { expandMacro? := expandMacro? env },
             ref            := ← getRef,
             currMacroScope := ← MonadMacroAdapter.getCurrMacroScope,
             mainModule     := env.mainModule,