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

feat: add tracing support

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-08 08:34:00 -08:00
parent 713fd29e92
commit f93b675ad4
1 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -86,6 +86,28 @@ fun ctx s => match x ctx.toContext s.toState with
| EStateM.Result.ok a newS => EStateM.Result.ok a { toState := newS, .. s }
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { toState := newS, .. s }
def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts
def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState
instance tracer : SimpleMonadTracerAdapter TermElabM :=
{ getOptions := getOptions,
getTraceState := getTraceState,
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