feat: add polymorphic trace and logTrace

This commit also makes sure we always use `withContext` when logging.

src/Lean/Elab/Command.lean

@@ -115,20 +115,18 @@ instance : MonadIO CommandElabM :=
 
 def getScope : CommandElabM Scope := do s ← get; pure s.scopes.head!
 
+instance : MonadLCtx CommandElabM :=
+{ getLCtx := pure {} }
+
+instance : MonadMCtx CommandElabM :=
+{ getMCtx := pure {} }
+
 instance CommandElabM.monadLog : MonadLog CommandElabM :=
 { getRef      := getRef,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
-  addContext  := Command.addContext',
   logMessage  := fun msg => modify $ fun s => { s with messages := s.messages.add msg } }
 
-def logTrace (cls : Name) (msg : MessageData) : CommandElabM Unit := do
-msg ← Command.addContext' $ MessageData.tagged cls msg;
-logInfo msg
-
-@[inline] def trace (cls : Name) (msg : Unit → MessageData) : CommandElabM Unit := do
-opts ← getOptions;
-when (checkTraceOption opts cls) $ logTrace cls (msg ())
 
 protected def getCurrMacroScope : CommandElabM Nat  := do ctx ← read; pure ctx.currMacroScope
 protected def getMainModule     : CommandElabM Name := do env ← getEnv; pure env.mainModule

src/Lean/Elab/Definition.lean

@@ -85,7 +85,7 @@ else withUsedWhen vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun vars =>
     pure (type, val)
   };
   let (type, val) := shareCommonTypeVal.run;
-  Term.trace `Elab.definition.body fun _ => declName ++ " : " ++ type ++ " :=" ++ Format.line ++ val;
+  trace `Elab.definition.body fun _ => declName ++ " : " ++ type ++ " :=" ++ Format.line ++ val;
   let usedParams : CollectLevelParams.State := {};
   let usedParams  := collectLevelParams usedParams type;
   let usedParams  := collectLevelParams usedParams val;

src/Lean/Elab/Log.lean

@@ -13,20 +13,18 @@ class MonadLog (m : Type → Type) :=
 (getRef       : m Syntax)
 (getFileMap   : m FileMap)
 (getFileName  : m String)
-(addContext   : MessageData → m MessageData)
 (logMessage   : Message → m Unit)
 
 instance monadLogTrans (m n) [MonadLog m] [MonadLift m n] : MonadLog n :=
 { getRef      := liftM (MonadLog.getRef : m _),
   getFileMap  := liftM (MonadLog.getFileMap : m _),
   getFileName := liftM (MonadLog.getFileName : m _),
-  addContext  := fun msgData => liftM (MonadLog.addContext msgData : m _),
   logMessage  := fun msg => liftM (MonadLog.logMessage msg : m _ ) }
 
 export MonadLog (getFileMap getFileName logMessage)
 open MonadLog (getRef)
 
-variables {m : Type → Type} [Monad m] [MonadLog m]
+variables {m : Type → Type} [Monad m] [MonadLog m] [MonadEnv m] [MonadOptions m] [MonadLCtx m] [MonadMCtx m]
 
 def getRefPos : m String.Pos := do
 ref ← getRef;
@@ -43,7 +41,11 @@ let ref  := replaceRef ref currRef;
 let pos  := ref.getPos.getD 0;
 fileMap  ← getFileMap;
 fileName ← getFileName;
-msgData  ← MonadLog.addContext msgData;
+env ← getEnv;
+mctx ← getMCtx;
+lctx ← getLCtx;
+opts ← getOptions;
+let msgData := MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData;
 logMessage { fileName := fileName, pos := fileMap.toPosition pos, data := msgData, severity := severity }
 
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
@@ -76,5 +78,15 @@ match ex with
     name ← liftIO $ id.getName;
     logError ("internal exception: " ++ name)
 
