lambda_calculus 3.6.1

//! [β-reduction](https://en.wikipedia.org/wiki/Beta_normal_form) for lambda `Term`s

pub use self::Order::*;
use crate::term::Term::*;
use crate::term::{Term, TermError};
use std::{cmp, fmt, mem};

/// The [evaluation order](http://www.cs.cornell.edu/courses/cs6110/2014sp/Handouts/Sestoft.pdf) of
/// β-reductions.
///
/// - the `NOR`, `HNO`, `APP` and `HAP` orders reduce expressions to their normal form
/// - the `APP` order will fail to fully reduce expressions containing terms without a normal form,
///   e.g. the `Y` combinator (they will expand forever)
/// - the `CBN` order reduces to weak head normal form
/// - the `CBV` order reduces to weak normal form
/// - the `HSP` order reduces to head normal form
#[derive(Debug, PartialEq, Eq, Clone, Copy)]
pub enum Order {
    /// normal - leftmost outermost; the most popular reduction strategy
    NOR,
    /// call-by-name - leftmost outermost, no reductions inside abstractions
    CBN,
    /// head spine - leftmost outermost, abstractions reduced only in head position
    HSP,
    /// hybrid normal - a mix between `HSP` (head spine) and `NOR` (normal) strategies
    HNO,
    /// applicative - leftmost innermost; the most eager strategy; unfit for recursion combinators
    APP,
    /// call-by-value - leftmost innermost, no reductions inside abstractions
    CBV,
    /// hybrid applicative - a mix between `CBV` (call-by-value) and `APP` (applicative) strategies;
    /// usually the fastest-reducing normalizing strategy
    HAP,
}

/// Performs η-reduction on a `Term` with an optional limit on the number of reductions (`0` means
/// no limit) and returns the reduced `Term`.
///
/// η-reduction removes a redundant abstraction wrapping an application of the bound variable:
/// `λx. M x → M` when `x` is not free in `M`.
///
/// # Example
///
/// ```
/// use lambda_calculus::*;
///
/// let expr    = parse(&"λa.λb. a b", Classic).unwrap();
/// let reduced = parse(&"λa.a", Classic).unwrap();
///
/// assert_eq!(eta(expr, 0), reduced);
/// ```
pub fn eta(mut term: Term, limit: usize) -> Term {
    term.eta(limit);
    term
}

/// Performs β-reduction on a `Term` with the specified evaluation `Order` and an optional limit on
/// the number of reductions (`0` means no limit) and returns the reduced `Term`.
///
/// # Example
///
/// ```
/// use lambda_calculus::*;
///
/// let expr    = parse(&"(λa.λb.λc.a (λd.λe.e (d b)) (λd.c) (λd.d)) (λa.λb.a b)", Classic).unwrap();
/// let reduced = parse(&"λa.λb.b", Classic).unwrap();
///
/// assert_eq!(beta(expr, NOR, 0), reduced);
/// ```
pub fn beta(mut term: Term, order: Order, limit: usize) -> Term {
    term.reduce(order, limit);
    term
}

impl Term {
    /// Applies a `Term` to `self` via substitution and variable update.
    ///
    /// # Example
    /// ```
    /// use lambda_calculus::*;
    ///
    /// let mut term1  = parse(&"λλ42(λ13)", DeBruijn).unwrap();
    /// let term2      = parse(&"λ51", DeBruijn).unwrap();
    /// let result     = parse(&"λ3(λ61)(λ1(λ71))", DeBruijn).unwrap();
    ///
    /// term1.apply(&term2);
    ///
    /// assert_eq!(term1, result);
    /// ```
    /// # Errors
    ///
    /// Returns a `TermError` if `self` is not an `Abs`traction.
    pub fn apply(&mut self, rhs: &Term) -> Result<(), TermError> {
        self.unabs_ref()?;

        self._apply(rhs, 0);

        let ret = mem::replace(self, Var(0)); // replace self with a dummy
        *self = ret.unabs().unwrap(); // move unabstracted self back to its place

        Ok(())
    }

