oxilean_kernel/def_eq_cache/
mod.rs

1//! Definitional Equality Cache for OxiLean Kernel.
2//!
3//! Provides a persistent cache of definitional equality results to avoid
4//! redundant re-checking of expression pairs that the kernel has already
5//! decided. Typical kernels spend significant time re-checking the same
6//! `(t1, t2)` pairs in nested reduction contexts; caching these results
7//! can yield substantial speedups.
8//!
9//! # Design
10//!
11//! - **Symmetric keys**: `DefEqKey::new(a, b) == DefEqKey::new(b, a)` since
12//!   definitional equality is symmetric.
13//! - **Hash-based**: Expression hashes (FNV-1a via `proof_cert::hash_expr`) are
14//!   used as keys. Hash collisions are benign — they may cause spurious cache
15//!   misses but never incorrect results (the hash merely gates a lookup; the
16//!   checker is always authoritative).
17//! - **Configurable eviction**: Choose `LRU`, `LFU`, or `FIFO` at construction
18//!   time via [`DefEqCache::with_eviction`].
19//! - **Memoizing wrapper**: [`with_cache`] transparently wraps any checker.
20
21pub mod functions;
22pub mod types;
23
24pub use functions::with_cache;
25pub use types::{CacheEviction, DefEqCache, DefEqCacheStats, DefEqEntry, DefEqKey};
oxilean_kernel/def_eq_cache/mod.rs

oxilean_kernel/def_eq_cache/
mod.rs
