max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: MonadTracer and helper functions

Browse source 
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.
This commit is contained in:
Leonardo de Moura 2019-12-08 09:05:15 -08:00
parent f93b675ad4
commit 1352619ee4
8 changed files with 58 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Init/Lean/Elab/Term.lean
View file

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

12
src/Init/Lean/Meta/Basic.lean
View file

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

2
src/Init/Lean/Meta/Check.lean
View file

@ -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 :=

20
src/Init/Lean/Meta/ExprDefEq.lean
View file

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

10
src/Init/Lean/Meta/LevelDefEq.lean
View file

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

45
src/Init/Lean/Meta/SynthInstance.lean
View file

@ -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;

17
src/Init/Lean/Util/Trace.lean
View file

@ -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`.

1
tests/lean/run/trace.lean
View file

@ -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 :=