1 files changed, 45 insertions, 5 deletions
diff --git a/src/simple.rs b/src/simple.rs
index b7ef94a..cedc016 100644
--- a/src/simple.rs
+++ b/src/simple.rs
@@ -1,13 +1,48 @@
 // Simple bidirectional type checking
 
+#![allow(unused_variables)]
+
 use crate::ast::*;
 
-pub fn infer(context: Context, expression: Expression) {
-    todo!();
+pub fn check(context: Context, expression: Expression, target: Type) -> bool {
+    match expression {
+        Expression::Annotation { expr, kind } => kind == target,
+        Expression::Constant { term } => term.kind == target,
+        Expression::Variable { id } => {
+            match context.get(&id) {
+                Some(term) => term.kind == target,
+                None => false,
+            }
+        },
+        Expression::Abstraction { param, func } => todo!(),
+        Expression::Application { func, arg } => todo!(),
+        Expression::Conditional { if_cond, if_then, if_else } => todo!(),
+    }
 }
 
-pub fn check(context: Context, expression: Expression) {
-    todo!();
+// empty's gonna cause problems
+pub fn infer(context: Context, expression: Expression) -> Option<Type> {
+    match expression {
+        Expression::Annotation { expr, kind } =>  Some(kind),
+        Expression::Constant { term } => Some(term.kind),
+        Expression::Variable { id } => {
+            match context.get(&id) {
+                Some(term) => Some(term.kind),
+                None => None
+            }
+        },
+        Expression::Abstraction { param, func } => return None,
+        Expression::Application { func, arg } => return None,
+        Expression::Conditional { if_cond, if_then, if_else } => {
+            if infer(context.clone(), *if_cond) == Some(Type::Boolean) {
+                let kind = infer(context.clone(), *if_then);
+                if infer(context, *if_else) == kind {
+                    return kind;
+                }
+            }
+            return None;
+        },
+    }
 }
 
 /// Evaluates an expression given a context (of variables) to a term.
@@ -16,7 +51,12 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, &'stati
     match expression {
         Expression::Annotation { expr, .. } => execute(context, *expr),
         Expression::Constant { term } => Ok(term),
-        Expression::Variable { id } => context.get(&id).ok_or("no such variable in context").map(|x| *x),
+        Expression::Variable { id } => {
+            match context.get(&id) {
+                Some(term) => Ok(*term),
+                None => Err("no such variable in context")
+            }
+        },
         Expression::Abstraction { .. } => Err("attempting to execute an abstraction"),
         Expression::Application { func, arg } => {
             match *func {