From 1352619ee43075cb783ec002ed9d67cb359892b2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Dec 2019 09:05:15 -0800 Subject: [PATCH] refactor: `MonadTracer` and helper functions This commit adds - `addContext : MessageData -> m MessageData` method. We need it to make sure we wrap the message with the current context. Before this commit I had to redefine `trace` for `MetaM`, `SynthM`, and `TermElabM`. - polymorphic `traceM` method. --- src/Init/Lean/Elab/Term.lean | 16 +++------- src/Init/Lean/Meta/Basic.lean | 12 +++---- src/Init/Lean/Meta/Check.lean | 2 +- src/Init/Lean/Meta/ExprDefEq.lean | 20 ++++++------ src/Init/Lean/Meta/LevelDefEq.lean | 10 +++--- src/Init/Lean/Meta/SynthInstance.lean | 45 +++++++++++---------------- src/Init/Lean/Util/Trace.lean | 17 +++++++--- tests/lean/run/trace.lean | 1 + 8 files changed, 58 insertions(+), 65 deletions(-) diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 0e57c79c16..ccfb849146 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -88,26 +88,20 @@ fun ctx s => match x ctx.toContext s.toState with def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState +def addContext (msg : MessageData) : TermElabM MessageData := +do ctx ← read; + s ← get; + pure $ MessageData.context s.env s.mctx ctx.lctx msg instance tracer : SimpleMonadTracerAdapter TermElabM := { getOptions := getOptions, getTraceState := getTraceState, + addContext := addContext, modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } } def dbgTrace {α} [HasToString α] (a : α) : TermElabM Unit := _root_.dbgTrace (toString a) $ fun _ => pure () -private def addTrace (cls : Name) (msg : MessageData) : TermElabM Unit := -do ctx ← read; - s ← get; - MonadTracerAdapter.addTrace cls (MessageData.context s.env s.mctx ctx.lctx msg) - -@[inline] def trace (cls : Name) (msg : Unit → MessageData) : TermElabM Unit := -whenM (MonadTracerAdapter.isTracingEnabledFor cls) $ addTrace cls (msg ()) - -@[inline] def traceM (cls : Name) (mkMsg : TermElabM MessageData) : TermElabM Unit := -whenM (MonadTracerAdapter.isTracingEnabledFor cls) $ mkMsg >>= addTrace cls - def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.isDefEq t s def inferType (e : Expr) : TermElabM Expr := liftMetaM $ Meta.inferType e def whnf (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnf e diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean index 8498b00004..a9158ca7a8 100644 --- a/src/Init/Lean/Meta/Basic.lean +++ b/src/Init/Lean/Meta/Basic.lean @@ -310,17 +310,17 @@ _root_.dbgTrace (toString a) $ fun _ => pure () @[inline] private def getTraceState : MetaM TraceState := do s ← get; pure s.traceState +def addContext (msg : MessageData) : MetaM MessageData := +do ctx ← read; + s ← get; + pure $ MessageData.context s.env s.mctx ctx.lctx msg + instance tracer : SimpleMonadTracerAdapter MetaM := { getOptions := getOptions, getTraceState := getTraceState, + addContext := addContext, modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } } -@[inline] def trace (cls : Name) (msg : Unit → MessageData) : MetaM Unit := -whenM (MonadTracerAdapter.isTracingEnabledFor cls) $ do - ctx ← read; - s ← get; - MonadTracerAdapter.addTrace cls (MessageData.context s.env s.mctx ctx.lctx (msg ())) - def getConstAux (constName : Name) (exception? : Bool) : MetaM (Option ConstantInfo) := do env ← getEnv; match env.find constName with diff --git a/src/Init/Lean/Meta/Check.lean b/src/Init/Lean/Meta/Check.lean index b20a230a36..1c4f324092 100644 --- a/src/Init/Lean/Meta/Check.lean +++ b/src/Init/Lean/Meta/Check.lean @@ -85,7 +85,7 @@ def isTypeCorrect (e : Expr) : MetaM Bool := catch (traceCtx `Meta.check $ do checkAux e; pure true) (fun ex => do - trace `Meta.typeError $ fun _ => ex.toMessageData; + trace! `Meta.typeError ex.toMessageData; pure false) @[init] private def regTraceClasses : IO Unit := diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean index 88268c452e..fc9ab73e44 100644 --- a/src/Init/Lean/Meta/ExprDefEq.lean +++ b/src/Init/Lean/Meta/ExprDefEq.lean @@ -438,18 +438,18 @@ end CheckAssignment private def checkAssignmentFailure (mvarId : MVarId) (fvars : Array Expr) (v : Expr) (ex : CheckAssignment.Exception) : MetaM (Option Expr) := match ex with | CheckAssignment.Exception.occursCheck => do - trace `Meta.isDefEq.assign.occursCheck $ fun _ => mkMVar mvarId ++ fvars ++ " := " ++ v; + trace! `Meta.isDefEq.assign.occursCheck (mkMVar mvarId ++ fvars ++ " := " ++ v); pure none | CheckAssignment.Exception.useFOApprox => pure none | CheckAssignment.Exception.outOfScopeFVar fvarId => do - trace `Meta.isDefEq.assign.outOfScopeFVar $ fun _ => mkFVar fvarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v; + trace! `Meta.isDefEq.assign.outOfScopeFVar (mkFVar fvarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v); pure none | CheckAssignment.Exception.readOnlyMVarWithBiggerLCtx nestedMVarId => do - trace `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx $ fun _ => mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v; + trace! `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx (mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v); pure none | CheckAssignment.Exception.mvarTypeNotWellFormedInSmallerLCtx nestedMVarId => do - trace `Meta.isDefEq.assign.mvarTypeNotWellFormedInSmallerLCtx $ fun _ => mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v; + trace! `Meta.isDefEq.assign.mvarTypeNotWellFormedInSmallerLCtx (mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v); pure none | CheckAssignment.Exception.unknownExprMVar mvarId => -- This case can only happen if the MetaM API is being misused @@ -604,7 +604,7 @@ else -/ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr) : Expr → MetaM Bool | v => do - trace `Meta.isDefEq.foApprox $ fun _ => mvar ++ " " ++ args ++ " := " ++ v; + trace! `Meta.isDefEq.foApprox (mvar ++ " " ++ args ++ " := " ++ v); condM (try $ processAssignmentFOApproxAux mvar args v) (pure true) (do v? ← unfoldDefinition v; @@ -688,7 +688,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) It assumes `?m` is unassigned. -/ private def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool := traceCtx `Meta.isDefEq.assign $ do - trace `Meta.isDefEq.assign $ fun _ => mvarApp ++ " := " ++ v; + trace! `Meta.isDefEq.assign (mvarApp ++ " := " ++ v); let mvar := mvarApp.getAppFn; mvarDecl ← getMVarDecl mvar.mvarId!; processAssignmentAux mvar mvarDecl v 0 mvarApp.getAppArgs @@ -704,17 +704,17 @@ toLBoolM $ isListLevelDefEqAux us vs /-- Auxiliary method for isDefEqDelta -/ private def isDefEqLeft (fn : Name) (t s : Expr) : MetaM LBool := -do trace `Meta.isDefEq.delta.unfoldLeft $ fun _ => fn; +do trace! `Meta.isDefEq.delta.unfoldLeft fn; toLBoolM $ isExprDefEqAux t s /-- Auxiliary method for isDefEqDelta -/ private def isDefEqRight (fn : Name) (t s : Expr) : MetaM LBool := -do trace `Meta.isDefEq.delta.unfoldRight $ fun _ => fn; +do trace! `Meta.isDefEq.delta.unfoldRight fn; toLBoolM $ isExprDefEqAux t s /-- Auxiliary method for isDefEqDelta -/ private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := -do trace `Meta.isDefEq.delta.unfoldLeftRight $ fun _ => fn; +do trace! `Meta.isDefEq.delta.unfoldLeftRight fn; toLBoolM $ isExprDefEqAux t s /-- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ`. @@ -728,7 +728,7 @@ traceCtx `Meta.isDefEq.delta $ b ← isDefEqArgs tFn t.getAppArgs s.getAppArgs <&&> isListLevelDefEqAux tFn.constLevels! sFn.constLevels!; - unless b $ trace `Meta.isDefEq.delta $ fun _ => "heuristic failed " ++ t ++ " =?= " ++ s; + unless b $ trace! `Meta.isDefEq.delta ("heuristic failed " ++ t ++ " =?= " ++ s); pure b /-- Auxiliary method for isDefEqDelta -/ diff --git a/src/Init/Lean/Meta/LevelDefEq.lean b/src/Init/Lean/Meta/LevelDefEq.lean index e7fbd55b92..40f568ce7f 100644 --- a/src/Init/Lean/Meta/LevelDefEq.lean +++ b/src/Init/Lean/Meta/LevelDefEq.lean @@ -58,7 +58,7 @@ partial def isLevelDefEqAux : Level → Level → MetaM Bool if lhs == rhs then pure true else do - trace `Meta.isLevelDefEq.step $ fun _ => lhs ++ " =?= " ++ rhs; + trace! `Meta.isLevelDefEq.step (lhs ++ " =?= " ++ rhs); lhs' ← instantiateLevelMVars lhs; let lhs' := lhs'.normalize; rhs' ← instantiateLevelMVars rhs; @@ -124,7 +124,7 @@ private partial def processPostponedAux : Unit → MetaM Bool if numPostponed == 0 then pure true else do - trace `Meta.isLevelDefEq.postponed $ fun _ => "processing #" ++ toString numPostponed ++ " postponed is-def-eq level constraints"; + trace! `Meta.isLevelDefEq.postponed ("processing #" ++ toString numPostponed ++ " postponed is-def-eq level constraints"); r ← processPostponedStep; if !r then pure r @@ -135,7 +135,7 @@ private partial def processPostponedAux : Unit → MetaM Bool else if numPostponed' < numPostponed then processPostponedAux () else do - trace `Meta.isLevelDefEq.postponed $ fun _ => format "no progress solving pending is-def-eq level constraints"; + trace! `Meta.isLevelDefEq.postponed (format "no progress solving pending is-def-eq level constraints"); pure false private def processPostponed : MetaM Bool := @@ -188,13 +188,13 @@ do s ← get; def isLevelDefEq (u v : Level) : MetaM Bool := traceCtx `Meta.isLevelDefEq $ do b ← try $ isLevelDefEqAux u v; - trace `Meta.isLevelDefEq $ fun _ => u ++ " =?= " ++ v ++ " ... " ++ if b then "success" else "failure"; + trace! `Meta.isLevelDefEq (u ++ " =?= " ++ v ++ " ... " ++ if b then "success" else "failure"); pure b def isExprDefEq (t s : Expr) : MetaM Bool := traceCtx `Meta.isDefEq $ do b ← try $ isExprDefEqAux t s; - trace `Meta.isDefEq $ fun _ => t ++ " =?= " ++ s ++ " ... " ++ if b then "success" else "failure"; + trace! `Meta.isDefEq (t ++ " =?= " ++ s ++ " ... " ++ if b then "success" else "failure"); pure b abbrev isDefEq := @isExprDefEq diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean index f2384424e6..66d81c4c4f 100644 --- a/src/Init/Lean/Meta/SynthInstance.lean +++ b/src/Init/Lean/Meta/SynthInstance.lean @@ -140,28 +140,19 @@ abbrev SynthM := ReaderT Context (EStateM Exception State) instance SynthM.inhabited {α} : Inhabited (SynthM α) := ⟨throw $ Exception.other ""⟩ -@[inline] private def getTraceState : SynthM TraceState := -do s ← get; pure s.traceState - -@[inline] private def getOptions : SynthM Options := -do ctx ← read; pure ctx.config.opts +def getTraceState : SynthM TraceState := do s ← get; pure s.traceState +def getOptions : SynthM Options := do ctx ← read; pure ctx.config.opts +def addContext (msg : MessageData) : SynthM MessageData := +do ctx ← read; + s ← get; + pure $ MessageData.context s.env s.mctx ctx.lctx msg instance tracer : SimpleMonadTracerAdapter SynthM := { getOptions := getOptions, getTraceState := getTraceState, + addContext := addContext, modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } } -def traceCore (cls : Name) (msg : MessageData) : SynthM Unit := -do ctx ← read; - s ← get; - MonadTracerAdapter.addTrace cls (MessageData.context s.env s.mctx ctx.lctx msg) - -@[inline] def trace (cls : Name) (msg : Unit → MessageData) : SynthM Unit := -whenM (MonadTracerAdapter.isTracingEnabledFor cls) $ traceCore cls (msg ()) - -@[inline] def traceM (cls : Name) (mkMsg : SynthM MessageData) : SynthM Unit := -whenM (MonadTracerAdapter.isTracingEnabledFor cls) (do msg ← mkMsg; traceCore cls msg) - @[inline] def liftMeta {α} (x : MetaM α) : SynthM α := adaptState (fun (s : State) => (s.toState, s)) (fun s' s => { toState := s', .. s }) x @@ -184,7 +175,7 @@ forallTelescopeReducing type $ fun _ type => do result ← result.mapM $ fun c => match c with | Expr.const constName us _ => do us ← us.mapM (fun _ => mkFreshLevelMVar); pure $ c.updateConst! us | _ => panic! "global instance is not a constant"; - Meta.trace `Meta.synthInstance.globalInstances $ fun _ => type ++ " " ++ result; + trace! `Meta.synthInstance.globalInstances (type ++ " " ++ result); localInstances ← getLocalInstances; let result := localInstances.foldl (fun (result : Array Expr) linst => if linst.className == className then result.push linst.fvar else result) @@ -195,7 +186,7 @@ forallTelescopeReducing type $ fun _ type => do `key` must be `mkTableKey mctx mvarType`. -/ def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Waiter) : SynthM Unit := withMCtx mctx $ do - trace `Meta.synthInstance.newSubgoal $ fun _ => key; + trace! `Meta.synthInstance.newSubgoal key; mvarType ← inferType mvar; mvarType ← instantiateMVars mvarType; instances ← getInstances mvarType; @@ -286,16 +277,16 @@ do mvarType ← inferType mvar; localInsts ← getLocalInstances; forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do (subgoals, instVal, instTypeBody) ← getSubgoals lctx localInsts xs inst; - Meta.trace `Meta.synthInstance.tryResolve $ fun _ => mvarTypeBody ++ " =?= " ++ instTypeBody; + trace! `Meta.synthInstance.tryResolve (mvarTypeBody ++ " =?= " ++ instTypeBody); condM (isDefEq mvarTypeBody instTypeBody) (do instVal ← mkLambda xs instVal; condM (isDefEq mvar instVal) - (do Meta.trace `Meta.synthInstance.tryResolve $ fun _ => fmt "success"; + (do trace! `Meta.synthInstance.tryResolve "success"; mctx ← getMCtx; pure (some (mctx, subgoals))) - (do Meta.trace `Meta.synthInstance.tryResolve $ fun _ => fmt "failure assigning"; + (do trace! `Meta.synthInstance.tryResolve "failure assigning"; pure none)) - (do Meta.trace `Meta.synthInstance.tryResolve $ fun _ => fmt "failure"; + (do trace! `Meta.synthInstance.tryResolve "failure"; pure none) /-- @@ -323,7 +314,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit modify $ fun s => { result := answer.expr, .. s } else do (_, _, answerExpr) ← openAbstractMVarsResult answer; - trace `Meta.synthInstance $ fun _ => "skip answer containing metavariables " ++ answerExpr; + trace! `Meta.synthInstance ("skip answer containing metavariables " ++ answerExpr); pure () | Waiter.consumerNode cNode => modify $ fun s => { resumeStack := s.resumeStack.push (cNode, answer), .. s } @@ -379,7 +370,7 @@ do gNode ← getTop; let inst := gNode.instances.get! idx; let mctx := gNode.mctx; let mvar := gNode.mvar; - trace `Meta.synthInstance.generate $ fun _ => "instance " ++ inst; + trace! `Meta.synthInstance.generate ("instance " ++ inst); modifyTop $ fun gNode => { currInstanceIdx := idx, .. gNode }; result? ← tryResolve mctx mvar inst; match result? with @@ -422,7 +413,7 @@ do s ← get; pure s.result partial def synth : Nat → SynthM (Option Expr) | 0 => do - trace `Meta.synthInstance $ fun _ => fmt "synthInstance is out of fule"; + trace! `Meta.synthInstance "synthInstance is out of fule"; pure none | n+1 => do condM step @@ -430,12 +421,12 @@ partial def synth : Nat → SynthM (Option Expr) match result? with | none => synth n | some result => pure result) - (do trace `Meta.synthInstance $ fun _ => fmt "failed"; + (do trace! `Meta.synthInstance "failed"; pure none) def main (type : Expr) (fuel : Nat) : MetaM (Option Expr) := traceCtx `Meta.synthInstance $ do - Meta.trace `Meta.synthInstance $ fun _ => "main goal " ++ type; + trace! `Meta.synthInstance ("main goal " ++ type); mvar ← mkFreshExprMVar type; mctx ← getMCtx; let key := mkTableKey mctx type; diff --git a/src/Init/Lean/Util/Trace.lean b/src/Init/Lean/Util/Trace.lean index 9456adfefd..2a7bc0a067 100644 --- a/src/Init/Lean/Util/Trace.lean +++ b/src/Init/Lean/Util/Trace.lean @@ -11,10 +11,12 @@ namespace Lean class MonadTracer (m : Type → Type u) := (traceCtx {α} : Name → m α → m α) -(trace {} : Name → (Unit → MessageData) → m PUnit) +(trace {} : Name → (Unit → MessageData) → m PUnit) +(traceM {} : Name → m MessageData → m PUnit) class MonadTracerAdapter (m : Type → Type) := (isTracingEnabledFor {} : Name → m Bool) +(addContext {} : MessageData → m MessageData) (enableTracing {} : Bool → m Bool) (getTraces {} : m (Array MessageData)) (modifyTraces {} : (Array MessageData → Array MessageData) → m Unit) @@ -37,7 +39,8 @@ do oldTraces ← getTraces; pure oldTraces def addTrace (cls : Name) (msg : MessageData) : m Unit := -modifyTraces $ fun traces => traces.push (MessageData.tagged cls msg) +do msg ← addContext msg; + modifyTraces $ fun traces => traces.push (MessageData.tagged cls msg) @[inline] protected def trace (cls : Name) (msg : Unit → MessageData) : m Unit := whenM (isTracingEnabledFor cls) (addTrace cls (msg ())) @@ -80,11 +83,13 @@ end MonadTracerAdapter instance monadTracerAdapter {m : Type → Type} [Monad m] [MonadTracerAdapter m] : MonadTracer m := { traceCtx := @MonadTracerAdapter.traceCtx _ _ _, - trace := @MonadTracerAdapter.trace _ _ _ } + trace := @MonadTracerAdapter.trace _ _ _, + traceM := @MonadTracerAdapter.traceM _ _ _ } instance monadTracerAdapterExcept {ε : Type} {m : Type → Type} [Monad m] [MonadExcept ε m] [MonadTracerAdapter m] : MonadTracer m := { traceCtx := @MonadTracerAdapter.traceCtxExcept _ _ _ _ _, - trace := @MonadTracerAdapter.trace _ _ _ } + trace := @MonadTracerAdapter.trace _ _ _, + traceM := @MonadTracerAdapter.traceM _ _ _ } structure TraceState := (enabled : Bool := true) @@ -104,6 +109,7 @@ class SimpleMonadTracerAdapter (m : Type → Type) := (getOptions {} : m Options) (modifyTraceState {} : (TraceState → TraceState) → m Unit) (getTraceState {} : m TraceState) +(addContext {} : MessageData → m MessageData) namespace SimpleMonadTracerAdapter variables {m : Type → Type} [Monad m] [SimpleMonadTracerAdapter m] @@ -140,9 +146,10 @@ instance simpleMonadTracerAdapter {m : Type → Type} [SimpleMonadTracerAdapter { isTracingEnabledFor := @SimpleMonadTracerAdapter.isTracingEnabledFor _ _ _, enableTracing := @SimpleMonadTracerAdapter.enableTracing _ _ _, getTraces := @SimpleMonadTracerAdapter.getTraces _ _ _, + addContext := @SimpleMonadTracerAdapter.addContext _ _, modifyTraces := @SimpleMonadTracerAdapter.modifyTraces _ _ _ } -export MonadTracer (traceCtx trace) +export MonadTracer (traceCtx trace traceM) /- Recipe for adding tracing support for a monad `M`. diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean index ccdb9ae0cc..54494422fb 100644 --- a/tests/lean/run/trace.lean +++ b/tests/lean/run/trace.lean @@ -11,6 +11,7 @@ abbrev M := ReaderT Options (EStateM String MyState) instance : SimpleMonadTracerAdapter M := { getOptions := read, getTraceState := MyState.traceState <$> get, + addContext := pure, modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } } def tst1 : M Unit :=