From f93b675ad4e8faeca683b2f6a269ca09aff0aa71 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Dec 2019 08:34:00 -0800
Subject: [PATCH] feat: add tracing support

---
 src/Init/Lean/Elab/Term.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index e0ec37123a..0e57c79c16 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -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