    fn _apply(&mut self, rhs: &Term, depth: usize) {
        match self {
            Var(i) => match (*i).cmp(&depth) {
                cmp::Ordering::Equal => {
                    rhs.clone_into(self); // substitute a top-level variable from lhs with rhs
                    self.update_free_variables(depth - 1, 0); // update indices of free variables from rhs
                }
                cmp::Ordering::Greater => {
                    *self = Var(*i - 1); // decrement a free variable's index
                }
                _ => {}
            },
            Abs(t) => t._apply(rhs, depth + 1),
            App(boxed) => {
                boxed.0._apply(rhs, depth);
                boxed.1._apply(rhs, depth);
            }
        }
    }

    fn update_free_variables(&mut self, added_depth: usize, own_depth: usize) {
        // Every branch below amounts to `*i += added_depth`, so with nothing to
        // add the traversal cannot change the term. Worth checking, because the
        // common case reaches here with `added_depth == 0`: `apply` enters the
        // abstraction body at depth 1, so substituting the variable that lambda
        // binds passes `depth - 1 == 0` — and the walk would cover a subtree
        // that was just deep-cloned.
        if added_depth == 0 {
            return;
        }
        match self {
            Var(i) => {
                if *i > own_depth {
                    *i += added_depth
                }
            }
            Abs(t) => t.update_free_variables(added_depth, own_depth + 1),
            App(boxed) => {
                boxed.0.update_free_variables(added_depth, own_depth);
                boxed.1.update_free_variables(added_depth, own_depth);
            }
        }
    }

    fn eval(&mut self, count: &mut usize) {
        let to_apply = mem::replace(self, Var(0)); // replace self with a dummy
        let (mut lhs, rhs) = to_apply.unapp().unwrap(); // safe; only called in reduction sites
        lhs.apply_owned(rhs); // ditto
        *self = lhs; // move self back to its place

        *count += 1;
    }

    /// `apply`, but consuming the argument.
    ///
    /// Substitution copies the argument into every occurrence of the bound
    /// variable. When the argument is owned, the *last* of those occurrences can
    /// take it rather than clone it — and since a variable used exactly once is
    /// the common case, that usually removes the copy altogether. Reduction sites
    /// always own the argument and drop it immediately afterwards, so cloning
    /// there meant paying for a full deep copy *and* a full deep drop of the
    /// same tree.
    ///
    /// Finding the last occurrence costs one allocation-free pass over the body,
    /// which `_apply` was going to walk anyway.
    fn apply_owned(&mut self, rhs: Term) {
        debug_assert!(self.unabs_ref().is_ok());

        let mut remaining = self.count_occurrences(0);
        if remaining == 0 {
            // The argument is discarded, but free variables in the body still
            // need their indices decremented.
            drop(rhs);
            self._apply_owned(&mut None, 0, &mut 0);
        } else {
            self._apply_owned(&mut Some(rhs), 0, &mut remaining);
        }

        let ret = mem::replace(self, Var(0)); // replace self with a dummy
        *self = ret.unabs().unwrap(); // move unabstracted self back to its place
    }

    /// How many times the variable bound at `depth` occurs, mirroring the
    /// traversal `_apply_owned` performs.
    fn count_occurrences(&self, depth: usize) -> usize {
        match self {
            Var(i) => (*i == depth) as usize,
            Abs(t) => t.count_occurrences(depth + 1),
            App(boxed) => boxed.0.count_occurrences(depth) + boxed.1.count_occurrences(depth),
        }
    }

    fn _apply_owned(&mut self, rhs: &mut Option<Term>, depth: usize, remaining: &mut usize) {
        match self {
            Var(i) => match (*i).cmp(&depth) {
                cmp::Ordering::Equal => {
                    *remaining -= 1;
                    if *remaining == 0 {
                        // Last occurrence: hand the argument over instead of copying it.
                        *self = rhs.take().expect("occurrence count is exact");
                    } else {
                        rhs.as_ref().expect("occurrences remain").clone_into(self);
                    }
                    self.update_free_variables(depth - 1, 0); // update indices of free variables from rhs
                }
                cmp::Ordering::Greater => {
                    *self = Var(*i - 1); // decrement a free variable's index
                }
                _ => {}
            },
            Abs(t) => t._apply_owned(rhs, depth + 1, remaining),
            App(boxed) => {
                boxed.0._apply_owned(rhs, depth, remaining);
                boxed.1._apply_owned(rhs, depth, remaining);
            }
        }
    }

