feat: implement proper macro scope handling for TermElabM

src/Init/Lean/Elab/Quotation.lean

@@ -11,36 +11,6 @@ import Init.Lean.Parser -- TODO: remove after removing old elaborator
 
 namespace Lean
 
-abbrev MacroScope := Nat
-
-/-- A monad that supports syntax quotations. -/
-class MonadQuotation (m : Type → Type) :=
--- Get the fresh scope of the current macro invocation
-(getCurrMacroScope {} : m MacroScope)
--- Execute action in a new macro invocation context
-(withFreshMacroScope {α : Type} : m α → m α)
-export MonadQuotation
-
-def addMacroScope (n : Name) (scp : MacroScope) : Name :=
--- TODO: try harder to avoid clashes with other autogenerated names
-mkNameNum n scp
-
-/-- Simplistic MonadQuotation that does not guarantee globally fresh names. It is only safe
-    if the syntax quotations do not introduce bindings around antiquotations, and
-    if references to globals are prefixed with `_root_.`. -/
-abbrev Unhygienic := ReaderT (List Nat) $ StateM Nat
-namespace Unhygienic
-instance MonadQuotation : MonadQuotation Unhygienic := {
-  getCurrMacroScope := do
-    stack ← read;
-    pure $ stack.head!,
-  withFreshMacroScope := fun α x => do
-    fresh ← modifyGet (fun n => (n, n + 1));
-    adaptReader (fun stack => fresh::stack) x
-}
-protected def run {α : Type} (x : Unhygienic α) : α := run x [0] 1
-end Unhygienic
-
 /-- Reflect a runtime datum back to surface syntax (best-effort). -/
 class HasQuote (α : Type) :=
 (quote : α → Syntax)
@@ -76,12 +46,6 @@ instance Array.HasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
 namespace Elab
 namespace Term
 
-instance TermElabM.MonadQuotation : MonadQuotation TermElabM := {
--- FIXME: actually allocate macro scopes when we actually make use of them
-  getCurrMacroScope := pure 0,
-  withFreshMacroScope := fun α => id
-}
-
 private partial def quoteSyntax {m : Type → Type} [Monad m] [MonadQuotation m] (env : Environment) : Nat → Syntax → m Syntax
 | _, Syntax.ident info rawVal val preresolved => do
   -- TODO: pass scope information

src/Init/Lean/Elab/Term.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Lean.Util.Sorry
 import Init.Lean.Structure
 import Init.Lean.Meta
+import Init.Lean.Hygiene
 import Init.Lean.Elab.Log
 import Init.Lean.Elab.Alias
 import Init.Lean.Elab.ResolveName
@@ -23,6 +24,7 @@ structure Context extends Meta.Context :=
 (univNames     : List Name := [])
 (openDecls     : List OpenDecl := [])
 (macroStack    : List Syntax := [])
+(macroScopeStack : List MacroScope := [0])
 (mayPostpone   : Bool := true)
 
 inductive SyntheticMVarKind
@@ -39,6 +41,7 @@ structure State extends Meta.State :=
 (messages        : MessageLog := {})
 (instImplicitIdx : Nat := 1)
 (anonymousIdx    : Nat := 1)
+(nextMacroScope  : Nat := 1)
 
 instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
 
@@ -52,6 +55,15 @@ instance TermElabM.inhabited {α} : Inhabited (TermElabM α) :=
 
 instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩
 
+instance TermElabM.MonadQuotation : MonadQuotation TermElabM := {
+  getCurrMacroScope := do
+    ctx ← read;
+    pure ctx.macroScopeStack.head!,
+  withFreshMacroScope := fun α x => do
+    fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }));
+    adaptReader (fun (ctx : Context) => { ctx with macroScopeStack := fresh::ctx.macroScopeStack }) x
+}
+
 inductive LVal
 | fieldIdx  (i : Nat)
 | fieldName (name : String)
@@ -272,7 +284,7 @@ partial def expandCDotAux : Bool → Syntax → StateT (Array Syntax) TermElabM
 | _, n => pure n
 
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
-withNode stx $ fun node => do
+withFreshMacroScope $ withNode stx $ fun node => do
   trace! `Elab.step (toString stx);
   s ← get;
   let tables := termElabAttribute.ext.getState s.env;

src/Init/Lean/Hygiene.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+prelude
+import Init.Control
+import Init.Lean.Syntax
+
+namespace Lean
+
+abbrev MacroScope := Nat
+
+/-- A monad that supports syntax quotations. -/
+class MonadQuotation (m : Type → Type) :=
+-- Get the fresh scope of the current macro invocation
+(getCurrMacroScope {} : m MacroScope)
+-- Execute action in a new macro invocation context
+(withFreshMacroScope {α : Type} : m α → m α)
+export MonadQuotation
+
+def addMacroScope (n : Name) (scp : MacroScope) : Name :=
+-- TODO: try harder to avoid clashes with other autogenerated names
+mkNameNum n scp
+
+/-- Simplistic MonadQuotation that does not guarantee globally fresh names. It is only safe
+    if the syntax quotations do not introduce bindings around antiquotations, and
+    if references to globals are prefixed with `_root_.`. -/
+abbrev Unhygienic := ReaderT (List Nat) $ StateM Nat
+namespace Unhygienic
+instance MonadQuotation : MonadQuotation Unhygienic := {
+  getCurrMacroScope := do
+    stack ← read;
+    pure stack.head!,
+  withFreshMacroScope := fun α x => do
+    fresh ← modifyGet (fun n => (n, n + 1));
+    adaptReader (fun stack => fresh::stack) x
+}
+protected def run {α : Type} (x : Unhygienic α) : α := run x [0] 1
+end Unhygienic
+
+end Lean