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]

Applies self to another term without substitution or reduction.

Example

use lambda_calculus::term::*;

assert_eq!(Var(1).app(Var(2)), App(Box::new(Var(1)), Box::new(Var(2))));

Consumes a lambda variable and returns its De Bruijn index.

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not a Variable.

Returns a reference to a variable's index.

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not a Variable.

Returns a mutable reference to a variable's index.

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not a Variable.

Consumes an abstraction and returns its underlying term.

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Abstraction.

Returns a reference to an abstraction's underlying term.

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Abstraction.

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Abstraction.

Consumes an application and returns a pair containing its underlying terms.

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

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

Example

use lambda_calculus::term::*;

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

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

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

Example

use lambda_calculus::term::*;

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

Errors

The function will return an error if self is not an Application.

impl Term
[src]

Applies self to another Term and performs substitution, consuming self in the process.

Example

use lambda_calculus::parser::parse;
use lambda_calculus::term::Notation::DeBruijn;

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

assert_eq!(lhs.apply(&rhs), Ok(result));

Errors

The function will return an error if self is not an Abstraction.

Reduces an Application by substitution and variable update.

Example

use lambda_calculus::term::{app, abs};
use lambda_calculus::term::Term::Var;
use lambda_calculus::church::numerals::zero;
use lambda_calculus::combinators::i;

assert_eq!(app(i(), zero()).eval(), Ok(zero()));

Errors

The function will return an error if self is not an Application or if its left hand side term is not an Abstraction.

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

Example

use lambda_calculus::church::numerals::pred;
use lambda_calculus::reduction::Order::NOR;

let mut pred_one = pred().app(1.into());
pred_one.beta(NOR, 0, false);

assert_eq!(pred_one, 0.into());

impl Term
[src]

Returns the value of self if it's a Church-encoded number.

Example

use lambda_calculus::church::numerals::one;

assert_eq!(one().value(), Ok(1));

Errors

The function will return an error if self is not a Church number.

Checks whether self is a Church-encoded number.

Example

use lambda_calculus::church::numerals::one;

assert!(one().is_cnum());

impl Term
[src]

Checks whether self is a Church-encoded pair.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let pair01 = app!(pair(), zero(), one());

assert!(pair01.is_pair());

Splits a Church-encoded pair into a pair of terms, consuming self.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.unpair(), Ok((zero(), one())));

Errors

The function will return an error if self is not a Church pair.

Splits a Church-encoded pair into a pair of references to its underlying terms.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.unpair_ref(), Ok((&zero(), &one())));

Errors

The function will return an error if self is not a Church pair.

Splits a Church-encoded pair into a pair of mutable references to its underlying terms.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let mut pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.unpair_mut(), Ok((&mut zero(), &mut one())));

Errors

The function will return an error if self is not a Church pair.

Returns the first term from a Church-encoded pair, consuming self.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.fst(), Ok(zero()));

Errors

The function will return an error if self is not a Church pair.

Returns a reference to the first term of a Church-encoded pair.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.fst_ref(), Ok(&zero()));

Errors

The function will return an error if self is not a Church pair.

Returns a mutable reference to the first term of a Church-encoded pair. Returns a reference to the first term of a Church-encoded pair.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let mut pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.fst_mut(), Ok(&mut zero()));

Errors

The function will return an error if self is not a Church pair.

Returns the second term from a Church-encoded pair, consuming self.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.snd(), Ok(one()));

Errors

The function will return an error if self is not a Church pair.

Returns a reference to the second term of a Church-encoded pair.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.snd_ref(), Ok(&one()));

Errors

The function will return an error if self is not a Church pair.

Returns a mutable reference to the second term of a Church-encoded pair.

Example

use lambda_calculus::church::pairs::pair;
use lambda_calculus::church::numerals::{zero, one};

let mut pair01 = app!(pair(), zero(), one());

assert_eq!(pair01.snd_mut(), Ok(&mut one()));

Errors

The function will return an error if self is not a Church pair.

impl Term
[src]

Checks whether self is a empty Church list, i.e. nil().

Example

use lambda_calculus::church::lists::nil;

assert!(nil().is_empty());

Checks whether self is a Church list.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert!(list_110.is_list());

Splits a Church list into a pair containing its first term and a list of all the other terms, consuming self.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.uncons(), Ok((one(), Term::from(vec![one(), zero()]))));

Errors

The function will return an error if self is not a Church list.

Splits a Church list into a pair containing references to its first term and a to list of all the other terms.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.uncons_ref(), Ok((&one(), &Term::from(vec![one(), zero()]))));

Errors

The function will return an error if self is not a Church list.

Splits a Church list into a pair containing mutable references to its first term and a to list of all the other terms.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let mut list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.uncons_mut(),
           Ok((&mut one(), &mut Term::from(vec![one(), zero()]))));

Errors

The function will return an error if self is not a Church list.

Returns the first term from a Church list, consuming self.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.head(), Ok(one()));

Errors

The function will return an error if self is not a Church list.

Returns a reference to the first term of a Church list.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.head_ref(), Ok(&one()));

Errors

The function will return an error if self is not a Church list.

Returns a mutable reference to the first term of a Church list.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let mut list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.head_mut(), Ok(&mut one()));

Errors

The function will return an error if self is not a Church list.

Returns a list of all the terms of a Church list but the first one, consuming self.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.tail(), Ok(Term::from(vec![one(), zero()])));

