Struct Reducer 

pub struct Reducer { /* private fields */ }

Reduction context with caching.

Implementations

impl Reducer

pub fn new() -> Self

Create a new reducer with default settings.

pub fn with_max_depth(max_depth: u32) -> Self

Create a reducer with custom max depth.

pub fn record_fvar_type(&mut self, id: FVarId, ty: Expr)

Record the type of a free variable opened by the surrounding checker so K-like iota reduction can type majors that mention it.

FVarIds are dispensed monotonically and never reused, so recorded types are stable and cached WHNF results stay sound. Defensively, a re-bind that could make them unsound invalidates the cache: an id in scope given a different type, or an id whose binder was closed (Self::forget_fvar_type) bound again.

pub fn forget_fvar_type(&mut self, id: FVarId)

The binder of a free variable recorded with Self::record_fvar_type has been closed: forget its type.

Nothing reduced from here on mentions the variable, so nothing needs its type; cached WHNF results that mention it are never looked up again, since its id is not dispensed again (and if a caller does bind it again, Self::record_fvar_type invalidates the cache). Without this the mirror grows by one type per binder opened, for as long as the reducer lives.

pub fn set_transparency(&mut self, mode: TransparencyMode)

Set the transparency mode.

pub fn clear_cache(&mut self)

Clear the cache (call between declarations).

pub fn whnf(&mut self, expr: &Expr) -> Expr

Reduce an expression to Weak Head Normal Form.

This implements all reduction rules except delta (which needs environment).

pub fn whnf_delta<F>(&mut self, expr: &Expr, lookup: &F) -> Expr

where F: Fn(&Name) -> Option<(Expr, ReducibilityHint)>,

Reduce to WHNF with delta-reduction (constant unfolding).

This requires environment access to look up definitions.

pub fn whnf_env(&mut self, expr: &Expr, env: &Environment) -> Expr

Full WHNF with environment-aware reductions.

Performs: beta, zeta, delta, iota (recursor), projection, nat/string ops.

pub fn is_alpha_equiv(e1: &Expr, e2: &Expr) -> bool

Check if two expressions are alpha-equivalent (syntactically equal).

Trait Implementations

impl Default for Reducer

fn default() -> Self

Returns the “default value” for a type.