Enum lambda_calculus::term::Term [] [src]

pub enum Term {
    Var(usize),
    Abs(Box<Term>),
    App(Box<Term>, Box<Term>),
}

A lambda term that is either a variable with a De Bruijn index, an abstraction over a term or an applicaction of one term to another.

Variants

a variable

an abstraction

an application

Methods

impl Term
[src]

[src]

Returns a variable's De Bruijn index, consuming it in the process.

Example

use lambda_calculus::*;

assert_eq!(Var(1).unvar(), Ok(1));

Errors

Returns a TermError if self is not a Variable.

[src]

Returns a reference to a variable's De Bruijn index.

Example

use lambda_calculus::*;

assert_eq!(Var(1).unvar_ref(), Ok(&1));

Errors

Returns a TermError if self is not a Variable.

[src]

Returns a mutable reference to a variable's De Bruijn index.

Example

use lambda_calculus::*;

assert_eq!(Var(1).unvar_mut(), Ok(&mut 1));

Errors

Returns a TermError if self is not a Variable.

[src]

Returns an abstraction's underlying term, consuming it in the process.

Example

use lambda_calculus::*;

assert_eq!(abs(Var(1)).unabs(), Ok(Var(1)));

Errors

Returns a TermError if self is not an Abstraction.

[src]

Returns a reference to an abstraction's underlying term.

Example

use lambda_calculus::*;

assert_eq!(abs(Var(1)).unabs_ref(), Ok(&Var(1)));

Errors

Returns a TermError if self is not an Abstraction.

[src]

Returns a mutable reference to an abstraction's underlying term.

Example

use lambda_calculus::*;

assert_eq!(abs(Var(1)).unabs_mut(), Ok(&mut Var(1)));

Errors

Returns a TermError if self is not an Abstraction.

[src]

Returns a pair containing an application's underlying terms, consuming it in the process.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).unapp(), Ok((Var(1), Var(2))));

Errors

Returns a TermError if self is not an Application.

[src]

Returns a pair containing references to an application's underlying terms.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).unapp_ref(), Ok((&Var(1), &Var(2))));

Errors

Returns a TermError if self is not an Application.

[src]

Returns a pair containing mutable references to an application's underlying terms.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).unapp_mut(), Ok((&mut Var(1), &mut Var(2))));

Errors

Returns a TermError if self is not an Application.

[src]

Returns the left-hand side term of an application. Consumes self.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).lhs(), Ok(Var(1)));

Errors

Returns a TermError if self is not an Application.

[src]

Returns a reference to the left-hand side term of an application.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).lhs_ref(), Ok(&Var(1)));

Errors

Returns a TermError if self is not an Application.

[src]

Returns a mutable reference to the left-hand side term of an application.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).lhs_mut(), Ok(&mut Var(1)));

[src]

Returns the right-hand side term of an application. Consumes self.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).rhs(), Ok(Var(2)));

Errors

Returns a TermError if self is not an Application.

[src]

Returns a reference to the right-hand side term of an application.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).rhs_ref(), Ok(&Var(2)));

Errors

Returns a TermError if self is not an Application.

[src]

Returns a mutable reference to the right-hand side term of an application.

Example

use lambda_calculus::*;

assert_eq!(app(Var(1), Var(2)).rhs_mut(), Ok(&mut Var(2)));

Errors

Returns a TermError if self is not an Application.

[src]

Returns true if self is a supercombinator.

Example

use lambda_calculus::*;

let term1 = abs(app(Var(1), abs(Var(1)))); // λ 1 (λ 1)
let term2 = app(abs(Var(2)), abs(Var(1))); // (λ 2) (λ 1)

assert_eq!(term1.is_supercombinator(), true);
assert_eq!(term2.is_supercombinator(), false);

impl Term
[src]

[src]

Applies a Term to self via substitution and variable update.

Example

use lambda_calculus::*;

let mut term1  = parse(&"λλ42(λ13)", DeBruijn).unwrap();
let term2      = parse(&"λ51", DeBruijn).unwrap();
let result     = parse(&"λ3(λ61)(λ1(λ71))", DeBruijn).unwrap();

term1.apply(&term2);

assert_eq!(term1, result);

Errors

Returns a TermError if self is not an Abstraction.

[src]

Performs β-reduction on a Term with the specified evaluation Order and an optional limit on the number of reductions (0 means no limit) and returns the number of performed reductions.

Example

use lambda_calculus::*;

let mut expression = parse(&"(λa.λb.λc.b (a b c)) (λa.λb.b)", Classic).unwrap();
let reduced        = parse(&"λa.λb.a b", Classic).unwrap();

expression.reduce(NOR, 0);

assert_eq!(expression, reduced);

Trait Implementations

impl PartialEq for Term
[src]

[src]

This method tests for self and other values to be equal, and is used by ==. Read more

[src]

This method tests for !=.

impl Clone for Term
[src]

[src]

Returns a copy of the value. Read more

1.0.0
[src]

Performs copy-assignment from source. Read more

impl Hash for Term
[src]

[src]

Feeds this value into the given [Hasher]. Read more

1.3.0
[src]

Feeds a slice of this type into the given [Hasher]. Read more

impl Eq for Term
[src]

impl Display for Term
[src]

[src]

Formats the value using the given formatter. Read more

impl Debug for Term
[src]

[src]

Formats the value using the given formatter.