<commit_before>//! [Single-pair list](https://en.wikipedia.org/wiki/Church_encoding#One_pair_as_a_list_node)

use term::{Term, abs, app};
use term::Term::*;
use data::boolean::{tru, fls};
use data::pair::{pair, fst, snd};
use combinators::{I, Z};
use data::num::church::{zero, is_zero, succ, pred};

/// Produces a `nil`, the last link of a pair-encoded list; equivalent to `boolean::fls`.
///
/// NIL ≡ λab.b ≡ λ λ 1 ≡ FALSE
pub fn nil() -> Term { fls() }

/// Applied to a pair-encoded list it determines if it is empty.
///
/// IS_NIL ≡ λl.l (λhtd.FALSE) TRUE ≡ λ 1 (λ λ λ FALSE) TRUE
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::is_nil;
/// use lambda_calculus::*;
///
/// assert_eq!(beta(app(is_nil(),                vec![].into_pair_list()), NOR, 0),  true.into());
/// assert_eq!(beta(app(is_nil(), vec![1.into_church()].into_pair_list()), NOR, 0), false.into());
/// ```
pub fn is_nil() -> Term {
    abs(app!(Var(1), abs!(3, fls()), tru()))
}

/// Applied to two terms it returns them contained in a pair-encoded list; equivalent to `pair::pair`.
///
/// CONS ≡ λxyz.z x y ≡ λ λ λ 1 3 2 ≡ PAIR
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::{nil, cons};
/// use lambda_calculus::*;
///
/// let list_consed =
///     app!(
///         cons(),
///         1.into_church(),
///         app!(
///             cons(),
///             2.into_church(),
///             app!(
///                 cons(),
///                 3.into_church(),
///                 nil()
///             )
///         )
///     );
///
/// let list_from_vec = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
///
/// assert_eq!(beta(list_consed, NOR, 0), list_from_vec);
/// ```
pub fn cons() -> Term { pair() }

/// Applied to a pair-encoded list it returns its first element; equivalent to `pair::fst`.
///
/// HEAD ≡ λp.p TRUE ≡ λ 1 TRUE ≡ FST
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::head;
/// use lambda_calculus::*;
///
/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
///
/// assert_eq!(beta(app(head(), list), NOR, 0), 1.into_church());
/// ```
pub fn head() -> Term { fst() }

/// Applied to a pair-encoded list it returns a new list with all its elements but the first one;
/// equivalent to `pair::snd`.
///
/// TAIL ≡ λp.p FALSE ≡ λ 1 FALSE ≡ SND
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::tail;
/// use lambda_calculus::*;
///
/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
///
/// assert_eq!(
///     beta(app(tail(), list), NOR, 0),
///     vec![2.into_church(), 3.into_church()].into_pair_list()
/// );
/// ```
pub fn tail() -> Term { snd() }

/// Applied to a pair-encoded list and a Church-encoded number it returns its Church-encoded length.
///
/// LENGTH ≡ Z (λzal.IS_NIL l (λx.a) (λx.z (SUCC a) (TAIL l)) I) ZERO
///        ≡ Z (λλλ IS_NIL 1 (λ 3) (λ 4 (SUCC 3) (TAIL 2)) I) ZERO
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::{length, nil};
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app(length(), nil()), NOR, 0),
///     0.into_church()
/// );
/// ```
pub fn length() -> Term {
    app!(
        Z(),
        abs!(3, app!(
            is_nil(),
            Var(1),
            abs(Var(3)),
            abs(app!(
                Var(4),
                app(succ(), Var(3)),
                app(tail(), Var(2))
            )),
            I()<commit_msg>update documentation for pair list length<commit_after>//! [Single-pair list](https://en.wikipedia.org/wiki/Church_encoding#One_pair_as_a_list_node)

use term::{Term, abs, app};
use term::Term::*;
use data::boolean::{tru, fls};
use data::pair::{pair, fst, snd};
use combinators::{I, Z};
use data::num::church::{zero, is_zero, succ, pred};

/// Produces a `nil`, the last link of a pair-encoded list; equivalent to `boolean::fls`.
///
/// NIL ≡ λab.b ≡ λ λ 1 ≡ FALSE
pub fn nil() -> Term { fls() }

/// Applied to a pair-encoded list it determines if it is empty.
///
/// IS_NIL ≡ λl.l (λhtd.FALSE) TRUE ≡ λ 1 (λ λ λ FALSE) TRUE
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::is_nil;
/// use lambda_calculus::*;
///
/// assert_eq!(beta(app(is_nil(),                vec![].into_pair_list()), NOR, 0),  true.into());
/// assert_eq!(beta(app(is_nil(), vec![1.into_church()].into_pair_list()), NOR, 0), false.into());
/// ```
pub fn is_nil() -> Term {
    abs(app!(Var(1), abs!(3, fls()), tru()))
}

/// Applied to two terms it returns them contained in a pair-encoded list; equivalent to `pair::pair`.
///
/// CONS ≡ λxyz.z x y ≡ λ λ λ 1 3 2 ≡ PAIR
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::{nil, cons};
/// use lambda_calculus::*;
///
/// let list_consed =
///     app!(
///         cons(),
///         1.into_church(),
///         app!(
///             cons(),
///             2.into_church(),
///             app!(
///                 cons(),
///                 3.into_church(),
///                 nil()
///             )
///         )
///     );
///
/// let list_from_vec = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
///
/// assert_eq!(beta(list_consed, NOR, 0), list_from_vec);
/// ```
pub fn cons() -> Term { pair() }

/// Applied to a pair-encoded list it returns its first element; equivalent to `pair::fst`.
///
/// HEAD ≡ λp.p TRUE ≡ λ 1 TRUE ≡ FST
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::head;
/// use lambda_calculus::*;
///
/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
///
/// assert_eq!(beta(app(head(), list), NOR, 0), 1.into_church());
/// ```
pub fn head() -> Term { fst() }

/// Applied to a pair-encoded list it returns a new list with all its elements but the first one;
/// equivalent to `pair::snd`.
///
/// TAIL ≡ λp.p FALSE ≡ λ 1 FALSE ≡ SND
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::tail;
/// use lambda_calculus::*;
///
/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
///
/// assert_eq!(
///     beta(app(tail(), list), NOR, 0),
///     vec![2.into_church(), 3.into_church()].into_pair_list()
/// );
/// ```
pub fn tail() -> Term { snd() }

/// Applied to a pair-encoded list it returns its Church-encoded length.
///
/// LENGTH ≡ Z (λzal.IS_NIL l (λx.a) (λx.z (SUCC a) (TAIL l)) I) ZERO
///        ≡ Z (λλλ IS_NIL 1 (λ 3) (λ 4 (SUCC 3) (TAIL 2)) I) ZERO
///
/// # Example
/// ```
/// use lambda_calculus::data::list::pair::{length, nil};
/// use lambda_calculus::*;
///
/// assert_eq!(
///     beta(app(length(), nil()), NOR, 0),
///     0.into_church()
/// );
/// ```
pub fn length() -> Term {
    app!(
        Z(),
        abs!(3, app!(
            is_nil(),
            Var(1),
            abs(Var(3)),
            abs(app!(
                Var(4),
                app(succ(), Var(3)),
                app(tail(), Var(2))
            )),
            I()
{'fraction_non_alphanumeric': 0.24022266628604053, 'fraction_numerical': 0.012275192691978304, 'mean_word_length': 2.1577287066246056, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 15, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7019817', 'n_tokens_mistral': 2608, 'n_tokens_neox': 2461, 'n_words': 654}