From e5c35d3a4e657e35d40a70df36d9c3f52e227a57 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Aug 2020 18:05:42 -0700 Subject: [PATCH] feat: add `AddMessageDataContext` --- src/Lean/CoreM.lean | 9 +++------ src/Lean/Elab/Command.lean | 9 +++------ src/Lean/Elab/Log.lean | 8 ++++---- src/Lean/Elab/Term.lean | 2 +- src/Lean/Environment.lean | 11 +++++++++++ src/Lean/Message.lean | 21 +++++++++++++++++++++ src/Lean/Meta/Basic.lean | 5 ++++- src/Lean/Meta/EqnCompiler/Match.lean | 2 +- src/Lean/MonadEnv.lean | 10 ---------- src/Lean/Util/Trace.lean | 11 ++--------- 10 files changed, 50 insertions(+), 38 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 9f1b34b07a..3736d4aeb6 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -63,16 +63,13 @@ liftM $ (adaptExcept (fun (err : IO.Error) => Exception.error ref (toString err) instance : MonadIO CoreM := { liftIO := @liftIOCore } -instance : MonadLCtx CoreM := -{ getLCtx := pure {} } - -instance : MonadMCtx CoreM := -{ getMCtx := pure {} } - instance : MonadTrace CoreM := { getTraceState := do s ← get; pure s.traceState, modifyTraceState := fun f => modify $ fun s => { s with traceState := f s.traceState } } +instance : AddMessageDataContext CoreM := +{ addMessageDataContext := addMessageDataContextPartial } + @[inline] def CoreM.run {α} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) := (x.run ctx).run s diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 934455971b..944d997a0c 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -113,14 +113,11 @@ liftEIO $ adaptExcept (fun (ex : IO.Error) => Exception.error ctx.ref ex.toStrin instance : MonadIO CommandElabM := { liftIO := fun α => liftIO } +instance : AddMessageDataContext CommandElabM := +{ addMessageDataContext := addMessageDataContextPartial } + 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, diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean index 292916c7fc..24c40ef30e 100644 --- a/src/Lean/Elab/Log.lean +++ b/src/Lean/Elab/Log.lean @@ -24,7 +24,7 @@ instance monadLogTrans (m n) [MonadLog m] [MonadLift m n] : MonadLog n := export MonadLog (getFileMap getFileName logMessage) open MonadLog (getRef) -variables {m : Type → Type} [Monad m] [MonadLog m] [MonadEnv m] [MonadOptions m] [MonadLCtx m] [MonadMCtx m] +variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageDataContext m] def getRefPos : m String.Pos := do ref ← getRef; @@ -41,7 +41,7 @@ let ref := replaceRef ref currRef; let pos := ref.getPos.getD 0; fileMap ← getFileMap; fileName ← getFileName; -msgData ← addWithContext msgData; +msgData ← addMessageDataContext msgData; logMessage { fileName := fileName, pos := fileMap.toPosition pos, data := msgData, severity := severity } def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit := @@ -77,11 +77,11 @@ match ex with 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 +@[inline] def trace [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do opts ← getOptions; when (checkTraceOption opts cls) $ logTrace cls (msg ()) -def logDbgTrace (msg : MessageData) : m Unit := do +def logDbgTrace [MonadOptions m] (msg : MessageData) : m Unit := do trace `Elab.debug fun _ => msg end Elab diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 84cb110a61..c29714bcca 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -180,7 +180,7 @@ instance MonadError : MonadError TermElabM := ctx ← read; let ref := getBetterRef ref ctx.macroStack; let msg := if ctx.macroStackAtErr then addMacroStack msg ctx.macroStack else msg; - msg ← addWithContext msg; + msg ← addMessageDataContext msg; pure (ref, msg) } instance monadLog : MonadLog TermElabM := diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index db335ecdb1..bece88fa63 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -683,4 +683,15 @@ constant isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool : constant whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Expr := arbitrary _ end Kernel + +class MonadEnv (m : Type → Type) := +(getEnv : m Environment) +(modifyEnv : (Environment → Environment) → m Unit) + +export MonadEnv (getEnv modifyEnv) + +instance monadEnvFromLift (m n) [MonadEnv m] [MonadLift m n] : MonadEnv n := +{ getEnv := liftM (getEnv : m Environment), + modifyEnv := fun f => liftM (modifyEnv f : m Unit) } + end Lean diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 77919f77d9..0722dcb13d 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -219,4 +219,25 @@ match e with | other msg => "(kernel) " ++ msg end KernelException + +class AddMessageDataContext (m : Type → Type) := +(addMessageDataContext : MessageData → m MessageData) + +export AddMessageDataContext (addMessageDataContext) + +instance addMessageDataContextTrans (m n) [AddMessageDataContext m] [MonadLift m n] : AddMessageDataContext n := +{ addMessageDataContext := fun msg => liftM (addMessageDataContext msg : m _) } + +def addMessageDataContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do +env ← getEnv; +opts ← getOptions; +pure $ MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData + +def addMessageDataContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do +env ← getEnv; +mctx ← getMCtx; +lctx ← getLCtx; +opts ← getOptions; +pure $ MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData + end Lean diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index dc3220b5c8..dcc176da20 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -116,10 +116,13 @@ instance : MonadLCtx MetaM := instance : MonadMCtx MetaM := { getMCtx := do s ← get; pure s.mctx } +instance : AddMessageDataContext MetaM := +{ addMessageDataContext := addMessageDataContextFull } + instance : MonadError MetaM := { getRef := getRef, withRef := fun α => withRef, - addContext := fun ref msg => do msg ← addWithContext msg; pure (ref, msg) } + addContext := fun ref msg => do msg ← addMessageDataContext msg; pure (ref, msg) } @[inline] def MetaM.run {α} (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) := (x.run ctx).run s diff --git a/src/Lean/Meta/EqnCompiler/Match.lean b/src/Lean/Meta/EqnCompiler/Match.lean index ad9b63bacd..a05a4292cf 100644 --- a/src/Lean/Meta/EqnCompiler/Match.lean +++ b/src/Lean/Meta/EqnCompiler/Match.lean @@ -91,7 +91,7 @@ partial def toMessageData (alt : Alt) : MetaM MessageData := do withExistingLocalDecls alt.fvarDecls do let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")"; let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs; - addWithContext msg + addMessageDataContext msg def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt := { alt with diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 09f4378dde..c660437bf4 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -8,16 +8,6 @@ import Lean.Exception namespace Lean -class MonadEnv (m : Type → Type) := -(getEnv : m Environment) -(modifyEnv : (Environment → Environment) → m Unit) - -export MonadEnv (getEnv modifyEnv) - -instance monadEnvFromLift (m n) [MonadEnv m] [MonadLift m n] : MonadEnv n := -{ getEnv := liftM (getEnv : m Environment), - modifyEnv := fun f => liftM (modifyEnv f : m Unit) } - section Methods variables {m : Type → Type} [MonadEnv m] diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index fd781f933f..fcd756d4ed 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -9,13 +9,6 @@ universe u namespace Lean -def addWithContext {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do -env ← getEnv; -mctx ← getMCtx; -lctx ← getLCtx; -opts ← getOptions; -pure $ MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData - open Std (PersistentArray) structure TraceState := @@ -104,10 +97,10 @@ modifyTraces $ fun _ => {}; pure oldTraces section -variables [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] +variables [AddMessageDataContext m] [MonadOptions m] def addTrace (cls : Name) (msg : MessageData) : m Unit := do -msg ← addWithContext msg; +msg ← addMessageDataContext msg; modifyTraces $ fun traces => traces.push (MessageData.tagged cls msg) @[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit :=