1 files changed, 59 insertions, 14 deletions

diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs
index ea571fd..80f2d5c 100644
--- a/lambda-calcul/rust/src/lambda.rs
+++ b/lambda-calcul/rust/src/lambda.rs
@@ -1,3 +1,4 @@
+use log::debug;
 use proptest::{
     arbitrary::any,
     prelude::*,
@@ -50,7 +51,11 @@ impl<'a, T: Clone> Default for Environment<'a, T> {
 
 pub fn eval_all(values: &[Value]) -> Vec<Value> {
     let mut env = Environment::new();
-    values.iter().map(|v| eval_whnf(v, &mut env)).collect()
+    let mut context = Environment::new();
+    values
+        .iter()
+        .map(|v| eval_whnf(v, &mut env, &mut context))
+        .collect()
 }
 
 /// Reduce the given value to weak head normal form using call-by-name
@@ -58,8 +63,13 @@ pub fn eval_all(values: &[Value]) -> Vec<Value> {
 ///
 /// call-by-name reduces the leftmost outermost redex first, which is
 /// not under a lambda abstraction.
-pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value {
-    match arg {
+pub fn eval_whnf(
+    arg: &Value,
+    env: &mut Environment<Value>,
+    context: &mut Environment<Type>,
+) -> Value {
+    debug!("evaluating {}", arg);
+    let result = match arg {
         Value::Def(var, value) => {
             env.bind(var, value);
             Value::Bool(true) // TODO: return a more meaningful value?
@@ -67,19 +77,26 @@ pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value {
         Value::Let(var, value, expr) => {
             let mut newenv = env.extends();
             newenv.bind(var, value);
-            eval_whnf(expr, &mut newenv)
+            eval_whnf(expr, &mut newenv, context)
         }
-        Value::App(l, r) => match eval_whnf(l, env) {
-            Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env),
-            Value::Sym(var) => match env.lookup(&var) {
-                Some(val) => eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env),
-                None => arg.clone(),
+        Value::App(l, r) => match eval_whnf(l, env, context) {
+            Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env, context),
+            Value::Sym(var) => match var.as_str() {
+                ":type-of" => type_of(r, context).map(Value::Type).unwrap(),
+                _ => match env.lookup(&var) {
+                    Some(val) => {
+                        eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env, context)
+                    }
+                    None => arg.clone(),
+                },
             },
             other => Value::App(Box::new(other), r.clone()),
         },
         Value::Sym(var) => env.lookup(var).unwrap_or(arg).clone(),
         other => other.clone(),
-    }
+    };
+    debug!("evaluated to {}", result);
+    result
 }
 
 fn subst(var: &str, body: &Value, e: &Value) -> Value {
@@ -234,21 +251,25 @@ fn gen_terms(u: u32) -> impl Strategy<Value = Value> {
 
 #[cfg(test)]
 mod lambda_test {
-    use crate::{ast::Type, parser::parse};
-
     use super::{eval_all, eval_whnf, type_of, Environment, Value};
+    use crate::{ast::Type, lambda::gen_terms, parser::parse};
+    use proptest::{
+        prelude::*,
+        strategy::{Strategy, ValueTree},
+        test_runner::TestRunner,
+    };
 
     fn parse1(string: &str) -> Value {
         parse(string).pop().unwrap()
     }
 
     fn eval1(value: &Value) -> Value {
-        eval_whnf(value, &mut Environment::new())
+        eval_whnf(value, &mut Environment::new(), &mut Environment::new())
     }
 
     #[test]
     fn evaluate_symbol_starting_with_x_returns_same_symbol() {
-        let sym= "x1xYgddw7";
+        let sym = "x1xYgddw7";
 
         let value = parse1(sym);
         assert_eq!(value, eval1(&value));
@@ -308,6 +329,11 @@ mod lambda_test {
     }
 
     #[test]
+    fn type_of_returns_type_of_expression() {
+        let value = parse1("(:type-of 11)");
+        assert_eq!(Value::Type(Type::Num), eval1(&value));
+    }
+    #[test]
     fn defined_symbols_are_evaluated_to_their_definition() {
         let values = parse("(def foo 12)  foo");
         assert_eq!(vec![Value::Bool(true), Value::Num(12)], eval_all(&values));
@@ -375,4 +401,23 @@ mod lambda_test {
 
         assert_eq!(Type::Arr(Box::new(Type::Num), Box::new(Type::Num)), ty);
     }
+
+    #[test]
+    fn any_terms() {
+        let mut runner = TestRunner::default();
+        for i in 0..100 {
+            let value = any::<u32>()
+                .prop_flat_map(gen_terms)
+                .new_tree(&mut runner)
+                .unwrap()
+                .current();
+            let evaluation = eval1(&value);
+            println!(
+                "{} term: {}, evaluation: {}",
+                value == evaluation,
+                value,
+                evaluation
+            );
+        }
+    }
 }