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:
extern crate moniker;
use Rc;
use ;
#
#
#
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 boundScope<P: BoundPattern<N>, T: BoundTerm<N>>
: bind the termT
using the patternP
Ignore<T>
: IgnoresT
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 equalityIgnore<T>
: IgnoresT
when comparing for alpha equalityEmbed<T: BoundTerm<N>>
: Embed a termT
in a patternNest<P: BoundPattern<N>>
: Multiple nested binding patternsRec<P: BoundPattern<N>>
: Recursively bind a pattern in itself
Implementations for tuples, strings, numbers, slices, vectors, and mart pointers are also provided for convenience.