Struct Tracer 

pub struct Tracer { /* private fields */ }

Tracer for collecting debugging information during type checking.

Implementations

impl Tracer

pub fn new(level: TraceLevel) -> Self

Create a new tracer with the given level.

pub fn silent() -> Self

Create a silent tracer.

pub fn verbose() -> Self

Create a fully verbose tracer.

pub fn set_level(&mut self, level: TraceLevel)

Set the trace level.

pub fn level(&self) -> TraceLevel

Get the trace level.

pub fn set_max_events(&mut self, max: usize)

Set the max events buffer size.

pub fn set_timing(&mut self, enabled: bool)

Enable or disable timing.

pub fn suppress(&mut self, cat: TraceCategory)

Suppress a category.

pub fn allow(&mut self, cat: &TraceCategory)

Allow a category.

pub fn log(&mut self, event: TraceEvent)

Log a trace event.

pub fn log_msg(&mut self, level: TraceLevel, msg: impl Into<String>)

Log a string at the given level.

pub fn error(&mut self, msg: impl Into<String>)

Log an error.

pub fn warn(&mut self, msg: impl Into<String>)

Log a warning.

pub fn info(&mut self, msg: impl Into<String>)

Log an info message.

pub fn debug(&mut self, msg: impl Into<String>)

Log a debug message.

pub fn trace_msg(&mut self, msg: impl Into<String>)

Log a trace message.

pub fn trace_infer(&mut self, msg: impl Into<String>)

Log a trace-level message in the Infer category.

pub fn trace_reduce(&mut self, msg: impl Into<String>)

Log a trace-level message in the Reduce category.

pub fn record_reduction( &mut self, rule: ReductionRule, before: Expr, after: Expr, )

Record a reduction step.

pub fn reduction_steps(&self) -> &[ReductionStep]

Get reduction steps.

pub fn clear_reductions(&mut self)

Clear reduction steps.

pub fn events(&self) -> &[TraceEvent]

Get all logged events.

pub fn events_at_level(&self, level: TraceLevel) -> Vec<&TraceEvent>

Get events at a specific level.

pub fn events_in_category(&self, cat: &TraceCategory) -> Vec<&TraceEvent>

Get events in a specific category.

pub fn clear(&mut self)

Clear all events.

pub fn event_count(&self) -> usize

Count events.

pub fn push(&mut self)

Push depth.

pub fn pop(&mut self)

Pop depth.

pub fn current_depth(&self) -> u32

Get current depth.

pub fn elapsed(&self) -> Option<Duration>

Get elapsed time since tracing started.

pub fn render(&self) -> String

Render all events as a multi-line string.

impl Tracer

Extension trait for Tracer providing convenience methods.

pub fn debug_return<T>(&mut self, value: T, msg: impl Into<String>) -> T

Log and return a message at Debug level.

pub fn debug_expr(&mut self, label: &str, expr: &Expr)

Log an expression at Debug level.

pub fn stats(&self) -> TracerStats

Compute statistics for this tracer.

pub fn last_event(&self) -> Option<&TraceEvent>

Return the most recent event, if any.

pub fn last_error(&self) -> Option<&TraceEvent>

Return the most recent error event, if any.

pub fn is_empty(&self) -> bool

Check whether the tracer has any events.

pub fn log_with_category( &mut self, level: TraceLevel, category: TraceCategory, msg: impl Into<String>, )

Log with a specific category.

pub fn log_infer(&mut self, msg: impl Into<String>)

Log an infer event at Debug level.

pub fn log_simp(&mut self, msg: impl Into<String>)

Log a simp event at Trace level.

pub fn log_tactic(&mut self, msg: impl Into<String>)

Log a tactic event at Info level.

pub fn log_elab(&mut self, msg: impl Into<String>)

Log an elaboration event at Debug level.

pub fn category_log(&self, cat: &TraceCategory) -> Vec<String>

Return all events in a given category as formatted strings.

pub fn clear_category(&mut self, cat: &TraceCategory)

Clear only events in a given category.

Trait Implementations

impl Default for Tracer

fn default() -> Self

Returns the “default value” for a type.