diff --git a/src/lib.rs b/src/lib.rs index 0d010f1..a8ad3a2 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,7 +1,9 @@ //! 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. +//! represented by the [`Iota`] type, via the +//! [SKI combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus), +//! represented by the [`SKI`] type. #[cfg(test)] mod test; @@ -10,27 +12,8 @@ use core::fmt; use std::rc::Rc; use thiserror::Error; -#[derive(Debug, PartialEq, Eq)] -pub enum Iota { - App(Rc, Rc), - Iota, -} - -#[derive(Debug, Error, PartialEq, Eq)] -pub enum IotaCompileError { - #[error("LC term has a free variable")] - FreeVar, -} - -impl TryFrom for Iota { - type Error = IotaCompileError; - - fn try_from(value: LC) -> Result { - todo!() - } -} - -/// A representation of the [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus), with +/// A representation of a term of the +/// [lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus), using /// [de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index). #[derive(Debug, PartialEq, Eq)] pub enum LC { @@ -56,7 +39,7 @@ impl LC { /// Applies this term to the given term. /// /// Often more ergonomic than [`LC::App`]. - /// # examples + /// # Examples /// ``` /// # use lc_to_iota::LC::{Abs, App, Var}; /// assert_eq!(Var(0).app(1), App(Var(0).into(), Var(1).into())); @@ -69,7 +52,7 @@ impl LC { /// Adds an abstration around this term. /// /// Often more ergonomic than [`LC::Abs`], but is somewhat backwards. - /// # examples + /// # Examples /// ``` /// # use lc_to_iota::LC::{Abs, App, Var}; /// assert_eq!(Var(0).abs(), Abs(Var(0).into())); @@ -125,3 +108,80 @@ impl fmt::Display for LC { } } } + +/// A representation of a term of the +/// [SKI combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus). +#[derive(Debug, PartialEq, Eq)] +pub enum SKI { + /// The S (substitution) combinator. + /// + /// ```text + /// S x y z = x z (y z) + /// ``` + S, + /// The K (constant) combinator. + /// + /// ```text + /// K x y = x + /// ``` + K, + /// The I (identity) combinator. + /// + /// ```text + /// I x = x + /// ``` + I, + /// Application of one combinator to another. + App(Rc, Rc), +} + +impl SKI { + /// Applies this term to the given term. + /// + /// Often more ergonomic than [`SKI::App`]. + /// # Examples + /// ``` + /// # use lc_to_iota::SKI::*; + /// assert_eq!(I.app(I), App(I.into(), I.into())); + /// assert_eq!(I.app(I).app(K), App(App(I.into(), I.into()).into(), K.into())); + /// ``` + #[must_use] + pub fn app(self, x: impl Into) -> Self { + Self::App(self.into(), x.into().into()) + } +} + +impl fmt::Display for SKI { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + SKI::S => write!(f, "S"), + SKI::K => write!(f, "K"), + SKI::I => write!(f, "I"), + SKI::App(g, x) => write!(f, "({g} {x})"), + } + } +} + +#[derive(Debug, PartialEq, Eq)] +pub enum Iota { + Iota, + App(Rc, Rc), +} + +#[derive(Debug, Error, PartialEq, Eq)] +pub enum SKICompileError { + #[error("LC term has a free variable")] + FreeVar, +} + +// explicit compile method is almost certainly better, but this is fun +impl TryFrom for SKI { + type Error = SKICompileError; + + fn try_from(term: LC) -> Result { + if term.has_free() { + return Err(SKICompileError::FreeVar); + } + todo!() + } +} diff --git a/src/test.rs b/src/test.rs index 24bc621..d56818a 100644 --- a/src/test.rs +++ b/src/test.rs @@ -31,3 +31,14 @@ fn lc_free() { assert!(!term.has_free()); } } + +#[test] +fn ski_display() { + use SKI::*; + assert_eq!(S.to_string(), "S"); + assert_eq!(K.to_string(), "K"); + assert_eq!(I.to_string(), "I"); + assert_eq!(I.app(I).to_string(), "(I I)"); + assert_eq!(S.app(K).app(I).to_string(), "((S K) I)"); + assert_eq!(S.app(K.app(I)).to_string(), "(S (K I))"); +}