From 39d456cb09dc06ca3c1ae5dc7b38d33a80080ac3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Aug 2020 16:49:24 -0700 Subject: [PATCH] feat: add polymorphic `trace` and `logTrace` This commit also makes sure we always use `withContext` when logging. --- src/Lean/Elab/Command.lean | 14 ++++++-------- src/Lean/Elab/Definition.lean | 2 +- src/Lean/Elab/Log.lean | 20 ++++++++++++++++---- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/Tactic/Basic.lean | 4 ---- src/Lean/Elab/Term.lean | 17 ----------------- src/Lean/Meta/Basic.lean | 8 ++++++-- 7 files changed, 30 insertions(+), 37 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 344d28b332..934455971b 100644 --- a/src/Lean/Elab/Command.lean +++ b/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 diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean index e29f515b5a..b8c7406d9b 100644 --- a/src/Lean/Elab/Definition.lean +++ b/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; diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean index a8ad71437b..61db6c2790 100644 --- a/src/Lean/Elab/Log.lean +++ b/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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 7b6a073a8c..6b58e56701 100644 --- a/src/Lean/Elab/Match.lean +++ b/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 } diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 819f92075b..a6296d48fc 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/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; diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index dea9680162..b3efb7df2e 100644 --- a/src/Lean/Elab/Term.lean +++ b/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; diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 376dfb1ca0..b6eaa1c708 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 }