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
121
122

//! [Lambda-encoded pair](https://en.wikipedia.org/wiki/Church_encoding#Church_pairs)

use crate::data::boolean::{fls, tru};
use crate::term::Term::*;
use crate::term::{abs, app, Term};

/// Applied to two `Term`s it contains them in a lambda-encoded pair.
///
/// PAIR ≡ λxyz.z x y ≡ λ λ λ 1 3 2
///
/// # Example
/// ```
/// use lambda_calculus::data::pair::pair;
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app!(pair(), 1.into_church(), 2.into_church()), NOR, 0),
///     (1, 2).into_church()
/// );
/// ```
pub fn pair() -> Term {
    abs!(3, app!(Var(1), Var(3), Var(2)))
}

/// Applied to a lambda-encoded pair `(a, b)` it yields `a`.
///
/// FST ≡ λp.p TRUE ≡ λ 1 TRUE
///
/// # Example
/// ```
/// use lambda_calculus::data::pair::fst;
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app(fst(), (1, 2).into_church()), NOR, 0),
///     1.into_church()
/// );
/// ```
pub fn fst() -> Term {
    abs(app(Var(1), tru()))
}

/// Applied to a lambda-encoded pair `(a, b)` it yields `b`.
///
/// SND ≡ λp.p FALSE ≡ λ 1 FALSE
///
/// # Example
/// ```
/// use lambda_calculus::data::pair::snd;
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app(snd(), (1, 2).into_church()), NOR, 0),
///     2.into_church()
/// );
/// ```
pub fn snd() -> Term {
    abs(app(Var(1), fls()))
}

/// Applied to a function and a lambda-encoded pair `(a, b)` it uncurries it
/// and applies the function to `a` and then `b`.
///
/// UNCURRY ≡ λfp.f (FST p) (SND p) ≡ λ λ 2 (FST 1) (SND 1)
///
/// # Example
/// ```
/// use lambda_calculus::data::pair::uncurry;
/// use lambda_calculus::data::num::church::add;
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app!(uncurry(), add(), (1, 2).into_church()), NOR, 0),
///     3.into_church()
/// );
/// ```
pub fn uncurry() -> Term {
    abs!(2, app!(Var(2), app(fst(), Var(1)), app(snd(), Var(1))))
}

/// Applied to a function and two arguments `a` and `b`, it applies the function to the
/// lambda-encoded pair `(a, b)`.
///
/// CURRY ≡ λfab.f (PAIR a b) ≡ λ λ λ 3 (PAIR 2 1)
///
/// # Example
/// ```
/// use lambda_calculus::data::pair::{fst, curry};
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app!(curry(), fst(), 1.into_church(), 2.into_church()), NOR, 0),
///     1.into_church()
/// );
/// ```
pub fn curry() -> Term {
    abs!(3, app(Var(3), app!(pair(), Var(2), Var(1))))
}

/// Applied to a lambda-encoded pair `(a, b)` it swaps its elements so that it becomes `(b, a)`.
///
/// SWAP ≡ λp.PAIR (SND p) (FST p) ≡ λ PAIR (SND 1) (FST 1)
///
/// # Example
/// ```
/// use lambda_calculus::data::pair::swap;
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app!(swap(), (1, 2).into_church()), NOR, 0),
///     (2, 1).into_church()
/// );
/// ```
pub fn swap() -> Term {
    abs(app!(pair(), app(snd(), Var(1)), app(fst(), Var(1))))
}

impl From<(Term, Term)> for Term {
    fn from((a, b): (Term, Term)) -> Term {
        abs(app!(Var(1), a, b))
    }
}