1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
//! Reduction Statistics Tracking for the OxiLean kernel.
//!
//! This module provides [`ReductionStats`] — a lightweight, zero-dependency
//! accumulator for counting and profiling WHNF reductions.
//!
//! # Tracked quantities
//!
//! | Field | Meaning |
//! |---------------|-----------------------------------------------------|
//! | `beta_count` | β-reductions `(λ x, t) a → t[a/x]` |
//! | `delta_count` | δ-reductions (definition unfoldings) |
//! | `zeta_count` | ζ-reductions `let x := v in t → t[v/x]` |
//! | `iota_count` | ι-reductions (recursor / match evaluations) |
//! | `eta_count` | η-reductions |
//! | `level_count` | Universe-level simplifications |
//! | `total_steps` | Sum of all counters |
//! | `max_depth` | Maximum recursion depth seen in a single WHNF call |
//!
//! # Usage
//!
//! ```
//! use oxilean_kernel::reduction_stats::ReductionStats;
//!
//! let mut stats = ReductionStats::new();
//! stats.increment_beta();
//! stats.increment_delta();
//! assert_eq!(stats.total(), 2);
//! assert_eq!(stats.beta_count, 1);
//! ```
//!
//! ## Depth tracking
//!
//! Use [`DepthGuard`] to automatically push/pop the depth counter in
//! recursive WHNF functions:
//!
//! ```ignore
//! use oxilean_kernel::reduction_stats::{ReductionStats, DepthGuard};
//!
//! fn whnf_recursive(expr: &Expr, stats: &mut ReductionStats) -> Expr {
//! let _guard = DepthGuard::new(stats);
//! // ... reduction logic ...
//! todo!()
//! }
//! ```
//!
//! ## Session-level deltas
//!
//! [`ReductionSession`] captures a before/after delta for a single
//! type-checking task:
//!
//! ```ignore
//! use oxilean_kernel::reduction_stats::{ReductionStats, ReductionSession};
//!
//! let mut stats = ReductionStats::new();
//! let session = ReductionSession::begin(&stats);
//! // ... run type checker ...
//! let delta = session.finish(&stats);
//! println!("Steps: {}", delta.total());
//! ```
pub use *;
pub use *;