+def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
+logInfo (MessageData.tagged cls msgData)
+
+@[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit := do
+opts ← getOptions;
+when (checkTraceOption opts cls) $ logTrace cls (msg ())
+
+def logDbgTrace (msg : MessageData) : m Unit := do
+trace `Elab.debug fun _ => msg
+
 end Elab
 end Lean

src/Lean/Elab/Match.lean

@@ -316,7 +316,7 @@ private partial def collect : Syntax → M Syntax
 
 def main (alt : MatchAltView) : M MatchAltView := do
 patterns ← alt.patterns.mapM fun p => do {
-  liftM $ trace `Elab.match fun _ => "collecting variables at pattern: " ++ p;
+  trace `Elab.match fun _ => "collecting variables at pattern: " ++ p;
   collect p
 };
 pure { alt with patterns := patterns }

src/Lean/Elab/Tactic/Basic.lean

@@ -112,10 +112,6 @@ unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
 mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic"
 @[init mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic := arbitrary _
 
-def logTrace (cls : Name) (msg : MessageData) : TacticM Unit := liftTermElabM $ Term.logTrace cls msg
-@[inline] def trace (cls : Name) (msg : Unit → MessageData) : TacticM Unit := liftTermElabM $ Term.trace cls msg
-@[inline] def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TacticM Unit := liftTermElabM $ Term.traceAtCmdPos cls msg
-
 private def evalTacticUsing (s : SavedState) (stx : Syntax) : List Tactic → TacticM Unit
 | []                => do
   let refFmt := stx.prettyPrint;

src/Lean/Elab/Term.lean

@@ -191,7 +191,6 @@ instance monadLog : MonadLog TermElabM :=
 { getRef      := getRef,
   getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
-  addContext  := addContext',
   logMessage  := fun msg => modify $ fun s => { s with messages := s.messages.add msg } }
 
 protected def getCurrMacroScope : TermElabM MacroScope := do ctx ← read; pure ctx.currMacroScope
@@ -235,22 +234,6 @@ def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modifyTh
 def withDeclName {α} (name : Name) (x : TermElabM α) : TermElabM α :=
 adaptReader (fun (ctx : Context) => { ctx with declName? := name }) x
 
-def logTrace (cls : Name) (msg : MessageData) : TermElabM Unit := do
-env  ← getEnv;
-mctx ← getMCtx;
-lctx ← getLCtx;
-opts ← getOptions;
-logInfo $
-  MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } $
-    MessageData.tagged cls msg
-
-@[inline] def trace (cls : Name) (msg : Unit → MessageData) : TermElabM Unit := do
-opts ← getOptions;
-when (checkTraceOption opts cls) $ logTrace cls (msg ())
-
-def logDbgTrace (msg : MessageData) : TermElabM Unit := do
-trace `Elab.debug $ fun _ => msg
-
 /-- For testing `TermElabM` methods. The #eval command will sign the error. -/
 def throwErrorIfErrors : TermElabM Unit := do
 s ← get;

src/Lean/Meta/Basic.lean

@@ -122,6 +122,12 @@ instance : MonadError MetaM :=
   withRef    := fun α => withRef,
   addContext := fun ref msg => do msg ← Meta.addTraceContext msg; pure (ref, msg) }
 
+instance : MonadLCtx MetaM :=
+{ getLCtx := do ctx ← read; pure ctx.lctx }
+
+instance : MonadMCtx MetaM :=
+{ getMCtx := do s ← get; pure s.mctx }
+
 instance : SimpleMonadTracerAdapter MetaM :=
 { getOptions       := getOptions,
   getTraceState    := getTraceState,
@@ -164,10 +170,8 @@ section Methods
 variables {m : Type → Type} [MonadLiftT MetaM m]
 variables {n : Type → Type} [MonadControlT MetaM n] [Monad n]
 
-def getLCtx : m LocalContext := liftMetaM do ctx ← read; pure ctx.lctx
 def getLocalInstances : m LocalInstances := liftMetaM do ctx ← read; pure ctx.localInstances
 def getConfig : m Config := liftMetaM do ctx ← read; pure ctx.config
-def getMCtx : m MetavarContext := liftMetaM do s ← get; pure s.mctx
 def setMCtx (mctx : MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := mctx }
 @[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : m Unit :=
 liftMetaM $ modify fun s => { s with mctx := f s.mctx }