implementation of the untyped lambda calculus in Rust and simple tests for it.

lib.rs

use std::collections::HashSet;

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct Var(String);

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Term {
    Var(Var),
    Lam(Var, Box<Term>),
    App(Box<Term>, Box<Term>),
}

impl Term {
    fn free_vars(&self) -> HashSet<&Var> {
        use Term::*;
        let mut set;
        match *self {
            Var(ref v) => {
                set = HashSet::new();
                set.insert(v);
            }
            App(ref left, ref right) => set = left.free_vars()
                                                  .union(&right.free_vars())
                                                  .cloned()
                                                  .collect(),
            Lam(ref bind, ref inner) => {
                set = inner.free_vars();
                set.remove(&bind);
            }
        }
        set
    }
    fn substitute(self, from: &Var, to: &Term) -> Term {
        use Term::*;
        match self {
            Var(v) => if v == *from { to.clone() } else { Var(v) },
            App(left, right) => App(Box::new(left.substitute(from, to)),
                                    Box::new(right.substitute(from, to))),
            Lam(ref bind, ref inner) => {
                if bind == from {
                    self.clone()
                } else {
                    if !to.free_vars().contains(bind) {
                        Lam(bind.clone(), Box::new(inner.clone().substitute(from, to)))
                    } else {
                        let mut should_be_unused = bind.clone();
                        should_be_unused.0.push_str("'");
                        loop {
                            let used: HashSet<&::Var> = inner.free_vars()
                                                             .union(&to.free_vars())
                                                             .cloned()
                                                             .collect();
                            if used.contains(&should_be_unused) {
                                should_be_unused.0.push_str("'")
                            } else {
                                let renamed = 
                                    Lam(should_be_unused.clone(),
                                        Box::new(inner.clone()
                                                      .substitute(bind, &Var(should_be_unused))));
                                return renamed.substitute(from, to)
                            }
                        }
                    }
                }
            }
        }
    }
    pub fn whnf(self) -> Term {
        use Term::*;
        fn spine(leftmost: Term, stack: &[Term]) -> Term {
            match (leftmost, stack) {
                (App(left, right), _) => {
                    let mut new_stack: Vec<Term> = stack.into();
                    new_stack.push(*right);
                    spine(*left, &new_stack)
                }
                (Lam(ref from, ref inner), ref stack) if !stack.is_empty() => {
                    let mut new_stack: Vec<Term> = (*stack).into();
                    let right = new_stack.pop().unwrap();
                    inner.clone().substitute(&from, &right)
                }
                (leftmost, _) =>
                    stack.iter()
                         .fold(leftmost, |l, r| App(Box::new(l), Box::new(r.clone()))),
            }
        }
        spine(self, &[])
    }
}

#[cfg(test)]
mod tests {

    use super::*;
    
    // I combinator = \x. x
    fn i_comb() -> Term {
        use Term::*;
        Lam(
            ::Var("x".into()),
            Box::new(Var(::Var("x".into())))
        )
    }

    // I y = y
    #[test]
    fn simple_subst() {
        use Term::*;
        let input = App(
                        Box::new(i_comb()),
                        Box::new(Var(::Var("y".into())))
                    );
        let output = Var(::Var("y".into()));
        assert_eq!(input.whnf(), output)
    }
    
    // I (y z) = y z
    #[test]
    fn simple_subst2() {
        use Term::*;
        let input = App(
                        Box::new(i_comb()),
                        Box::new(App(
                            Box::new(Var(::Var("y".into()))),
                            Box::new(Var(::Var("z".into())))
                        ))
                    );
        let output = App(
                         Box::new(Var(::Var("y".into()))),
                         Box::new(Var(::Var("z".into())))
                     );
        assert_eq!(input.whnf(), output)
    }
    
    // \z. I z = \z. I z
    #[test]
    fn whnf_no_subst_in_lam() {
        use Term::*;
        let term = Lam(
                       ::Var("z".into()),
                       Box::new(App(
                           Box::new(i_comb()),
                           Box::new(Var(::Var("z".into())))
                       ))
                   );
        assert_eq!(term.clone().whnf(), term)
    }
    
    // (\x. \z. x) z = \z'. z
    #[test]
    fn should_rename() {
        use Term::*;
        let input = App(
                        Box::new(Lam(
                           ::Var("x".into()),
                           Box::new(Lam(
                               ::Var("z".into()),
                               Box::new(Var(::Var("x".into())))
                           ))
                       )),
                       Box::new(Var(::Var("z".into())))
                    );
        let output = Lam(
                         ::Var("z'".into()),
                         Box::new(Var(::Var("z".into())))
                     );
        assert_eq!(input.whnf(), output)
    }
    
}