Skip to content
Snippets Groups Projects
Commit ec8fb35f authored by v-lafeychine's avatar v-lafeychine
Browse files

Resolve "Term definitions" ✨️ 

Closes #2 🐔️👍️
Approved-by: default avatarbelazy <aarthuur01@gmail.com>
Approved-by: default avatarloutr <loutr@crans.org>
Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>

🦀️🍰🦀️🍰🦀️🍰

* feat(term): Complete beta-reduction

* [WIP] feat(term): Improve beta-reduction + Add tests

* feat(term): Early beta-reduction

* feat(term): Add early Term struct + Display trait
parent 5b58307f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
core/src/command.rs
+ 1
− 1
View file @ ec8fb35f
use crate::Term; use crate::Term;
use std::fmt::{Display, Formatter}; use std::fmt::{Display, Formatter};
#[derive(Clone, Debug, PartialEq)] #[derive(Clone, Debug, Eq, PartialEq)]
pub enum Command { pub enum Command {
Define(String, Term), Define(String, Term),
CheckType(Term, Term), CheckType(Term, Term),
......
core/src/lib.rs
+ 1
− 0
View file @ ec8fb35f
#![feature(box_patterns)]
#![feature(box_syntax)] #![feature(box_syntax)]
mod command; mod command;
......
core/src/term.rs
+ 227
− 7
View file @ ec8fb35f
use std::fmt::{Display, Formatter}; 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 { pub enum Term {
Prop, Prop,
Var(usize), Var(usize),
...@@ -10,15 +14,231 @@ pub enum Term { ...@@ -10,15 +14,231 @@ pub enum Term {
Prod(Box<Term>, Box<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 { impl Display for Term {
fn fmt(&self, f: &mut Formatter) -> std::fmt::Result { fn fmt(&self, f: &mut Formatter) -> std::fmt::Result {
match self { match self {
Term::Prop => write!(f, "\u{02119}"), Prop => write!(f, "\u{02119}"),
Term::Var(i) => write!(f, "{}", i), Var(i) => write!(f, "{}", i),
Term::Type(i) => write!(f, "\u{1D54B}({})", i), Type(i) => write!(f, "\u{1D54B}({})", i),
Term::App(t1, t2) => write!(f, "({}) {}", t1, t2), App(t1, t2) => write!(f, "({} {})", t1, t2),
Term::Abs(t1, t2) => write!(f, "\u{003BB}{} \u{02192} {}", t1, t2), Abs(t1, t2) => write!(f, "\u{003BB}{} \u{02192} {}", t1, t2),
Term::Prod(t1, t2) => write!(f, "\u{02200}{} \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);
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment