Trait lamcal::BetaReduce [−][src]
pub trait BetaReduce { fn reduce_inspected(
expr: Term,
inspect: &mut impl Inspect
) -> Term; fn reduce(expr: Term) -> Term { ... } fn reduce_once(expr: Term) -> Term { ... } }
Defines a strategy for β-reduction of terms.
Possible implementations may follow the strategies described in the reduction strategy article on wikipedia.
Required Methods
fn reduce_inspected(
expr: Term,
inspect: &mut impl Inspect
) -> Term
expr: Term,
inspect: &mut impl Inspect
) -> Term
Performs β-reduction allowing to inspect the current term before each contraction.
Implementations must call the Inspect::inspect
function of the given
Inspect
instance exactly once before each contraction and respect
their return value. If the Inspect::inspect
function returns
Stop::Yes
the reduction must be stopped immediately, so that no
further reduction is performed.
Provided Methods
fn reduce(expr: Term) -> Term
Performs β-reduction on the given Term
and returns the result.
The default implementation limits the reduction to Limit::default()
reduction steps to prevent endless loops on diverging expressions.
fn reduce_once(expr: Term) -> Term
Performs one step of β-reduction on the given Term
and returns the
result.
Implementors
impl<A> BetaReduce for CallByName<A> where
A: AlphaRename,impl<A> BetaReduce for NormalOrder<A> where
A: AlphaRename,impl<A> BetaReduce for CallByValue<A> where
A: AlphaRename,impl<A> BetaReduce for ApplicativeOrder<A> where
A: AlphaRename,impl<A> BetaReduce for HybridApplicativeOrder<A> where
A: AlphaRename,impl<A> BetaReduce for HeadSpine<A> where
A: AlphaRename,impl<A> BetaReduce for HybridNormalOrder<A> where
A: AlphaRename,