From e681bd71d9d761976fdc834b98b83f19ddc32fa5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jan 2020 12:22:33 -0800
Subject: [PATCH] feat: simplify `MacroM`

---
 src/Init/Lean/Elab/Command.lean      |  2 --
 src/Init/Lean/Elab/Tactic/Basic.lean |  2 --
 src/Init/Lean/Elab/Term.lean         |  2 --
 src/Init/Lean/Elab/Util.lean         | 11 ++++-------
 src/Init/LeanInit.lean               | 14 ++++----------
 5 files changed, 8 insertions(+), 23 deletions(-)

diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 7813ba19ad..96ec4ed2ab 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/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}
 
diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index c63967eb98..789609c747 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/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 }
 
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 8e86af5040..8dacd0b3a8 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/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}
 
diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index 47559b0f76..66e669f80b 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/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;
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 67ede337b7..1c02b45ab0 100644
--- a/src/Init/LeanInit.lean
+++ b/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,