1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120

//! 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][stlc]:
//!
//! ```rust
//! #[macro_use]
//! extern crate moniker;
//!
//! use std::rc::Rc;
//! use moniker::{Embed, Nest, Binder, Scope, Var};
//!
//! # #[cfg(feature = "moniker-derive")]
//! #[derive(Debug, Clone, BoundTerm)]
//! pub enum Type {
//!     Base,
//!     Arrow(Rc<Type>, Rc<Type>),
//! }
//!
//! # #[cfg(feature = "moniker-derive")]
//! #[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>),
//! }
//! # fn main() {}
//! ```
//!
//! [stlc]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
//!
//! # 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.
//!
//! [`BoundTerm`]: trait.BoundTerm.html
//! [`Var<N>`]: enum.Var.html
//! [`Scope<P: BoundPattern<N>, T: BoundTerm<N>>`]: struct.Scope.html
//!
//! ## 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.
//!
//! [`BoundPattern`]: trait.BoundPattern.html
//! [`Binder<N>`]: enum.Binder.html
//! [`Ignore<T>`]: struct.Ignore.html
//! [`Embed<T: BoundTerm<N>>`]: struct.Embed.html
//! [`Nest<P: BoundPattern<N>>`]: struct.Nest.html
//! [`Rec<P: BoundPattern<N>>`]: struct.Rec.html

#[macro_use]
extern crate lazy_static;
#[cfg(feature = "moniker-derive")]
#[allow(unused_imports)]
#[macro_use]
extern crate moniker_derive;

// Optional impls
#[cfg(feature = "codespan")]
extern crate codespan;
#[cfg(feature = "im")]
extern crate im;
#[cfg(feature = "num-bigint")]
extern crate num_bigint;

#[cfg(feature = "moniker-derive")]
#[doc(hidden)]
pub use moniker_derive::*;

#[macro_use]
#[doc(hidden)]
pub mod macros;

mod binder;
mod bound;
mod bound_var;
mod embed;
mod free_var;
mod ignore;
mod nest;
mod rec;
mod scope;
mod unique_id;
mod var;

pub use self::binder::Binder;
pub use self::bound::{BoundPattern, BoundTerm, OnBoundFn, OnFreeFn, ScopeState};
pub use self::bound_var::{BinderIndex, BoundVar, ScopeOffset};
pub use self::embed::Embed;
pub use self::free_var::FreeVar;
pub use self::ignore::Ignore;
pub use self::nest::Nest;
pub use self::rec::Rec;
pub use self::scope::Scope;
pub use self::unique_id::UniqueId;
pub use self::var::Var;