lambda_calculus/data/
tuple.rs

1//! [Lambda-encoded `n`-tuple](https://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf)
2//!
3//! This module contains the `tuple` and `pi` macros.
4
5/// A macro for creating lambda-encoded tuples.
6///
7/// # Example
8/// ```
9/// # #[macro_use] extern crate lambda_calculus;
10/// # fn main() {
11/// use lambda_calculus::term::*;
12/// use lambda_calculus::*;
13///
14/// assert_eq!(
15///     tuple!(1.into_church(), 2.into_church()),
16///     abs(app!(Var(1), 1.into_church(), 2.into_church()))
17/// );
18///
19/// assert_eq!(
20///     tuple!(1.into_church(), 2.into_church(), 3.into_church()),
21///     abs(app!(Var(1), 1.into_church(), 2.into_church(), 3.into_church()))
22/// );
23/// # }
24/// ```
25#[macro_export]
26macro_rules! tuple {
27    ($first:expr, $($next:expr),+) => {
28        {
29            let mut ret = app(Var(1), $first);
30            $(ret = app(ret, $next);)*
31            abs(ret)
32        }
33    };
34}
35
36/// A macro for obtaining a projection function (`π`) providing the `i`-th (one-indexed) element of
37/// a lambda-encoded `n`-tuple.
38///
39/// # Example
40/// ```
41/// # #[macro_use] extern crate lambda_calculus;
42/// # fn main() {
43/// use lambda_calculus::term::*;
44/// use lambda_calculus::*;
45///
46/// let t2 = || tuple!(1.into_church(), 2.into_church());
47///
48/// assert_eq!(beta(app(pi!(1, 2), t2()), NOR, 0), 1.into_church());
49/// assert_eq!(beta(app(pi!(2, 2), t2()), NOR, 0), 2.into_church());
50///
51/// let t3 = || tuple!(1.into_church(), 2.into_church(), 3.into_church());
52///
53/// assert_eq!(beta(app(pi!(1, 3), t3()), NOR, 0), 1.into_church());
54/// assert_eq!(beta(app(pi!(2, 3), t3()), NOR, 0), 2.into_church());
55/// assert_eq!(beta(app(pi!(3, 3), t3()), NOR, 0), 3.into_church());
56/// # }
57/// ```
58#[macro_export]
59macro_rules! pi {
60    ($i:expr, $n:expr) => {{
61        let mut ret = Var($n + 1 - $i);
62
63        for _ in 0..$n {
64            ret = abs(ret);
65        }
66
67        abs(app(Var(1), ret))
68    }};
69}
lambda_calculus/data/tuple.rs

lambda_calculus/data/
tuple.rs
