1 files changed, 57 insertions, 16 deletions

diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs
index ed1515a..c624b19 100644
--- a/lambda-calcul/rust/src/lambda.rs
+++ b/lambda-calcul/rust/src/lambda.rs
@@ -10,12 +10,12 @@ use std::collections::HashMap;
 use crate::ast::*;
 
 #[derive(Debug, PartialEq)]
-pub struct Environment<'a> {
-    parent: Box<Option<&'a Environment<'a>>>,
-    bindings: HashMap<String, Value>,
+pub struct Environment<'a, T> {
+    parent: Box<Option<&'a Environment<'a, T>>>,
+    bindings: HashMap<String, T>,
 }
 
-impl<'a> Environment<'a> {
+impl<'a, T: Clone> Environment<'a, T> {
     pub fn new() -> Self {
         Environment {
             parent: Box::new(None),
@@ -23,7 +23,7 @@ impl<'a> Environment<'a> {
         }
     }
 
-    fn bind(&mut self, var: &str, value: &Value) {
+    fn bind(&mut self, var: &str, value: &T) {
         self.bindings.insert(var.to_string(), value.clone());
     }
 
@@ -34,7 +34,7 @@ impl<'a> Environment<'a> {
         }
     }
 
-    fn lookup(&self, var: &str) -> Option<&Value> {
+    fn lookup(&self, var: &str) -> Option<&T> {
         self.bindings.get(var).or_else(|| match *self.parent {
             Some(parent) => parent.lookup(var),
             None => None,
@@ -42,7 +42,7 @@ impl<'a> Environment<'a> {
     }
 }
 
-impl<'a> Default for Environment<'a> {
+impl<'a, T: Clone> Default for Environment<'a, T> {
     fn default() -> Self {
         Self::new()
     }
@@ -58,7 +58,7 @@ 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 {
+pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value {
     match arg {
         Value::Def(var, value) => {
             env.bind(var, value);
@@ -98,14 +98,22 @@ fn subst(var: &str, body: &Value, e: &Value) -> Value {
 
 pub fn type_of_all(values: &[Value]) -> Vec<Type> {
     let mut env = Environment::new();
-    values.iter().map(|v| type_of(v, &mut env).unwrap()).collect()
+    values
+        .iter()
+        .map(|v| type_of(v, &mut env).unwrap())
+        .collect()
 }
 
-fn type_of(v: &Value, env: &mut Environment) -> Result<Type, TypeError> {
+fn type_of(v: &Value, env: &mut Environment<Type>) -> Result<Type, TypeError> {
     match v {
-        Value::Num(_) => Ok(Type::Int),
+        Value::Num(_) => Ok(Type::Num),
+        Value::Bool(_) => Ok(Type::Bool),
+        Value::Sym(s) => match env.lookup(s) {
+            Some(ty) => Ok(ty.clone()),
+            None => Err(TypeError::UnboundVariable(s.clone())),
+        },
         _ => Err(TypeError::UnknownType(v.clone())),
-   }
+    }
 }
 
 pub fn gensym() -> String {
@@ -138,10 +146,15 @@ pub fn generate_expr(size: u32, runner: &mut TestRunner) -> Value {
 
 pub fn generate_expression_to_type(size: u32, runner: &mut TestRunner) -> Vec<Value> {
     match size {
-        _ => {
+        0 => {
             let n = any::<u16>().new_tree(runner).unwrap().current();
             vec![Value::Num(n.into())]
-        }
+        },
+        _ => {
+            let n = any::<bool>().new_tree(runner).unwrap().current();
+            vec![Value::Bool(n.into())]
+        },
+
     }
 }
 
@@ -224,7 +237,7 @@ fn gen_terms(u: u32) -> impl Strategy<Value = Value> {
 mod lambda_test {
     use crate::{ast::Type, parser::parse};
 
-    use super::{Environment, Value, eval_all, eval_whnf, type_of};
+    use super::{eval_all, eval_whnf, type_of, Environment, Value};
 
     fn parse1(string: &str) -> Value {
         parse(string).pop().unwrap()
@@ -315,6 +328,34 @@ mod lambda_test {
     fn type_of_a_number_is_int() {
         let value = parse1("12");
         let ty = type_of(&value, &mut Environment::new()).unwrap();
-        assert_eq!(Type::Int, ty);
+        assert_eq!(Type::Num, ty);
+    }
+
+    #[test]
+    fn type_of_a_boolean_is_bool() {
+        let value = parse1("true");
+        let ty = type_of(&value, &mut Environment::new()).unwrap();
+        assert_eq!(Type::Bool, ty);
+    }
+
+    #[test]
+    fn type_of_a_bound_variable_is_looked_up_in_context() {
+        let value = parse1("x");
+        let mut ctx = Environment::new();
+        ctx.bind("x", &Type::Bool);
+
+        let ty = type_of(&value, &mut ctx).unwrap();
+
+        assert_eq!(Type::Bool, ty);
+    }
+
+    #[test]
+    fn type_of_an_unbound_variable_yields_an_error() {
+        let value = parse1("x");
+        let mut ctx = Environment::new();
+
+        let ty = type_of(&value, &mut ctx);
+
+        assert!(ty.is_err());
     }
 }