    fn is_reducible(&self, limit: usize, count: usize) -> bool {
        self.lhs_ref().and_then(|t| t.unabs_ref()).is_ok() && (limit == 0 || count < limit)
    }

    /// Performs β-reduction on a `Term` with the specified evaluation `Order` and an optional limit
    /// on the number of reductions (`0` means no limit) and returns the number of performed
    /// reductions.
    ///
    /// # Example
    ///
    /// ```
    /// use lambda_calculus::*;
    ///
    /// let mut expression = parse(&"(λa.λb.λc.b (a b c)) (λa.λb.b)", Classic).unwrap();
    /// let reduced        = parse(&"λa.λb.a b", Classic).unwrap();
    ///
    /// expression.reduce(NOR, 0);
    ///
    /// assert_eq!(expression, reduced);
    /// ```
    pub fn reduce(&mut self, order: Order, limit: usize) -> usize {
        let mut count = 0;

        match order {
            CBN => self.beta_cbn(limit, &mut count),
            NOR => self.beta_nor(limit, &mut count),
            CBV => self.beta_cbv(limit, &mut count),
            APP => self.beta_app(limit, &mut count),
            HSP => self.beta_hsp(limit, &mut count),
            HNO => self.beta_hno(limit, &mut count),
            HAP => self.beta_hap(limit, &mut count),
        }

        count
    }

    fn beta_cbn(&mut self, limit: usize, count: &mut usize) {
        if limit != 0 && *count == limit {
            return;
        }

        if let App(_) = *self {
            self.lhs_mut().unwrap().beta_cbn(limit, count);

            if self.is_reducible(limit, *count) {
                self.eval(count);
                self.beta_cbn(limit, count);
            }
        }
    }

    fn beta_nor(&mut self, limit: usize, count: &mut usize) {
        if limit != 0 && *count == limit {
            return;
        }

        match *self {
            Abs(ref mut abstracted) => abstracted.beta_nor(limit, count),
            App(_) => {
                self.lhs_mut().unwrap().beta_cbn(limit, count);

                if self.is_reducible(limit, *count) {
                    self.eval(count);
                    self.beta_nor(limit, count);
                } else {
                    self.lhs_mut().unwrap().beta_nor(limit, count);
                    self.rhs_mut().unwrap().beta_nor(limit, count);
                }
            }
            _ => (),
        }
    }

    fn beta_cbv(&mut self, limit: usize, count: &mut usize) {
        if limit != 0 && *count == limit {
            return;
        }

        if let App(_) = *self {
            self.lhs_mut().unwrap().beta_cbv(limit, count);
            self.rhs_mut().unwrap().beta_cbv(limit, count);

            if self.is_reducible(limit, *count) {
                self.eval(count);
                self.beta_cbv(limit, count);
            }
        }
    }

    fn beta_app(&mut self, limit: usize, count: &mut usize) {
        if limit != 0 && *count == limit {
            return;
        }

        match *self {
            Abs(ref mut abstracted) => abstracted.beta_app(limit, count),
            App(_) => {
                self.lhs_mut().unwrap().beta_app(limit, count);
                self.rhs_mut().unwrap().beta_app(limit, count);

                if self.is_reducible(limit, *count) {
                    self.eval(count);
                    self.beta_app(limit, count);
                }
            }
            _ => (),
        }
    }

    fn beta_hap(&mut self, limit: usize, count: &mut usize) {
        if limit != 0 && *count == limit {
            return;
        }

        match *self {
            Abs(ref mut abstracted) => abstracted.beta_hap(limit, count),
            App(_) => {
                self.lhs_mut().unwrap().beta_cbv(limit, count);
                self.rhs_mut().unwrap().beta_hap(limit, count);

                if self.is_reducible(limit, *count) {
                    self.eval(count);
                    self.beta_hap(limit, count);
                } else {
                    self.lhs_mut().unwrap().beta_hap(limit, count);
                }
            }
            _ => (),
        }
    }

    fn beta_hsp(&mut self, limit: usize, count: &mut usize) {
        if limit != 0 && *count == limit {
            return;
        }

        match *self {
            Abs(ref mut abstracted) => abstracted.beta_hsp(limit, count),
            App(_) => {
                self.lhs_mut().unwrap().beta_hsp(limit, count);

                if self.is_reducible(limit, *count) {
                    self.eval(count);
                    self.beta_hsp(limit, count)
                }
            }
            _ => (),
        }
    }

