Documentation

Lean.Util.Trace

structure Lean.TraceElem:

Type

ref : Lean.Syntax
msg : Lean.MessageData

instance Lean.instInhabitedTraceElem:

Inhabited Lean.TraceElem

Equations

Lean.instInhabitedTraceElem = { default := { ref := default, msg := default } }

structure Lean.TraceState:

Type

enabled : Bool
traces : Std.PersistentArray Lean.TraceElem

instance Lean.instInhabitedTraceState:

Inhabited Lean.TraceState

Equations

Lean.instInhabitedTraceState = { default := { enabled := default, traces := default } }

class Lean.MonadTrace (m : Type → Type) :

Type

modifyTraceState : (Lean.TraceState → Lean.TraceState) → m Unit
getTraceState : m Lean.TraceState

Instances

instance Lean.instMonadTrace (m : Type → Type) (n : Type → Type) [inst : MonadLift m n] [inst : Lean.MonadTrace m] :

Lean.MonadTrace n

Equations

Lean.instMonadTrace m n = { modifyTraceState := fun f => liftM (Lean.modifyTraceState f), getTraceState := liftM Lean.getTraceState }

def Lean.printTraces {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : MonadLiftT IO m] :

Equations

Lean.printTraces = do let traceState ← Lean.getTraceState Std.PersistentArray.forM traceState.traces fun m => do let d ← liftM (Lean.MessageData.format m.msg) liftM (IO.println d)

def Lean.resetTraceState {m : Type → Type} [inst : Lean.MonadTrace m] :

Equations

One or more equations did not get rendered due to their size.

def Lean.checkTraceOption (opts : Lean.Options) (cls : Lean.Name) :

Equations

Lean.checkTraceOption opts cls = if Lean.KVMap.isEmpty opts = true then false else Lean.checkTraceOptionAux opts (`trace ++ cls)

@[inline]

def Lean.isTracingEnabledFor {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] (cls : Lean.Name) :

Equations

Lean.isTracingEnabledFor cls = do let s ← Lean.getTraceState if (!s.enabled) = true then pure false else Lean.checkTraceOptionM cls

@[inline]

def Lean.enableTracing {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] (b : Bool) :

Equations

Lean.enableTracing b = do let s ← Lean.getTraceState let oldEnabled : Bool := s.enabled Lean.modifyTraceState fun s => { enabled := b, traces := s.traces } pure oldEnabled

@[inline]

def Lean.getTraces {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] :

m (Std.PersistentArray Lean.TraceElem)

Equations

Lean.getTraces = do let s ← Lean.getTraceState pure s.traces

@[inline]

def Lean.modifyTraces {m : Type → Type} [inst : Lean.MonadTrace m] (f : Std.PersistentArray Lean.TraceElem → Std.PersistentArray Lean.TraceElem) :

Equations

Lean.modifyTraces f = Lean.modifyTraceState fun s => { enabled := s.enabled, traces := f s.traces }

@[inline]

def Lean.setTraceState {m : Type → Type} [inst : Lean.MonadTrace m] (s : Lean.TraceState) :

Equations

Lean.setTraceState s = Lean.modifyTraceState fun x => s

def Lean.addRawTrace {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] [inst : Lean.AddMessageContext m] (msg : Lean.MessageData) :

Equations

One or more equations did not get rendered due to their size.

def Lean.addTrace {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] [inst : Lean.AddMessageContext m] (cls : Lean.Name) (msg : Lean.MessageData) :

Equations

One or more equations did not get rendered due to their size.

@[inline]

def Lean.trace {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (cls : Lean.Name) (msg : Unit → Lean.MessageData) :

Equations

Lean.trace cls msg = do let a ← Lean.isTracingEnabledFor cls if a = true then Lean.addTrace cls (msg ()) else pure PUnit.unit

@[inline]

def Lean.traceM {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (cls : Lean.Name) (mkMsg : m Lean.MessageData) :

Equations

Lean.traceM cls mkMsg = do let a ← Lean.isTracingEnabledFor cls if a = true then do let msg ← mkMsg Lean.addTrace cls msg else pure PUnit.unit

@[inline]

def Lean.traceCtx {α : Type} {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] [inst : Lean.MonadOptions m] [inst : MonadFinally m] (cls : Lean.Name) (ctx : m α) :

m α

Equations

One or more equations did not get rendered due to their size.

def Lean.MonadTracer.trace {m : Type → Type} [inst : Monad m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (cls : Lean.Name) (msg : Unit → Lean.MessageData) :

Equations

Lean.MonadTracer.trace cls msg = Lean.trace cls msg

def Lean.registerTraceClass (traceClassName : Lean.Name) :

Equations

One or more equations did not get rendered due to their size.

def Lean.«doElemTrace[_]__»:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

@[inline]

def Lean.withNestedTraces {α : Type} {m : Type → Type} [inst : Monad m] [inst : MonadFinally m] [inst : Lean.MonadTrace m] [inst : Lean.MonadRef m] (x : m α) :

m α

Equations

One or more equations did not get rendered due to their size.