refactor: add MonadLift CoreM CommandElabM

src/Lean/Elab/Attributes.lean

@@ -44,7 +44,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
+def elabAttr (attrInstance : Syntax) : CoreM Attribute := do
   /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
   let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
   let attr := attrInstance[1]
@@ -60,7 +60,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
   return { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs (attrInstances : Array Syntax) : CoreM (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
     try
@@ -70,7 +70,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs (stx : Syntax) : CoreM (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab

src/Lean/Elab/BuiltinCommand.lean

@@ -543,10 +543,6 @@ open Lean.Parser.Command.InternalSyntax in
     -- TODO: this really shouldn't have to re-elaborate section vars... they should come
     -- pre-elaborated
     let omittedVars ← runTermElabM fun vars => do
-      Term.synthesizeSyntheticMVarsNoPostponing
-      -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
-      -- So, we use `Core.resetMessageLog`.
-      Core.resetMessageLog
       -- resolve each omit to variable user name or type pattern
       let elaboratedOmits : Array (Sum Name Expr) ← omits.mapM fun
         | `(ident| $id:ident) => pure <| Sum.inl id.getId

src/Lean/Elab/Command.lean

@@ -17,18 +17,10 @@ public section
 
 namespace Lean.Elab.Command
 
-structure State where
-  env            : Environment
-  messages       : MessageLog := {}
+structure State extends Core.State where
   scopes         : List Scope := [{ header := "" }]
   usedQuotCtxts  : NameSet := {}
-  nextMacroScope : Nat := firstFrontendMacroScope + 1
   maxRecDepth    : Nat
-  ngen           : NameGenerator := {}
-  auxDeclNGen    : DeclNameGenerator := .ofPrefix .anonymous
-  infoState      : InfoState := {}
-  traceState     : TraceState := {}
-  snapshotTasks  : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
   deriving Nonempty
 
 structure Context where
@@ -74,6 +66,39 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
+private def liftCoreMDirect (x : CoreM α) : CommandElabM α := do
+  let ctx ← read
+  let s ← get
+  let scope := s.scopes.head!
+  let coreCtx := {
+    fileName           := ctx.fileName
+    fileMap            := ctx.fileMap
+    currRecDepth       := ctx.currRecDepth
+    maxRecDepth        := s.maxRecDepth
+    ref                := ctx.ref
+    currNamespace      := scope.currNamespace
+    openDecls          := scope.openDecls
+    initHeartbeats     := 0
+    quotContext        := ctx.quotContext?.getD s.env.mainModule
+    currMacroScope     := ctx.currMacroScope
+    options            := scope.opts
+    cancelTk?          := ctx.cancelTk?
+    suppressElabErrors := ctx.suppressElabErrors }
+  let (a, coreS) ← x.run coreCtx s.toState
+  modify ({ · with toState := coreS })
+  return a
+
+instance : MonadLift CoreM CommandElabM where
+  monadLift := private liftCoreMDirect
+
+instance : MonadStateOf State CommandElabM := inferInstance
+
+protected nonrec def CommandElabM.run (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception (α × State) := do
+  x.run ctx |>.run s
+
+protected def CommandElabM.run' (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception α := do
+  (·.1) <$> x.run ctx s
+
 /--
 Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
 want to catch and process them at the command level.
@@ -161,51 +186,17 @@ instance : MonadQuotation CommandElabM where
   withFreshMacroScope := Command.withFreshMacroScope
 
 private def runCore (x : CoreM α) : CommandElabM α := do
-  let s ← get
   let ctx ← read
   let heartbeats ← IO.getNumHeartbeats
-  let env := Kernel.resetDiag s.env
-  let scope := s.scopes.head!
-  let coreCtx : Core.Context := {
-    fileName           := ctx.fileName
-    fileMap            := ctx.fileMap
-    currRecDepth       := ctx.currRecDepth
-    maxRecDepth        := s.maxRecDepth
-    ref                := ctx.ref
-    currNamespace      := scope.currNamespace
-    openDecls          := scope.openDecls
-    initHeartbeats     := heartbeats
-    quotContext        := (← MonadQuotation.getMainModule)
-    currMacroScope     := ctx.currMacroScope
-    options            := scope.opts
-    cancelTk?          := ctx.cancelTk?
-    suppressElabErrors := ctx.suppressElabErrors }
-  let x : EIO _ _ := x.run coreCtx {
-    env
-    ngen := s.ngen
-    auxDeclNGen := s.auxDeclNGen
-    nextMacroScope := s.nextMacroScope
-    infoState.enabled := s.infoState.enabled
-    -- accumulate lazy assignments from all `CoreM` lifts
-    infoState.lazyAssignment := s.infoState.lazyAssignment
-    traceState := s.traceState
-    snapshotTasks := s.snapshotTasks
-  }
-  let (ea, coreS) ← liftM x
-  modify fun s => { s with
-    env                      := coreS.env
-    nextMacroScope           := coreS.nextMacroScope
-    ngen                     := coreS.ngen
-    auxDeclNGen              := coreS.auxDeclNGen
-    infoState.trees          := s.infoState.trees.append coreS.infoState.trees
-    -- we assume substitution of `assignment` has already happened, but for lazy assignments we only
-    -- do it at the very end
-    infoState.lazyAssignment := coreS.infoState.lazyAssignment
-    traceState.traces        := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    snapshotTasks            := coreS.snapshotTasks
-    messages                 := s.messages ++ coreS.messages
-  }
-  return ea
+  let env := Kernel.resetDiag (← getEnv)
+  liftM (m := CoreM) do
+    withReader ({ · with initHeartbeats := heartbeats }) do
+      modify ({ · with env })
+      let a ← x
+      modify fun s => { s with
+        traceState.traces        := s.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
+      }
+      return a
 
 def liftCoreM (x : CoreM α) : CommandElabM α := do
   MonadExcept.ofExcept (← runCore (observing x))
@@ -278,7 +269,7 @@ def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option
   setDeclNGen parentNGen
   let st ← get
   let st := { st with auxDeclNGen := childNGen }
-  return (act · |>.run ctx |>.run' st)
+  return (act · |>.run' ctx st)
 
 open Language in
 @[inherit_doc Core.wrapAsyncAsSnapshot]
@@ -412,10 +403,6 @@ def withMacroExpansion (beforeStx afterStx : Syntax) (x : CommandElabM α) : Com
   withInfoContext (mkInfo := pure <| .ofMacroExpansionInfo { stx := beforeStx, output := afterStx, lctx := .empty }) do
     withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
 
-instance : MonadMacroAdapter CommandElabM where
-  getNextMacroScope := return (← get).nextMacroScope
-  setNextMacroScope next := modify fun s => { s with nextMacroScope := next }
-
 instance : MonadRecDepth CommandElabM where
   withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
   getRecDepth      := return (← read).currRecDepth
@@ -581,7 +568,7 @@ def withInitQuotContext (hint? : Option UInt64) (act : CommandElabM Unit) : Comm
   finally
     modify ({ · with nextMacroScope })
 
-private partial def recordUsedSyntaxKinds (stx : Syntax) : CommandElabM Unit := do
+private partial def recordUsedSyntaxKinds (stx : Syntax) : CoreM Unit := do
   if let .node _ k .. := stx then
     -- do not record builtin parsers, they do not have to be imported
     if !(← Parser.builtinSyntaxNodeKindSetRef.get).contains k then
@@ -598,8 +585,13 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
   -- initialize quotation context using hash of input string
   let ss? := stx.getSubstring? (withLeading := false) (withTrailing := false)
   withInitQuotContext (ss?.map (hash ·.toString.trim)) do
-  -- Reset messages and info state, which are both per-command
-  modify fun st => { st with messages := {}, infoState := { enabled := st.infoState.enabled } }
+  -- Reset per-command state
+  modify fun st => { st with
+    messages := {}
+    infoState := { enabled := st.infoState.enabled }
+    traceState := {}
+    snapshotTasks := #[]
+  }
   try
     -- We should *not* factor out `elabCommand`'s `withLogging` to here since it would make its error
     -- recovery more coarse. In particular, if `c` in `set_option ... in $c` fails, the remaining
@@ -731,19 +723,19 @@ variable (n : Nat)
 -/
 def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
   let scope ← getScope
+  let msgs ← Core.getMessageLog
   liftTermElabM <|
     Term.withAutoBoundImplicit <|
       Term.elabBinders scope.varDecls fun xs => do
         -- We need to synthesize postponed terms because this is a checkpoint for the auto-bound implicit feature
         -- If we don't use this checkpoint here, then auto-bound implicits in the postponed terms will not be handled correctly.
         Term.synthesizeSyntheticMVarsNoPostponing
+        -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
+        Core.setMessageLog msgs
         let mut sectionFVars := {}
         for uid in scope.varUIds, x in xs do
           sectionFVars := sectionFVars.insert uid x
         withReader ({ · with sectionFVars := sectionFVars }) do
-          -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
-          -- So, we use `Core.resetMessageLog`.
-          Core.resetMessageLog
           let xs ← Term.addAutoBoundImplicits xs none
           if xs.all (·.isFVar) then
             Term.withoutAutoBoundImplicit <| elabFn xs
@@ -801,8 +793,8 @@ open Elab Command MonadRecDepth
 private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) : CoreM α := do
   let s : Core.State ← get
   let ctx : Core.Context ← read
-  let (a, commandState) ←
-    cmd.run {
+  let (a, commandState) ← do
+    let cmdCtx := {
       fileName := ctx.fileName
       fileMap := ctx.fileMap
       currRecDepth := ctx.currRecDepth
@@ -811,7 +803,8 @@ private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) :
       snap? := none
       cancelTk? := ctx.cancelTk?
       suppressElabErrors := ctx.suppressElabErrors
-    } |>.run {
+    }
+    cmd.run cmdCtx {
       env := s.env
       nextMacroScope := s.nextMacroScope
       maxRecDepth := ctx.maxRecDepth

src/Lean/Elab/DeclModifiers.lean

@@ -164,10 +164,8 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m (
 
 section Methods
 
-variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadFinally m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
-
 /-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `meta`, `noncomputable`, doc string)-/
-def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
+def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : CoreM Modifiers := do
   let docCommentStx := stx.raw[0]
   let attrsStx      := stx.raw[1]
   let visibilityStx := stx.raw[2]
@@ -209,7 +207,7 @@ Ensure the function has not already been declared, and apply the given visibilit
 If `private`, return the updated name using our internal encoding for private names.
 If `protected`, register `declName` as protected in the environment.
 -/
-def applyVisibility (modifiers : Modifiers) (declName : Name) : m Name := do
+def applyVisibility (modifiers : Modifiers) (declName : Name) : CoreM Name := do
   let mut declName := declName
   if !modifiers.visibility.isInferredPublic (← getEnv) then
     declName := mkPrivateName (← getEnv) declName
@@ -218,7 +216,7 @@ def applyVisibility (modifiers : Modifiers) (declName : Name) : m Name := do
     modifyEnv fun env => addProtected env declName
   pure declName
 
-def checkIfShadowingStructureField (declName : Name) : m Unit := do
+def checkIfShadowingStructureField (declName : Name) : CoreM Unit := do
   match declName with
   | Name.str pre .. =>
     if isStructure (← getEnv) pre then
@@ -228,7 +226,7 @@ def checkIfShadowingStructureField (declName : Name) : m Unit := do
           throwError "invalid declaration name `{.ofConstName declName}`, structure `{pre}` has field `{fieldName}`"
   | _ => pure ()
 
-def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : m (Name × Name) := do
+def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : CoreM (Name × Name) := do
   let mut shortName := shortName
   let mut currNamespace := currNamespace
   let view := extractMacroScopes shortName

src/Lean/Elab/DocString/Builtin.lean

@@ -696,7 +696,7 @@ where
       (cctx : Command.Context) (cmdState : Command.State) :
       DocM Command.State := do
     let (output, cmdState) ←
-      match (← liftM <| IO.FS.withIsolatedStreams <| EIO.toIO' <| (act.run cctx).run cmdState) with
+      match (← liftM <| IO.FS.withIsolatedStreams <| EIO.toIO' <| act.run cctx cmdState) with
       | (output, .error e) => Lean.logError e.toMessageData; pure (output, cmdState)
       | (output, .ok ((), cmdState)) => pure (output, cmdState)
 
@@ -706,7 +706,7 @@ where
       if let some tok := firstToken? stx then logInfoAt tok
       else logInfo
 
-    match (← liftM <| EIO.toIO' <| ((log output).run cctx).run cmdState) with
+    match (← liftM <| EIO.toIO' <| (log output).run cctx cmdState) with
     | .error _ => pure cmdState
     | .ok ((), cmdState) => pure cmdState
 

src/Lean/Elab/Frontend.lean

@@ -39,7 +39,7 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
     snap?        := none
     cancelTk?    := none
   }
-  match (← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState) with
+  match (← liftM <| EIO.toIO' <| x.run cmdCtx s.commandState) with
   | Except.error e      => throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"
   | Except.ok (a, sNew) => setCommandState sNew; return a
 

src/Lean/Elab/RecommendedSpelling.lean

@@ -19,7 +19,7 @@ open Lean.Parser.Command
 @[builtin_command_elab «recommended_spelling»] def elabRecommendedSpelling : CommandElab
   | `(«recommended_spelling»|$[$docs:docComment]? recommended_spelling $spelling:str for $«notation»:str in [$[$decls:ident],*]) => do
     let declNames ← liftTermElabM <| decls.mapM (fun decl => realizeGlobalConstNoOverloadWithInfo decl)
-    declNames.forM (recordExtraModUseFromDecl (isMeta := false))
+    declNames.forM (recordExtraModUseFromDecl (isMeta := false) ·)
     let recommendedSpelling : RecommendedSpelling := {
       «notation» := «notation».getString
       recommendedSpelling := spelling.getString

src/Lean/Elab/Term/TermElabM.lean

@@ -1457,10 +1457,6 @@ private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catch
   | []      => throwError "elaboration function for `{k}` has not been implemented{indentD stx}"
   | elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
 
-instance : MonadMacroAdapter TermElabM where
-  getNextMacroScope := return (← getThe Core.State).nextMacroScope
-  setNextMacroScope next := modifyThe Core.State fun s => { s with nextMacroScope := next }
-
 private def isExplicit (stx : Syntax) : Bool :=
   match stx with
   | `(@$_) => true

src/Lean/Elab/Util.lean

@@ -166,17 +166,7 @@ def expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Ex
       | ex                                => return (e.declName, Except.error ex)
   return none
 
-class MonadMacroAdapter (m : Type → Type) extends MonadQuotation m where
-  getNextMacroScope                  : m MacroScope
-  setNextMacroScope                  : MacroScope → m Unit
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadQuotation n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
-  getNextMacroScope := liftM (MonadMacroAdapter.getNextMacroScope : m _)
-  setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _)
-}
-
-def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : MacroM α) : m α := do
+def liftMacroM (x : MacroM α) : CoreM α := do
   let env  ← getEnv
   let opts ← getOptions
   let currNamespace ← getCurrNamespace
@@ -198,7 +188,7 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M
             quotContext    := ← MonadQuotation.getContext
             currRecDepth   := ← MonadRecDepth.getRecDepth
             maxRecDepth    := ← MonadRecDepth.getMaxRecDepth
-          } { macroScope := (← MonadMacroAdapter.getNextMacroScope) } with
+          } { macroScope := (← get).nextMacroScope } with
   | EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
   | EStateM.Result.error (Macro.Exception.error ref msg) _   =>
     if msg == maxRecDepthErrorMessage then
@@ -209,11 +199,11 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M
   | EStateM.Result.ok a s =>
     for n in s.expandedMacroDecls do
       recordExtraModUseFromDecl (isMeta := true) n
-    MonadMacroAdapter.setNextMacroScope s.macroScope
+    modify ({ · with nextMacroScope :=  s.macroScope })
     s.traceMsgs.reverse.forM fun (clsName, msg) => trace clsName fun _ => msg
     return a
 
-@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m]  [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : Macro) (stx : Syntax) : m Syntax :=
+@[inline] def adaptMacro (x : Macro) (stx : Syntax) : CoreM Syntax :=
   liftMacroM (x stx)
 
 partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do