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))
}
}