small_step.rs

use crate::arith::syntax::*;
use Term::*;

pub fn eval1(term: Term) -> Term {
    match term {
        // E-IfTrue
        If(box True, box t1, _) => t1,
        // E-IfFalse
        If(box False, _, box t2) => t2,
        // E-If-Wrong
        If(box t0, _, _) if is_bad_bool(&t0) => Wrong,
        // E-If
        If(box t0, t1, t2) => If(box eval1(t0), t1, t2),
        // E-Succ-Wrong
        Succ(box t0) if is_bad_nat(&t0) => Wrong,
        // E-Succ
        Succ(box t0) => Succ(box eval1(t0)),
        // E-Pred-Wrong
        Pred(box t0) if is_bad_nat(&t0) => Wrong,
        // E-PredZero
        Pred(box Zero) => Zero,
        // E-PredSucc
        Pred(box Succ(box t0)) => t0,
        // E-Pred
        Pred(box t0) => Pred(box eval1(t0)),
        // E-IsZero-Wrong
        IsZero(box t0) if is_bad_nat(&t0) => Wrong,
        // E-IsZeroZero
        IsZero(box Zero) => True,
        // E-IsZeroSucc
        IsZero(box Succ(_)) => False,
        // E-IsZero
        IsZero(box t0) => IsZero(box eval1(t0)),
        _ => term,
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_eval1() {
        assert_eq!(
            eval1(If(box True, box If(box False, box False, box False), box True)),
            If(box False, box False, box False)
        );
        assert_eq!(eval1(Pred(box Succ(box Zero))), Zero);
        assert_eq!(eval1(Pred(box Zero)), Zero);
        assert_eq!(eval1(IsZero(box Zero)), True);
        assert_eq!(eval1(IsZero(box Succ(box Zero))), False);
    }

    #[test]
    fn test_eval_wrong() {
        assert_eq!(eval1(If(box Wrong, box True, box False)), Wrong);
        assert_eq!(eval1(If(box Zero, box True, box False)), Wrong);
        assert_eq!(eval1(If(box Succ(box Zero), box True, box False)), Wrong);
        assert_eq!(eval1(Succ(box Wrong)), Wrong);
        assert_eq!(eval1(Succ(box True)), Wrong);
        assert_eq!(eval1(Succ(box False)), Wrong);
        assert_eq!(eval1(Pred(box Wrong)), Wrong);
        assert_eq!(eval1(Pred(box True)), Wrong);
        assert_eq!(eval1(Pred(box False)), Wrong);
        assert_eq!(eval1(IsZero(box Wrong)), Wrong);
        assert_eq!(eval1(IsZero(box True)), Wrong);
        assert_eq!(eval1(IsZero(box False)), Wrong);
    }
}