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 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
//! [Lambda-encoded option](https://en.wikipedia.org/wiki/Option_type)
use crate::combinators::I;
use crate::data::boolean::{fls, tru};
use crate::term::Term::*;
use crate::term::{abs, app, Term};
/// Produces a lambda-encoded empty option; equivalent to `boolean::tru`.
///
/// NONE ≡ λns.n ≡ λ λ 2 ≡ TRUE
pub fn none() -> Term {
tru()
}
/// Applied to an argument it consumes it and produces a lambda-encoded option that contains it.
///
/// SOME ≡ λans.s a ≡ λ λ λ 1 3
///
/// # Example
/// ```
/// use lambda_calculus::data::option::some;
/// use lambda_calculus::*;
///
/// assert_eq!(beta(app(some(), 1.into_church()), NOR, 0), Some(1).into_church());
/// ```
pub fn some() -> Term {
abs!(3, app(Var(1), Var(3)))
}
/// Applied to a lambda-encoded option it produces a lambda-encoded boolean indicating whether it
/// is empty.
///
/// IS_NONE ≡ λa.a TRUE (λx.FALSE) ≡ λ 1 TRUE (λ FALSE)
///
/// # Example
/// ```
/// use lambda_calculus::data::option::{is_none, none};
/// use lambda_calculus::*;
///
/// assert_eq!(beta(app(is_none(), none()), NOR, 0), true.into());
/// assert_eq!(beta(app(is_none(), Some(1).into_church()), NOR, 0), false.into());
/// ```
pub fn is_none() -> Term {
abs(app!(Var(1), tru(), abs(fls())))
}
/// Applied to a lambda-encoded option it produces a lambda-encoded boolean indicating whether it
/// is not empty.
///
/// IS_SOME ≡ λa.a FALSE (λx.TRUE) ≡ λ 1 FALSE (λ TRUE)
///
/// # Example
/// ```
/// use lambda_calculus::data::option::{is_some, none};
/// use lambda_calculus::*;
///
/// assert_eq!(beta(app(is_some(), none()), NOR, 0), false.into());
/// assert_eq!(beta(app(is_some(), Some(2).into_church()), NOR, 0), true.into());
/// ```
pub fn is_some() -> Term {
abs(app!(Var(1), fls(), abs(tru())))
}
/// Applied to a function and a lambda-encoded option it applies the function to the contents of
/// the option, returning the empty option if the option does not contain a value.
///
/// MAP ≡ λfm.m NONE (λx.SOME (f x)) ≡ λ λ 1 NONE (λ SOME (3 1))
///
/// # Example
/// ```
/// use lambda_calculus::data::option::{map, none};
/// use lambda_calculus::data::num::church::succ;
/// use lambda_calculus::*;
///
/// let some_one: Term = Some(1).into_church();
///
/// assert_eq!(beta(app!(map(), succ(), some_one), NOR, 0), Some(2).into_church());
/// assert_eq!(beta(app!(map(), succ(), none()), NOR, 0), none());
/// ```
pub fn map() -> Term {
abs!(
2,
app!(Var(1), none(), abs(app(some(), app(Var(3), Var(1)))))
)
}
/// Applied to two arguments and a lambda-encoded option it returns the second argument applied to
/// the contents of the option if it contains a value or the first argument if it doesn't.
///
/// MAP_OR ≡ λdfm.m d f ≡ λ λ λ 1 3 2
///
/// # Example
/// ```
/// use lambda_calculus::data::option::{map_or, none};
/// use lambda_calculus::data::num::church::succ;
/// use lambda_calculus::*;
///
/// let some_one: Term = Some(1).into_church();
///
/// assert_eq!(beta(app!(map_or(), 0.into_church(), succ(), some_one), NOR, 0), 2.into_church());
/// assert_eq!(beta(app!(map_or(), 0.into_church(), succ(), none()), NOR, 0), 0.into_church());
/// ```
pub fn map_or() -> Term {
abs!(3, app!(Var(1), Var(3), Var(2)))
}
/// Applied to one argument and a lambda-encoded option it returns the value inside the option or
/// the first argument if the option doesn't contain a value.
///
/// UNWRAP_OR ≡ λdm.m d I ≡ λ λ 1 2 I
///
/// # Example
/// ```
/// use lambda_calculus::data::option::{unwrap_or, none};
/// use lambda_calculus::*;
///
/// let some_one: Term = Some(1).into_church();
///
/// assert_eq!(beta(app!(unwrap_or(), 2.into_church(), some_one), NOR, 0), 1.into_church());
/// assert_eq!(beta(app!(unwrap_or(), 2.into_church(), none()), NOR, 0), 2.into_church());
/// ```
pub fn unwrap_or() -> Term {
abs!(2, app!(Var(1), Var(2), I()))
}
/// Applied to a lambda-encoded option and a function that returns a lambda-encoded option, it
/// applies the function to the contents of the option.
///
/// AND_THEN ≡ λmf.m NONE f ≡ λ λ 2 NONE 1
///
/// # Example
/// ```
/// use lambda_calculus::data::option::{and_then, some, none};
/// use lambda_calculus::data::num::church::succ;
/// use lambda_calculus::*;
///
/// // Equivalent to the closure `|x| { Some(x+1) }` in Rust
/// let some_succ: Term = abs(app(some(), app(succ(), Var(1))));
///
/// assert_eq!(beta(app!(and_then(), none(), some_succ.clone()), NOR, 0), none());
/// assert_eq!(beta(
/// app!(and_then(), Some(1).into_church(), some_succ.clone()), NOR, 0),
/// Some(2).into_church()
/// );
/// ```
pub fn and_then() -> Term {
abs!(2, app!(Var(2), none(), Var(1)))
}
impl From<Option<Term>> for Term {
fn from(option: Option<Term>) -> Term {
match option {
None => none(),
Some(value) => abs!(2, app(Var(1), value)),
}
}
}