Enum ReductionStrategy 

pub enum ReductionStrategy {
    WHNF,
    NF,
    OneStep,
    CBV,
    CBN,
    HeadOnly,
}

Reduction strategy for expression simplification.

Different strategies trade off between completeness and efficiency. Most use cases should use ReductionStrategy::WHNF or ReductionStrategy::NF.

Variants

WHNF

Reduce to weak head normal form.

Only reduces the outermost redex; sub-expressions may remain unreduced. Efficient for most type-checking purposes.

NF

Reduce to normal form.

Fully reduces all sub-expressions. More expensive than WHNF.

OneStep

Reduce exactly one step.

Finds and reduces the outermost leftmost redex.

CBV

Call-by-value reduction.

Evaluates arguments before applying functions (strict evaluation).

CBN

Call-by-name reduction.

Applies functions before evaluating arguments (lazy evaluation).

HeadOnly

Head reduction only.

Like OneStep but restricted to the head position.

Implementations

impl ReductionStrategy

pub fn name(&self) -> &'static str

Returns a human-readable name for the strategy.

pub fn is_complete(&self) -> bool

Returns true if this strategy reduces to a complete normal form.

pub fn is_lazy(&self) -> bool

Returns true if this is a lazy strategy.

pub fn is_eager(&self) -> bool

Returns true if this is an eager/strict strategy.

Trait Implementations

impl Clone for ReductionStrategy

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for ReductionStrategy

impl Debug for ReductionStrategy

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for ReductionStrategy

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for ReductionStrategy

impl Hash for ReductionStrategy

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for ReductionStrategy

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for ReductionStrategy