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

Lean.resetTraceState = Lean.modifyTraceState fun x => { enabled := true, traces := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }

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

Lean.addTrace cls msg = (fun addTraceOptions => do let ref ← Lean.getRef let msg ← Lean.addMessageContext msg let msg : Lean.MessageData := addTraceOptions msg Lean.modifyTraces fun traces => Std.PersistentArray.push traces { ref := ref, msg := Lean.MessageData.tagged (cls ++ `_traceMsg) (Lean.toMessageData "[" ++ Lean.toMessageData cls ++ Lean.toMessageData "] " ++ Lean.toMessageData msg ++ Lean.toMessageData "") }) Lean.addTrace.addTraceOptions

def Lean.addTrace.addTraceOptions :

Lean.MessageData → Lean.MessageData

Equations

Lean.addTrace.addTraceOptions x = match x with | Lean.MessageData.withContext ctx msg => Lean.MessageData.withContext { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := Lean.KVMap.setBool ctx.opts `pp.analyze false } msg | msg => msg

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

Lean.traceCtx cls ctx = do let b ← Lean.isTracingEnabledFor cls if (!b) = true then do let old ← Lean.enableTracing false tryFinally ctx (Lean.enableTracing old) else do let ref ← Lean.getRef let oldCurrTraces ← Lean.getResetTraces tryFinally ctx (Lean.addNode oldCurrTraces cls ref)

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

Lean.registerTraceClass traceClassName = Lean.registerOption (`trace ++ traceClassName) { defValue := Lean.DataValue.ofBool false, group := "trace", descr := "enable/disable tracing for the given module and submodules" }

def Lean.«doElemTrace[__]__» :

Lean.ParserDescr

Equations

Lean.«doElemTrace[__]__» = Lean.ParserDescr.node `Lean.«doElemTrace[__]__» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "trace[") (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.symbol "]")) (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.unary `interpolatedStr (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.cat `term 0)))

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

Lean.withNestedTraces x = do let currTraces ← Lean.getTraces Lean.modifyTraces fun x => { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } let ref ← Lean.getRef tryFinally x (Lean.withNestedTracesFinalizer ref currTraces)