feat: start working on typechecker

2 files changed, 98 insertions, 0 deletions

diff --git a/lambda-calcul/rust/src/lib.rs b/lambda-calcul/rust/src/lib.rs
index a8cf18e..53f4c99 100644
--- a/lambda-calcul/rust/src/lib.rs
+++ b/lambda-calcul/rust/src/lib.rs
@@ -2,3 +2,4 @@ pub mod ast;
 pub mod io;
 pub mod lambda;
 pub mod parser;
+mod types;
diff --git a/lambda-calcul/rust/src/types.rs b/lambda-calcul/rust/src/types.rs
new file mode 100644
index 0000000..e91d57e
--- /dev/null
+++ b/lambda-calcul/rust/src/types.rs
@@ -0,0 +1,97 @@
+use crate::ast::Value;
+use proptest::prelude::*;
+use proptest::prop_oneof;
+use std::collections::BTreeMap;
+
+type Name = String;
+
+#[derive(Debug, Clone, PartialEq)]
+enum Type {
+    Int,
+    Bool,
+}
+
+fn any_type() -> impl Strategy<Value = Type> {
+    prop_oneof![Just(Type::Int), Just(Type::Bool),]
+}
+
+struct Context {
+    context: BTreeMap<Name, Type>,
+}
+
+impl Context {
+    pub fn empty() -> Self {
+        Context {
+            context: BTreeMap::new(),
+        }
+    }
+
+    pub fn bind(&mut self, sym: Name, ty: Type) -> &mut Self {
+        self.context.insert(sym, ty);
+        self
+    }
+
+    pub fn type_of(&self, val: &Value) -> Option<Type> {
+        use Value::*;
+
+        match val {
+            Num(_) => Some(Type::Int),
+            Bool(_) => Some(Type::Bool),
+            Sym(s) => self.context.get(s).cloned(),
+            _ => None,
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+
+    use super::*;
+    use crate::ast::Value::*;
+    use proptest::prelude::*;
+
+    proptest! {
+
+        #[test]
+        fn any_int_value_has_type_int(n in any::<i32>().prop_map(Num)) {
+            let ctx = Context::empty();
+
+            let ty = ctx.type_of(&n);
+
+            assert_eq!(Some(Type::Int), ty);
+        }
+
+        #[test]
+        fn any_bool_value_has_type_Bool(n in any::<bool>().prop_map(Bool)) {
+            let ctx = Context::empty();
+
+            let ty = ctx.type_of(&n);
+
+            assert_eq!(Some(Type::Bool), ty);
+        }
+
+        #[test]
+        fn any_bound_variable_has_bound_type(s in crate::ast::identifier(), t in any_type()) {
+            let mut ctx = Context::empty();
+            ctx.bind(s.clone(), t.clone());
+
+            let ty = ctx.type_of(&Sym(s));
+
+            assert_eq!(Some(t), ty);
+        }
+
+        #[test]
+        fn any_unbound_variable_has_no_type(s in crate::ast::identifier()) {
+            let mut ctx = Context::empty();
+
+            let ty = ctx.type_of(&Sym(s));
+
+            assert_eq!(None, ty);
+        }
+
+        #[test]
+        fn def_symbol_has_type_of_its_body(s in crate::ast::identifier(), t in any_type()) {
+        }
+
+    }
+}