Evaluate in normal order until normal form is reached

1 files changed, 31 insertions, 14 deletions

diff --git a/rust/src/lambda.rs b/rust/src/lambda.rs
index 9b2a6f2..a6da87b 100644
--- a/rust/src/lambda.rs
+++ b/rust/src/lambda.rs
@@ -10,25 +10,36 @@ use parser::*;
 pub fn run(arg: &str) -> String {
     let content = read_to_string(arg).unwrap();
     let value = parse(&content.to_string());
-    let result = interpret(&value);
+    let result = eval(&value);
 
     result.to_string()
 }
 
-fn interpret(arg: &Value) -> Value {
+fn eval(arg: &Value) -> Value {
     match arg {
         Value::App(l, r) => {
-            let result = apply(&interpret(l), &interpret(r));
-            if result == *arg {
-                result
+            let result = apply(&eval(l), r);
+            if is_reducible(&result) {
+                eval(&result)
             } else {
-                interpret(&result)
+                result
             }
         }
         other => other.clone(),
     }
 }
 
+fn is_reducible(result: &Value) -> bool {
+    match result {
+        Value::App(l, r) => match **l {
+            Value::Lam(_, _) => true,
+            _ => is_reducible(l) || is_reducible(r),
+        },
+        Value::Lam(_, _) => false,
+        _ => false,
+    }
+}
+
 fn apply(l: &Value, r: &Value) -> Value {
     if let Value::Lam(v, body) = l {
         subst(v, body, r)
@@ -60,24 +71,24 @@ fn gensym() -> String {
 
 #[cfg(test)]
 mod lambda_test {
-    use crate::{interpret, parse, Value};
+    use crate::{eval, parse, Value};
 
     #[test]
     fn evaluating_a_non_reducible_value_yields_itself() {
         let value = parse("(foo 12)");
-        assert_eq!(value, interpret(&value));
+        assert_eq!(value, eval(&value));
     }
 
     #[test]
     fn evaluating_application_on_an_abstraction_reduces_it() {
         let value = parse("((lam x x) 12)");
-        assert_eq!(Value::Num(12), interpret(&value));
+        assert_eq!(Value::Num(12), eval(&value));
     }
 
     #[test]
     fn substitution_occurs_within_abstraction_body() {
         let value = parse("(((lam x (lam y x)) 13) 12)");
-        assert_eq!(Value::Num(13), interpret(&value));
+        assert_eq!(Value::Num(13), eval(&value));
     }
 
     #[test]
@@ -85,26 +96,32 @@ mod lambda_test {
         let value = parse("(((lam x (lam y (y x))) 13) 12)");
         assert_eq!(
             Value::App(Box::new(Value::Num(12)), Box::new(Value::Num(13))),
-            interpret(&value)
+            eval(&value)
         );
     }
 
     #[test]
     fn substitution_does_not_capture_free_variables() {
         let value = parse("(((lam x (lam x x)) 13) 12)");
-        assert_eq!(Value::Num(12), interpret(&value));
+        assert_eq!(Value::Num(12), eval(&value));
     }
 
     #[test]
     fn interpretation_applies_to_both_sides_of_application() {
         let value = parse("((lam x x) ((lam x x) 12))");
-        assert_eq!(Value::Num(12), interpret(&value));
+        assert_eq!(Value::Num(12), eval(&value));
     }
 
     #[test]
     fn reduction_is_applied_until_normal_form_is_reached() {
         let value = parse("((((lam y (lam x (lam y (x y)))) 13) (lam x x)) 11)");
-        assert_eq!(Value::Num(11), interpret(&value));
+        assert_eq!(Value::Num(11), eval(&value));
     }
 
+    #[test]
+    fn reduction_always_select_leftmost_outermost_redex() {
+        // this should not terminate if we evaluate the rightmost redex first
+        let value = parse("((lam x 1) ((lam x (x x)) (lam x (x x))))");
+        assert_eq!(Value::Num(1), eval(&value));
+    }
 }