diff --git a/core/src/command.rs b/core/src/command.rs
index 0054e094c53cece6d8cb150876c6ffc7dfb9c068..e387449e0b417fd97f68d61cf83cb242baa6a6e5 100644
--- a/core/src/command.rs
+++ b/core/src/command.rs
@@ -1,7 +1,7 @@
use crate::Term;
use std::fmt::{Display, Formatter};
-#[derive(Clone, Debug, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq)]
pub enum Command {
Define(String, Term),
CheckType(Term, Term),
diff --git a/core/src/lib.rs b/core/src/lib.rs
index 30e5e5c82bcf4b8428c3b7a0eebe83f7534556a6..b91b3b42d12a072dfc863de6890d4422b6146bdc 100644
--- a/core/src/lib.rs
+++ b/core/src/lib.rs
@@ -1,3 +1,4 @@
+#![feature(box_patterns)]
#![feature(box_syntax)]
mod command;
diff --git a/core/src/term.rs b/core/src/term.rs
index 351d33b3857ef1b8b7fcc6bd7551a993f14215ef..016a918dd260cb93edab9222b3c7f20c4db11240 100644
--- a/core/src/term.rs
+++ b/core/src/term.rs
@@ -1,6 +1,10 @@
use std::fmt::{Display, Formatter};
-#[derive(Clone, Debug, PartialEq)]
+// TODO: Use derive_more to constraint types (#11)
+// struct Index(usize);
+// struct Level(usize);
+
+#[derive(Clone, Debug, Eq, PartialEq)]
pub enum Term {
Prop,
Var(usize),
@@ -10,15 +14,231 @@ pub enum Term {
Prod(Box<Term>, Box<Term>),
}
+use Term::*;
+
+impl Term {
+ /// Apply one step of β-reduction, using leftmost outermost evaluation strategy.
+ pub fn beta_reduction(self) -> Term {
+ match self {
+ App(box Abs(_, box t1), box t2) => t1.substitute(t2, 1),
+ App(box t1, box t2) => App(box t1.beta_reduction(), box t2),
+ Abs(x, box t) => Abs(x, box t.beta_reduction()),
+ _ => self,
+ }
+ }
+
+ fn shift(self, offset: usize, depth: usize) -> Term {
+ match self {
+ Var(i) if i > depth => Var(i + offset),
+ App(box t1, box t2) => App(box t1.shift(offset, depth), box t2.shift(offset, depth)),
+ Abs(t1, box t2) => Abs(t1, box t2.shift(offset, depth + 1)),
+ Prod(t1, box t2) => Prod(t1, box t2.shift(offset, depth + 1)),
+ _ => self,
+ }
+ }
+
+ fn substitute(self, rhs: Term, depth: usize) -> Term {
+ match self {
+ Var(i) if i == depth => rhs.shift(depth - 1, 0),
+ Var(i) if i > depth => Var(i - 1),
+
+ App(l, r) => App(
+ box l.substitute(rhs.clone(), depth),
+ box r.substitute(rhs, depth),
+ ),
+ Abs(t, term) => Abs(t, box term.substitute(rhs, depth + 1)),
+ Prod(t, term) => Prod(t, box term.substitute(rhs, depth + 1)),
+ _ => self,
+ }
+ }
+}
+
impl Display for Term {
fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
match self {
- Term::Prop => write!(f, "\u{02119}"),
- Term::Var(i) => write!(f, "{}", i),
- Term::Type(i) => write!(f, "\u{1D54B}({})", i),
- Term::App(t1, t2) => write!(f, "({}) {}", t1, t2),
- Term::Abs(t1, t2) => write!(f, "\u{003BB}{} \u{02192} {}", t1, t2),
- Term::Prod(t1, t2) => write!(f, "\u{02200}{} \u{02192} {}", t1, t2),
+ Prop => write!(f, "\u{02119}"),
+ Var(i) => write!(f, "{}", i),
+ Type(i) => write!(f, "\u{1D54B}({})", i),
+ App(t1, t2) => write!(f, "({} {})", t1, t2),
+ Abs(t1, t2) => write!(f, "\u{003BB}{} \u{02192} {}", t1, t2),
+ Prod(t1, t2) => write!(f, "\u{02200}{} \u{02192} {}", t1, t2),
}
}
}
+
+#[cfg(test)]
+mod tests {
+ // TODO: Correctly types lambda terms (#9)
+
+ use super::Term::*;
+
+ #[test]
+ fn simple_subst() {
+ // λx.(λy.x y) x
+ let term = Abs(
+ box Prop,
+ box App(
+ box Abs(box Prop, box App(box Var(2), box Var(1))),
+ box Var(1),
+ ),
+ );
+
+ // λx.x x
+ let reduced = Abs(box Prop, box App(box Var(1), box Var(1)));
+
+ assert_eq!(term.beta_reduction(), reduced);
+ }
+
+ #[test]
+ fn complex_subst() {
+ // (λa.λb.λc.(a (λd.λe.e (d b) (λ_.c)) (λd.d)) (λa.λb.a b)
+ let term = App(
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box App(
+ box App(
+ box Var(3),
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(box Var(1), box App(box Var(2), box Var(4))),
+ ),
+ ),
+ ),
+ box Abs(box Prop, box Var(2)),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ ),
+ ),
+ box Abs(box Prop, box Abs(box Prop, box App(box Var(2), box Var(1)))),
+ );
+
+ // λa.λb.(((λc.λd.c d) (λc.λd.d (c a))) (λ_.b)) (λc.c)
+ let term_step_1 = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box App(
+ box App(
+ box Abs(box Prop, box Abs(box Prop, box App(box Var(2), box Var(1)))),
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(box Var(1), box App(box Var(2), box Var(4))),
+ ),
+ ),
+ ),
+ box Abs(box Prop, box Var(2)),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ );
+
+ // λa.λb.((λc.(λd.λe.e (d a)) c) (λ_.b)) (λc.c)
+ let term_step_2 = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box App(
+ box Abs(
+ box Prop,
+ box App(
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(box Var(1), box App(box Var(2), box Var(5))),
+ ),
+ ),
+ box Var(1),
+ ),
+ ),
+ box Abs(box Prop, box Var(2)),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ );
+
+ // λa.λb.[(λc.λd.(d (c a))) (λ_.b)] (λc.c)
+ let term_step_3 = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box App(
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(box Var(1), box App(box Var(2), box Var(4))),
+ ),
+ ),
+ box Abs(box Prop, box Var(2)),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ );
+
+ // λa.λb.(λc.c ((λ_.b) a)) (λc.c)
+ let term_step_4 = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box Abs(
+ box Prop,
+ box App(
+ box Var(1),
+ box App(box Abs(box Prop, box Var(3)), box Var(3)),
+ ),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ );
+
+ // λa.λb.(λc.c) ((λ_.b) a)
+ let term_step_5 = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box Abs(box Prop, box Var(1)),
+ box App(box Abs(box Prop, box Var(2)), box Var(2)),
+ ),
+ ),
+ );
+
+ // λa.λb.(λc.b) a
+ let term_step_6 = Abs(
+ box Prop,
+ box Abs(box Prop, box App(box Abs(box Prop, box Var(2)), box Var(2))),
+ );
+
+ // λa.λb.b
+ let term_step_7 = Abs(box Prop, box Abs(box Prop, box Var(1)));
+
+ assert_eq!(term.beta_reduction(), term_step_1);
+ assert_eq!(term_step_1.beta_reduction(), term_step_2);
+ assert_eq!(term_step_2.beta_reduction(), term_step_3);
+ assert_eq!(term_step_3.beta_reduction(), term_step_4);
+ assert_eq!(term_step_4.beta_reduction(), term_step_5);
+ assert_eq!(term_step_5.beta_reduction(), term_step_6);
+ assert_eq!(term_step_6.beta_reduction(), term_step_7);
+ assert_eq!(term_step_7.clone().beta_reduction(), term_step_7);
+ }
+}