Crate moniker

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
• Ignore<T>: Ignores T when comparing for alpha equality

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

BoundVar

Embed

Embed a term in a pattern

FreeVar

A free variable

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

UniqueId

A generated id

Enums

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

OnBoundFn

OnFreeFn