[−][src]Enum lalrpop_lambda::Expression
A mutually recursive definition for all lambda expressions
let parser = lalrpop_lambda::parse::ExpressionParser::new(); assert!(parser.parse("λx.(x x)").is_ok());
Variants
Var(Variable)
Abs(Abstraction)
App(Application)
Methods
impl Expression
[src]
pub fn rename(&self, old: &Variable, new: &Variable) -> Self
[src]
α-conversion
pub fn apply(&self, η: bool) -> Self
[src]
β-reduction small-step semantics (→)
Represents local reducibility in natural deduction.
-
η: λx.(e1 x) -> e1 whenever x does not appear free in e1
Represents local completeness in natural deduction.
pub fn normalize(&self, η: bool) -> Self
[src]
Big-step natural semantics (⇓)
Represents global reducibility in natural deduction.
TODO: Reduction strategy.
- η: (see
Expression::apply
)
let parser = lalrpop_lambda::parse::ExpressionParser::new(); let expression = parser.parse("((λx.(λy.x y) b) a)").unwrap(); let normal = parser.parse("a b").unwrap(); assert_eq!(normal, expression.normalize(false));
pub fn variables(&self) -> HashSet<Variable>
[src]
pub fn free_variables(&self) -> HashSet<Variable>
[src]
FV(M) is the set of variables in M, not closed by a λ term.
use std::collections::HashSet; use lalrpop_lambda::Variable; let parser = lalrpop_lambda::parse::ExpressionParser::new(); let mut free = HashSet::new(); free.insert(Variable("y".into())); let expression = parser.parse("λx.(x y)").unwrap(); assert_eq!(free, expression.free_variables());
pub fn resolve(&self, env: &HashMap<Variable, Expression>) -> Expression
[src]
let env = map! { variable!(id) => abs!{x.x}, variable!(ad) => abs!{x.y}, variable!(x) => 1.into(), }; assert_eq!(var!(q), var!(q).resolve(&env)); assert_eq!(1u64, var!(x).resolve(&env).into()); // Works with functions too! let id: fn(u64) -> u64 = var!(id).resolve(&env).into(); assert_eq!(1, id(1)); let ad: fn(u64) -> u64 = var!(ad).resolve(&env).into(); assert_eq!(u64::from(var!(y)), ad(0)); assert_eq!(u64::from(var!(y)), ad(1));
Trait Implementations
impl Eq for Expression
[src]
impl PartialEq<Expression> for Expression
[src]
fn eq(&self, other: &Expression) -> bool
[src]
fn ne(&self, other: &Expression) -> bool
[src]
impl Clone for Expression
[src]
fn clone(&self) -> Expression
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more
impl<T> FnOnce(T) for Expression where
T: Into<Expression> + From<Expression>,
[src]
T: Into<Expression> + From<Expression>,
Function call support for an Expression
.
assert_eq!(0u64, λ!{x.x}(0).into()); assert_eq!(γ!(γ!(a,b),0), γ!(a,b)(0));
type Output = Expression
The returned type after the call operator is used.
extern "rust-call" fn call_once(self, t: (T,)) -> Expression
[src]
impl From<Expression> for fn(_: u64) -> u64
[src]
fn from(e: Expression) -> Self
[src]
impl From<fn(u64) -> u64> for Expression
[src]
impl From<bool> for Expression
[src]
Church encoded booleans
use lalrpop_lambda::Expression; assert_eq!(λ!{a.λ!{b.a}}, Expression::from(true)); assert_eq!(λ!{a.λ!{b.b}}, Expression::from(false));
impl From<Expression> for bool
[src]
Convert λ term back to native Rust type
assert_eq!(true , bool::from(λ!{a.λ!{b.a}})); assert_eq!(false, bool::from(λ!{a.λ!{b.γ!(b,b)}}));
fn from(e: Expression) -> bool
[src]
impl From<u64> for Expression
[src]
Church encoded natural numbers
use lalrpop_lambda::Expression; assert_eq!(λ!{f.λ!{x.x}}, Expression::from(0)); assert_eq!(λ!{f.λ!{x.γ!(f,x)}}, Expression::from(1)); assert_eq!(λ!{f.λ!{x.γ!(f,γ!(f,γ!(f,x)))}}, Expression::from(3));
impl From<Expression> for u64
[src]
Convert λ term back to native Rust type
assert_eq!(0, u64::from(λ!{f.λ!{x.x}})); assert_eq!(1, u64::from(λ!{f.λ!{x.γ!(f,x)}})); assert_eq!(3, u64::from(λ!{f.λ!{x.γ!(f,γ!(f,γ!(f,x)))}}));
fn from(e: Expression) -> u64
[src]
impl Debug for Expression
[src]
impl Display for Expression
[src]
impl Add<Expression> for Expression
[src]
let one = λ!{f.λ!{x.γ!(f,x)}}; let two = one.clone() + one.clone(); assert_eq!(2, u64::from(two.clone())); assert_eq!(4, u64::from(two.clone() + two.clone()));
type Output = Self
The resulting type after applying the +
operator.
fn add(self, other: Self) -> Self
[src]
impl Mul<Expression> for Expression
[src]
let one = λ!{f.λ!{x.γ!(f,x)}}; let two = one.clone() + one.clone(); assert_eq!(1, u64::from(one.clone() * one.clone())); assert_eq!(4, u64::from(two.clone() * two.clone()));
type Output = Self
The resulting type after applying the *
operator.
fn mul(self, other: Self) -> Self
[src]
impl Not for Expression
[src]
let t = λ!{a.λ!{b.a}}; assert_eq!(false, bool::from(!t.clone())); assert_eq!(true, bool::from(!!t.clone()));
Evaluation Strategy
Note that there are two version of not, depending on the evaluation strategy that is chosen. We currently only evaluate using application order, so we choose the first option.
- Applicative evaluation order: λp.λa.λb.p b a
- Normal evaluation order: λp.p (λa.λb.b) (λa.λb.a)
impl BitAnd<Expression> for Expression
[src]
let t = λ!{a.λ!{b.a}}; let f = λ!{a.λ!{b.b}}; assert_eq!(true, bool::from(t.clone() & t.clone())); assert_eq!(false, bool::from(t.clone() & f.clone())); assert_eq!(false, bool::from(f.clone() & t.clone())); assert_eq!(false, bool::from(f.clone() & f.clone()));
type Output = Self
The resulting type after applying the &
operator.
fn bitand(self, other: Self) -> Self
[src]
impl BitOr<Expression> for Expression
[src]
let t = λ!{a.λ!{b.a}}; let f = λ!{a.λ!{b.b}}; assert_eq!(true, bool::from(t.clone() | t.clone())); assert_eq!(true, bool::from(t.clone() | f.clone())); assert_eq!(true, bool::from(f.clone() | t.clone())); assert_eq!(false, bool::from(f.clone() | f.clone()));
type Output = Self
The resulting type after applying the |
operator.
fn bitor(self, other: Self) -> Self
[src]
impl BitXor<Expression> for Expression
[src]
let t = λ!{a.λ!{b.a}}; let f = λ!{a.λ!{b.b}}; assert_eq!(false, bool::from(t.clone() ^ t.clone())); assert_eq!(true, bool::from(t.clone() ^ f.clone())); assert_eq!(true, bool::from(f.clone() ^ t.clone())); assert_eq!(false, bool::from(f.clone() ^ f.clone()));
Auto Trait Implementations
impl Send for Expression
impl Sync for Expression
Blanket Implementations
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T> From<T> for T
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<A, F> FnBox<A> for F where
F: FnOnce<A>,
[src]
F: FnOnce<A>,