de-classify ExtraModUses

Author: Kha

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/Command.lean

@@ -446,10 +446,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

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/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

src/Lean/ExtraModUses.lean

@@ -49,9 +49,7 @@ public def copyExtraModUses (src dest : Environment) : Environment := Id.run do
       env := extraModUses.addEntry env entry
   env
 
-variable [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m]
-
-def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymous) : m Unit := do
+def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymous) : CoreM Unit := do
   let entry := { module := mod, isExported := (← getEnv).isExporting, isMeta }
   if !(extraModUses.getState (asyncMode := .local) (← getEnv)).contains entry then
     trace[extraModUses] "recording {if entry.isExported then "public" else "private"} \
@@ -63,7 +61,7 @@ def recordExtraModUseCore (mod : Name) (isMeta : Bool) (hint : Name := .anonymou
 Records an additional import dependency for the current module, using `Environment.isExporting` as
 the visibility level.
 -/
-public def recordExtraModUse (modName : Name) (isMeta : Bool) : m Unit := do
+public def recordExtraModUse (modName : Name) (isMeta : Bool) : CoreM Unit := do
   if modName != (← getEnv).mainModule then
     recordExtraModUseCore modName isMeta
 
@@ -72,7 +70,7 @@ Records the module of the given declaration as an additional import dependency f
 module, using `Environment.isExporting` as the visibility level. If the declaration itself is
 already `meta`, the module dependency is recorded as a non-`meta` dependency.
 -/
-public def recordExtraModUseFromDecl (declName : Name) (isMeta : Bool) : m Unit := do
+public def recordExtraModUseFromDecl (declName : Name) (isMeta : Bool) : CoreM Unit := do
   let env ← getEnv
   if let some mod := env.getModuleIdxFor? declName |>.bind (env.header.modules[·]?) then
     -- If the declaration itself is already `meta`, no need to mark the import.
@@ -91,7 +89,7 @@ public def isExtraRevModUse (env : Environment) (modIdx : ModuleIdx) : Bool :=
   !(isExtraRevModUseExt.getModuleEntries env modIdx |>.isEmpty)
 
 /-- Records this module to be preserved as an import by `shake`. -/
-public def recordExtraRevUseOfCurrentModule : m Unit := do
+public def recordExtraRevUseOfCurrentModule : CoreM Unit := do
   if isExtraRevModUseExt.getEntries (asyncMode := .local) (← getEnv) |>.isEmpty then
     modifyEnv (isExtraRevModUseExt.addEntry · ())