1 files changed, 38 insertions, 39 deletions

diff --git a/src/simple.rs b/src/simple.rs
index 30a609b..e794f93 100644
--- a/src/simple.rs
+++ b/src/simple.rs
@@ -6,80 +6,79 @@ use crate::ast::*;
 
 pub fn check(context: Context, expression: Expression, target: Type) -> bool {
     match expression {
-        Expression::Annotation { expr, kind } => kind == target,
+        // should never happen
+        Expression::Annotation { expr, kind } => (kind == target) && check(context, *expr, kind),
         Expression::Constant { term } => term.kind == target,
         Expression::Variable { id } => {
+            // in the future: extend to closures? nah probably not
             match context.get(&id) {
-                Some(term) => term.kind == target,
-                None => false,
+                Some(term) if term.kind == target => true,
+                _ => false
             }
         },
-        // fixme: i don't think this works
         Expression::Abstraction { param, func } => {
-            todo!()
-        },
-        Expression::Application { func, arg } => {
-            match *func {
-                Expression::Abstraction { param, func } => {
+            match target {
+                Type::Function { from, to } => {
                     let mut context = context;
-                    context.insert(param, Term { val: 0, kind: arg.kind });
-                    return check(context, *func, target);
+                    context.insert(param, Term { val: 0, kind: *from }); // hack
+                    return check(context, *func, *to);
                 },
                 _ => false
             }
         },
+        // should never happen
+        Expression::Application { func, arg } => check(context, *func, target),
         Expression::Conditional { if_cond, if_then, if_else } => {
             check(context.clone(), *if_cond, Type::Boolean) &&
-            check(context.clone(), *if_then, target) &&
-            check(context.clone(), *if_else, target)
-        },
+            check(context.clone(), *if_then, target.clone()) &&
+            check(context.clone(), *if_else, target.clone())
+        }
     }
 }
 
 // empty's gonna cause problems
 pub fn infer(context: Context, expression: Expression) -> Option<Type> {
     match expression {
-        Expression::Annotation { expr, kind } => Some(kind),
+        Expression::Annotation { expr, kind } => {
+            match check(context, *expr, kind.clone()) {
+                true => Some(kind),
+                false => None
+            }
+        },
         Expression::Constant { term } => Some(term.kind),
         Expression::Variable { id } => {
             match context.get(&id) {
-                Some(term) => Some(term.kind),
+                Some(term) => Some(term.clone().kind),
                 None => None
             }
         },
-        // this is probably bad. we don't know what type param is since it's a raw identifier.
-        // to fix: probably either require param to be annotated (good idea?), or
-        // allow arbitrary expressions (bad idea?)
-        // edit: turns out the typed lambda calculus actually REQUIREs annotations on parameters lmao
-        Expression::Abstraction { param, func } => {
-            let mut context = context;
-            context.insert(param, Term { val: 0, kind: Type::Empty}); // even worse hack
-            return infer(context, *func);
-        },
         Expression::Application { func, arg } => {
-            match *func {
-                Expression::Abstraction { param, func } => {
-                    match infer(context.clone(), *arg) {
-                        Some(arg) => {
-                            let mut context = context;
-                            context.insert(param, Term { val: 0, kind: arg }); // hack
-                            return infer(context, *func);
-                        },
-                        None => None
+            // Bt-App:
+            // \Gamma \derives t_1 \infer \tau_1 \to \tau_2, \Gamma \derives t_2 \check \tau_1
+            // -------------------------------------------
+            // \Gamma \derives t_1 t_2 \infer \tau_2
+            match infer(context.clone(), *func) {
+                Some(Type::Function { from, to }) => {
+                    match check(context, *arg, *from) {
+                        true => Some(*to),
+                        false => None
                     }
                 },
                 _ => None
             }
         },
+        // should not happen
+        Expression::Abstraction { param, func } => infer(context, *func),
+        // idk
         Expression::Conditional { if_cond, if_then, if_else } => {
-            if infer(context.clone(), *if_cond) == Some(Type::Boolean) {
+            if check(context.clone(), *if_cond, Type::Boolean) {
                 let kind = infer(context.clone(), *if_then);
-                if infer(context, *if_else) == kind {
+                if kind == infer(context, *if_else) {
                     return kind;
                 }
             }
             return None;
-        },
+        }
     }
 }
 
@@ -91,7 +90,7 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, &'stati
         Expression::Constant { term } => Ok(term),
         Expression::Variable { id } => {
             match context.get(&id) {
-                Some(term) => Ok(*term),
+                Some(term) => Ok(term.clone()),
                 None => Err("no such variable in context")
             }
         },
@@ -118,6 +117,6 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, &'stati
                 Ok(Term { val: 0, .. }) => execute(context, *if_else),
                 _ => Err("invalid type for a conditional")
             }
-        },
+        }
     }
 }