This commit is contained in:
mehbark 2024-11-18 16:19:23 -05:00
parent 16fa54cc51
commit 3c80563ed6
2 changed files with 95 additions and 24 deletions

View file

@ -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<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
/// 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<SKI>, Rc<SKI>),
}
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<SKI>) -> 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<Iota>, Rc<Iota>),
}
#[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<LC> for SKI {
type Error = SKICompileError;
fn try_from(term: LC) -> Result<Self, Self::Error> {
if term.has_free() {
return Err(SKICompileError::FreeVar);
}
todo!()
}
}

View file

@ -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))");
}