feat: simplify MacroM

src/Init/Lean/Elab/Command.lean

@@ -192,9 +192,7 @@ adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after
 
 instance : MonadMacroAdapter CommandElabM :=
 { getEnv                 := getEnv,
-  getNameGenerator       := do s ← get; pure s.ngen,
   getCurrMacroScope      := getCurrMacroScope,
-  setNameGenerator       := fun ngen => modify $ fun s => { ngen := ngen, .. s },
   throwError             := @throwError,
   throwUnsupportedSyntax := @throwUnsupportedSyntax}
 

src/Init/Lean/Elab/Tactic/Basic.lean

@@ -176,9 +176,7 @@ adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after
 
 instance : MonadMacroAdapter TacticM :=
 { getEnv                 := getEnv,
-  getNameGenerator       := do s ← get; pure s.ngen,
   getCurrMacroScope      := getCurrMacroScope,
-  setNameGenerator       := fun ngen => modify $ fun s => { ngen := ngen, .. s },
   throwError             := @throwError,
   throwUnsupportedSyntax := @throwUnsupportedSyntax }
 

src/Init/Lean/Elab/Term.lean

@@ -465,9 +465,7 @@ private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Exp
 
 instance : MonadMacroAdapter TermElabM :=
 { getEnv                 := getEnv,
-  getNameGenerator       := do s ← get; pure s.ngen,
   getCurrMacroScope      := getCurrMacroScope,
-  setNameGenerator       := fun ngen => modify $ fun s => { ngen := ngen, .. s },
   throwError             := @throwError,
   throwUnsupportedSyntax := @throwUnsupportedSyntax}
 

src/Init/Lean/Elab/Util.lean

@@ -187,19 +187,16 @@ fun stx =>
 class MonadMacroAdapter (m : Type → Type) :=
 (getEnv {}                            : m Environment)
 (getCurrMacroScope {}                 : m MacroScope)
-(getNameGenerator {}                  : m NameGenerator)
-(setNameGenerator {}                  : NameGenerator → m Unit)
 (throwError {} {α : Type}             : Syntax → MessageData → m α)
 (throwUnsupportedSyntax {} {α : Type} : m α)
 
 @[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] (x : Macro) (stx : Syntax) : m Syntax := do
 scp  ← MonadMacroAdapter.getCurrMacroScope;
 env  ← MonadMacroAdapter.getEnv;
-ngen ← MonadMacroAdapter.getNameGenerator;
-match x stx { currMacroScope := scp, mainModule := env.mainModule } { ngen := ngen } with
-| EStateM.Result.error Macro.Exception.unsupportedSyntax newS => MonadMacroAdapter.throwUnsupportedSyntax
-| EStateM.Result.ok stx newS                                  => do MonadMacroAdapter.setNameGenerator newS.ngen; pure stx
-| EStateM.Result.error (Macro.Exception.error msg) newS       => do MonadMacroAdapter.setNameGenerator newS.ngen; MonadMacroAdapter.throwError stx msg
+match x stx { currMacroScope := scp, mainModule := env.mainModule } with
+| Except.error Macro.Exception.unsupportedSyntax => MonadMacroAdapter.throwUnsupportedSyntax
+| Except.error (Macro.Exception.error msg)       => MonadMacroAdapter.throwError stx msg
+| Except.ok stx                                  => pure stx
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab;

src/Init/LeanInit.lean

@@ -9,7 +9,7 @@ import Init.Data.Array.Basic
 import Init.Data.UInt
 import Init.Data.Hashable
 import Init.Control.Reader
-import Init.Control.EState
+import Init.Control.Except
 
 namespace Lean
 /-
@@ -321,23 +321,17 @@ structure Context :=
 (mainModule     : Name)
 (currMacroScope : MacroScope)
 
-structure State :=
-(ngen : NameGenerator)
-
 inductive Exception
 | error             : String → Exception
 | unsupportedSyntax : Exception
 
 end Macro
 
-abbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception Macro.State)
+abbrev MacroM := ReaderT Macro.Context (ExceptT Macro.Exception Id)
 
-def Macro.mkFreshName (namePrefix : Name) : MacroM Name := do
+def Macro.addMacroScope (n : Name) : MacroM Name := do
 ctx ← read;
-s   ← get;
-let id := namePrefix ++ ctx.mainModule ++ s.ngen.curr;
-modify $ fun s => { ngen := s.ngen.next, .. s };
-pure id
+pure $ Lean.addMacroScope ctx.mainModule n ctx.currMacroScope
 
 instance MacroM.monadQuotation : MonadQuotation MacroM :=
 { getCurrMacroScope   := fun ctx => pure ctx.currMacroScope,