[−][src]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 ( |
app | An application ( |
var | A variable ( |
variable | A raw |
γ | 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 | A reduction strategy for an |