    fn beta_hno(&mut self, limit: usize, count: &mut usize) {
        if limit != 0 && *count == limit {
            return;
        }

        match *self {
            Abs(ref mut abstracted) => abstracted.beta_hno(limit, count),
            App(_) => {
                self.lhs_mut().unwrap().beta_hsp(limit, count);

                if self.is_reducible(limit, *count) {
                    self.eval(count);
                    self.beta_hno(limit, count)
                } else {
                    self.lhs_mut().unwrap().beta_hno(limit, count);
                    self.rhs_mut().unwrap().beta_hno(limit, count);
                }
            }
            _ => (),
        }
    }

    /// Checks whether a term contains a free reference to the binder at a given depth.
    ///
    /// At depth `d`, the binder is index `d` (1-indexed De Bruijn).  Each inner abstraction
    /// increments the depth, so the check correctly follows how the index shifts.
    fn _refers_to_binder(&self, depth: usize) -> bool {
        match self {
            Var(0) => true,
            Var(i) => *i == depth,
            Abs(t) => t._refers_to_binder(depth + 1),
            App(boxed) => boxed.0._refers_to_binder(depth) || boxed.1._refers_to_binder(depth),
        }
    }

    /// Decrements all free variable indices that exceed `depth` by one, used after removing
    /// one level of abstraction during η-reduction.
    fn _shift_down_eta(&mut self, depth: usize) {
        match self {
            Var(0) => {}
            Var(i) => {
                if *i > depth {
                    *i -= 1;
                }
            }
            Abs(t) => t._shift_down_eta(depth + 1),
            App(boxed) => {
                boxed.0._shift_down_eta(depth);
                boxed.1._shift_down_eta(depth);
            }
        }
    }

    /// Performs η-reduction on this term with an optional limit on reductions (`0` = no limit)
    /// and returns the number of reductions performed.
    ///
    /// η-reduction removes `λx. M x → M` when `x` is not free in `M`.
    ///
    /// # Example
    ///
    /// ```
    /// use lambda_calculus::*;
    ///
    /// let mut expr = parse(&"λa.λb. a b", Classic).unwrap();
    /// let reduced  = parse(&"λa.a", Classic).unwrap();
    ///
    /// expr.eta(0);
    ///
    /// assert_eq!(expr, reduced);
    /// ```
    pub fn eta(&mut self, limit: usize) -> usize {
        let mut count = 0;
        self._eta_impl(limit, &mut count);
        count
    }

    /// Attempts one η-reduction at the current level. Returns `true` if a reduction occurred.
    fn _eta_step(&mut self, limit: usize, count: &mut usize) -> bool {
        if limit != 0 && *count == limit {
            return false;
        }

        let can_eta = match self {
            Abs(boxed) => match &**boxed {
                App(inner) => match &inner.1 {
                    Var(1) => !inner.0._refers_to_binder(1),
                    _ => false,
                },
                _ => false,
            },
            _ => false,
        };

        if can_eta {
            let body = mem::replace(self, Var(0)).unabs().unwrap();
            let (mut lhs, _rhs) = body.unapp().unwrap();
            lhs._shift_down_eta(1);
            *self = lhs;
            *count += 1;
            true
        } else {
            false
        }
    }

    fn _eta_impl(&mut self, limit: usize, count: &mut usize) {
        // Reduce at this level as much as possible
        loop {
            if !self._eta_step(limit, count) {
                break;
            }
        }

        // Recurse into subterms; then re-check this level since the body may have changed
        match self {
            Abs(boxed) => {
                boxed._eta_impl(limit, count);
                // The body was modified; try this level again
                loop {
                    if !self._eta_step(limit, count) {
                        break;
                    }
                }
            }
            App(boxed) => {
                boxed.0._eta_impl(limit, count);
                boxed.1._eta_impl(limit, count);
            }
            _ => {}
        }
    }
}

impl fmt::Display for Order {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        write!(
            f,
            "{}",
            match *self {
                NOR => "normal",
                CBN => "call-by-name",
                HSP => "head spine",
                HNO => "hybrid normal",
                APP => "applicative",
                CBV => "call-by-value",
                HAP => "hybrid applicative",
            }
        )
    }
}