Crate lalrpop_lambda

This project started as just the parse.lalrpop and AST, but grew into a bit more.

Evaluation of λ-expressions is currently done in a single big-step semantics Expression::normalize function. The reduction strategy is so far only configurable by η.

See the impl From items under Expression. These define conversions between Rust and λ-expressions. These are all defined in mod encode.

#![feature(box_syntax)]

#[macro_use]
extern crate lalrpop_lambda;

use lalrpop_lambda::Strategy;

fn main() {
    use lalrpop_lambda::Expression;
    use lalrpop_lambda::parse::ExpressionParser;

    // Define an expression parser, for shortest lambda term strings.
    let parser = ExpressionParser::new();

    // The successor Church numeral function.
    let add1 = parser.parse("λn.λf.λx.f (n f x)").unwrap();

    // The first two church numerals.
    let zero = Expression::from(0u64);
    let one = app!({add1},{zero})
        .normalize(&Strategy::Applicative(false));
    assert_eq!(Expression::from(1u64), one);

    // Use a parsed identity function with other `Experssion`s.
    let id = parser.parse("λx.x").unwrap();
    let id_one = id(Expression::from(1u64))
        .normalize(&Strategy::Applicative(false));
    assert_eq!(one, id_one);
}

Modules

parse	Parse λ-expressions
wasm	WASM types for use in JS.

Macros

abs	An abstraction (Abs) expression
app	An application (App) expression
var	A variable (Var) expression
variable	A raw Variable
γ	Theory is nothing without application
λ	The all-powerful λ

Structs

Abstraction	An abstraction over a bound variable
Application	An application of two expressions
Variable	A potentially free variable

Enums

Expression	A mutually recursive definition for all lambda expressions
Strategy