Crate moniker[−][src]

Automatically derive variable binding and alpha equivalence for abstract syntax trees.

Example

Here is an example of how you might use moniker to define the AST for the simply typed lambda calculus:

#[macro_use]
extern crate moniker;

use std::rc::Rc;
use moniker::{Embed, Nest, Binder, Scope, Var};

#[derive(Debug, Clone, BoundTerm)]
pub enum Type {
    Base,
    Arrow(Rc<Type>, Rc<Type>),
}

#[derive(Debug, Clone, BoundTerm)]
pub enum Expr {
    Var(Var<String>),
    Lam(Scope<(Binder<String>, Embed<Rc<Type>>), Rc<Expr>>),
    Let(Scope<Nest<(Binder<String>, Embed<(Rc<Type>, Rc<Expr>)>)>, Rc<Expr>>),
    App(Rc<Expr>, Rc<Expr>),
}

Overview of traits and data types

We separate data types into terms and patterns:

Terms

Terms are data types that implement the BoundTerm trait.

Var<N>: A variable that is either free or bound
Scope<P: BoundPattern<N>, T: BoundTerm<N>>: bind the term T using the pattern P

Implementations for tuples, strings, numbers, slices, vectors, and mart pointers are also provided for convenience.

Patterns

Patterns are data types that implement the BoundPattern trait.

Binder<N>: Captures a free variables within a term, but is ignored for alpha equality
Ignore<T>: Ignores T when comparing for alpha equality
Embed<T: BoundTerm<N>>: Embed a term T in a pattern
Nest<P: BoundPattern<N>>: Multiple nested binding patterns
Rec<P: BoundPattern<N>>: Recursively bind a pattern in itself

Implementations for tuples, strings, numbers, slices, vectors, and mart pointers are also provided for convenience.

Macros

assert_pattern_eq	Assert that two expressions are alpha equivalent to each other (using `BoundPattern::pattern_eq`).
assert_term_eq	Assert that two expressions are alpha equivalent to each other (using `BoundTerm::term_eq`).

Structs

Binder
BinderIndex
BinderOffset
Embed	Embed a term in a pattern
GenId	A generated id
Ignore	Data that does not participate in name binding
Nest	Nested binding patterns
Rec	Recursively bind a pattern in itself
Scope	A bound scope
ScopeOffset	The Debruijn index of the binder that introduced the variable
ScopeState

Enums

FreeVar	A free variable
Var	A variable that can either be free or bound

Traits

BoundPattern	Patterns that bind variables in terms
BoundTerm	Terms that may contain variables that can be bound by patterns

Type Definitions

Permutations