Errors

The function will return an error if self is not a Church list.

Returns a reference to a list of all the terms of a Church list but the first one.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.tail_ref(), Ok(&Term::from(vec![one(), zero()])));

Errors

The function will return an error if self is not a Church list.

Returns a mutable reference to a list of all the terms of a Church list but the first one.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let mut list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.tail_mut(), Ok(&mut Term::from(vec![one(), zero()])));

Errors

The function will return an error if self is not a Church list.

Returns the length of a Church list

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.len(), Ok(3));

Errors

The function will return an error if self is not a Church list.

Adds a term to the beginning of a Church list and returns the new list. Consumes self and the argument.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.push(zero()), Ok(Term::from(vec![zero(), one(), one(), zero()])));

Errors

The function will return an error if self is not a Church list or a nil().

Removes the first element from a Church list and returns it.

Example

use lambda_calculus::term::Term;
use lambda_calculus::church::numerals::{zero, one};

let mut list_110 = Term::from(vec![one(), one(), zero()]);

assert_eq!(list_110.pop(), Ok(one()));
assert_eq!(list_110, Term::from(vec![one(), zero()]));
assert_eq!(list_110.pop(), Ok(one()));
assert_eq!(list_110, Term::from(vec![zero()]));
assert_eq!(list_110.pop(), Ok(zero()));
assert_eq!(list_110, Term::from(vec![]));

assert!(list_110.is_empty())

Errors

The function will return an error if self is not a Church list.

Trait Implementations

impl PartialEq for Term
[src]

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

This method tests for !=.

impl Clone for Term
[src]

Returns a copy of the value. Read more

Performs copy-assignment from source. Read more

impl Hash for Term
[src]

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

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

impl Eq for Term
[src]

impl Display for Term
[src]

Formats the value using the given formatter. Read more

impl Debug for Term
[src]

Formats the value using the given formatter.

impl From<usize> for Term
[src]

Performs the conversion.

impl From<bool> for Term
[src]

Performs the conversion.

impl From<(Term, Term)> for Term
[src]

Performs the conversion.

impl From<Vec<Term>> for Term
[src]

Performs the conversion.

impl Iterator for Term
[src]

The type of the elements being iterated over.

Advances the iterator and returns the next value. Read more

Returns the bounds on the remaining length of the iterator. Read more

Consumes the iterator, counting the number of iterations and returning it. Read more

Consumes the iterator, returning the last element. Read more

Returns the nth element of the iterator. Read more

🔬 This is a nightly-only experimental API. (iterator_step_by)

unstable replacement of Range::step_by

Creates an iterator starting at the same point, but stepping by the given amount at each iteration. Read more

Takes two iterators and creates a new iterator over both in sequence. Read more

'Zips up' two iterators into a single iterator of pairs. Read more

Takes a closure and creates an iterator which calls that closure on each element. Read more

Creates an iterator which uses a closure to determine if an element should be yielded. Read more

Creates an iterator that both filters and maps. Read more

Creates an iterator which gives the current iteration count as well as the next value. Read more

Creates an iterator which can use peek to look at the next element of the iterator without consuming it. Read more

Creates an iterator that [skip]s elements based on a predicate. Read more

Creates an iterator that yields elements based on a predicate. Read more

Creates an iterator that skips the first n elements. Read more

Creates an iterator that yields its first n elements. Read more

An iterator adaptor similar to [fold] that holds internal state and produces a new iterator. Read more

Creates an iterator that works like map, but flattens nested structure. Read more

Creates an iterator which ends after the first [None]. Read more

Do something with each element of an iterator, passing the value on. Read more

Borrows an iterator, rather than consuming it. Read more

Transforms an iterator into a collection. Read more

Consumes an iterator, creating two collections from it. Read more

An iterator adaptor that applies a function, producing a single, final value. Read more

Tests if every element of the iterator matches a predicate. Read more

Tests if any element of the iterator matches a predicate. Read more

Searches for an element of an iterator that satisfies a predicate. Read more

Searches for an element in an iterator, returning its index. Read more

Searches for an element in an iterator from the right, returning its index. Read more

Returns the maximum element of an iterator. Read more

Returns the minimum element of an iterator. Read more

Returns the element that gives the maximum value from the specified function. Read more

Returns the element that gives the maximum value with respect to the specified comparison function. Read more

Returns the element that gives the minimum value from the specified function. Read more

Returns the element that gives the minimum value with respect to the specified comparison function. Read more

Reverses an iterator's direction. Read more

Converts an iterator of pairs into a pair of containers. Read more

Creates an iterator which [clone]s all of its elements. Read more

Repeats an iterator endlessly. Read more

Sums the elements of an iterator. Read more

Iterates over the entire iterator, multiplying all the elements Read more

Lexicographically compares the elements of this Iterator with those of another. Read more

Lexicographically compares the elements of this Iterator with those of another. Read more

Determines if the elements of this Iterator are equal to those of another. Read more

Determines if the elements of this Iterator are unequal to those of another. Read more

Determines if the elements of this Iterator are lexicographically less than those of another. Read more

Determines if the elements of this Iterator are lexicographically less or equal to those of another. Read more

Determines if the elements of this Iterator are lexicographically greater than those of another. Read more

Determines if the elements of this Iterator are lexicographically greater than or equal to those of another. Read more

impl Index<usize> for Term
[src]

The returned type after indexing

The method for the indexing (container[index]) operation