//! Compiles the [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus),
//! represented by the [`LC`] type,
//! to a tree of [Iota (ι) combinators](https://en.wikipedia.org/wiki/Iota_and_Jot),
//! represented by the [`Iota`] type.

#[cfg(test)]
mod test;

use core::fmt;
use std::rc::Rc;
use thiserror::Error;

#[derive(Debug, PartialEq, Eq)]
pub enum Iota {
    App(Rc<Iota>, Rc<Iota>),
    Iota,
}

#[derive(Debug, Error, PartialEq, Eq)]
pub enum IotaCompileError {
    #[error("LC term has a free variable")]
    FreeVar,
}

impl TryFrom<LC> for Iota {
    type Error = IotaCompileError;

    fn try_from(value: LC) -> Result<Self, Self::Error> {
        todo!()
    }
}

/// A representation of the [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus), with
/// [de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index).
#[derive(Debug, PartialEq, Eq)]
pub enum LC {
    /// A lambda abstraction; binds a new variable.
    Abs(Rc<LC>),
    /// An application of a function to an argument.
    App(Rc<LC>, Rc<LC>),
    /// A variable represented by a
    /// [de Bruijn index](https://en.wikipedia.org/wiki/De_Bruijn_index).
    ///
    /// Zero refers to the closest abstraction, and each successive number refers to a
    /// nested abstraction, as shown in this diagram:
    /// ```text
    ///   ┌─────┐  
    ///   │ ┌─┐ │  
    /// λ λ λ 0 1 2
    /// └─────────┘
    /// ```
    Var(usize),
}

impl LC {
    /// Applies this term to the given term.
    ///
    /// Often more ergonomic than [`LC::App`].
    /// # examples
    /// ```
    /// # use lc_to_iota::LC::{Abs, App, Var};
    /// assert_eq!(Var(0).app(1), App(Var(0).into(), Var(1).into()));
    /// ```
    #[must_use]
    pub fn app(self, x: impl Into<Self>) -> Self {
        Self::App(self.into(), x.into().into())
    }

    /// Adds an abstration around this term.
    ///
    /// Often more ergonomic than [`LC::Abs`], but is somewhat backwards.
    /// # examples
    /// ```
    /// # use lc_to_iota::LC::{Abs, App, Var};
    /// assert_eq!(Var(0).abs(), Abs(Var(0).into()));
    /// ```
    #[must_use]
    pub fn abs(self) -> Self {
        Self::Abs(self.into())
    }

    /// Returns whether any variables are
    /// [free](https://en.wikipedia.org/wiki/Free_variables_and_bound_variables) in self;
    /// that is, whether any variables occur that are not bound by an abstraction.
    ///
    /// # Examples
    /// ```
    /// # use lc_to_iota::LC::{Abs, App, Var};
    /// // x
    /// let x = Var(0);
    /// assert!(x.has_free());
    /// // λx.x
    /// assert!(!x.abs().has_free());
    /// // λfx.f x
    /// let apply = Var(1).app(0).abs().abs();
    /// assert!(!apply.has_free());
    /// ```
    #[must_use]
    pub fn has_free(&self) -> bool {
        self.has_free_past(0)
    }

    fn has_free_past(&self, bound: usize) -> bool {
        match self {
            LC::Abs(x) => x.has_free_past(bound + 1),
            LC::App(f, x) => f.has_free_past(bound) || x.has_free_past(bound),
            // if nothing is bound (bound = 0), x is always free
            LC::Var(x) => *x >= bound,
        }
    }
}

impl From<usize> for LC {
    fn from(n: usize) -> Self {
        Self::Var(n)
    }
}

impl fmt::Display for LC {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            LC::Abs(x) => write!(f, "(λ {x})"),
            LC::App(g, x) => write!(f, "({g} {x})"),
            LC::Var(n) => write!(f, "{n}"),
        }
    }
}