bidirectional working

2 files changed, 72 insertions, 59 deletions

diff --git a/src/main.rs b/src/main.rs
index 8f93e51..bff203b 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -21,16 +21,28 @@ fn main() {
 
                 input.clear();
                 stdin().read_line(&mut input).unwrap();
-                simple::infer(Context::new(), parser::parse(&input));
+                match simple::infer(Context::new(), parser::parse(&input)) {
+                    Ok(term) => println!("infers! {:?}", term),
+                    Err(e) => println!("{:?}", e),
+                }
             },
-            "c" | "t" | "check" | "typecheck" => {
+            "c" | "t" | "check" => {
                 println!("enter fully annotated expression to typecheck");
                 print!("\x1b[1m====> \x1b[22m");
                 stdout().flush().unwrap();
 
                 input.clear();
                 stdin().read_line(&mut input).unwrap();
-                simple::check(Context::new(), parser::parse(&input), Type::Empty);
+                let kind = simple::infer(Context::new(), parser::parse(&input));
+                match kind {
+                    Ok(kind) => {
+                        match simple::check(Context::new(), parser::parse(&input), kind) {
+                            Ok(_) => println!("checks!"),
+                            Err(e) => println!("{:?}", e),
+                        }
+                    },
+                    Err(_) => println!("failed to infer high-level type!")
+                }
             },
             "e" | "r" | "execute" | "run" => {
                 println!("enter expression to execute");
@@ -39,7 +51,10 @@ fn main() {
 
                 input.clear();
                 stdin().read_line(&mut input).unwrap();
-                println!("{:?}", simple::execute(Context::new(), parser::parse(&input)));
+                match simple::execute(Context::new(), parser::parse(&input)) {
+                    Ok(term) => println!("{:?}", term),
+                    Err(e) => println!("{:?}", e)
+                }
             },
             _ => println!("invalid option {}. please try again.", input.trim())
         }
diff --git a/src/simple.rs b/src/simple.rs
index e794f93..4419680 100644
--- a/src/simple.rs
+++ b/src/simple.rs
@@ -4,18 +4,27 @@
 
 use crate::ast::*;
 
-pub fn check(context: Context, expression: Expression, target: Type) -> bool {
+pub fn check(context: Context, expression: Expression, target: Type) -> Result<(), (&'static str, Context, Type)> {
     match expression {
-        // should never happen
-        Expression::Annotation { expr, kind } => (kind == target) && check(context, *expr, kind),
-        Expression::Constant { term } => term.kind == target,
+        Expression::Annotation { expr, kind } => Err(("attempting to typecheck an annotation", context, target)),
+        // Bt-CheckInfer
+        Expression::Constant { term } => {
+            if term.kind == target {
+                Ok(())
+            } else {
+                Err(("constant is of wrong type", context, target))
+            }
+        },
+        // Bt-CheckInfer
         Expression::Variable { id } => {
             // in the future: extend to closures? nah probably not
             match context.get(&id) {
-                Some(term) if term.kind == target => true,
-                _ => false
+                Some(term) if term.kind == target => Ok(()),
+                Some(_) => Err(("variable is of wrong type", context, target)),
+                None => Err(("failed to find variable in context", context, target))
             }
         },
+        // Bt-Abs
         Expression::Abstraction { param, func } => {
             match target {
                 Type::Function { from, to } => {
@@ -23,99 +32,88 @@ pub fn check(context: Context, expression: Expression, target: Type) -> bool {
                     context.insert(param, Term { val: 0, kind: *from }); // hack
                     return check(context, *func, *to);
                 },
-                _ => false
+                _ => Err(("attempting to check an abstraction with a non-function type", context, target))
             }
         },
-        // should never happen
-        Expression::Application { func, arg } => check(context, *func, target),
+        Expression::Application { func, arg } => Err(("attempting to check an application", context, target)),
+        // T-If
         Expression::Conditional { if_cond, if_then, if_else } => {
-            check(context.clone(), *if_cond, Type::Boolean) &&
-            check(context.clone(), *if_then, target.clone()) &&
-            check(context.clone(), *if_else, target.clone())
+            check(context.clone(), *if_cond, Type::Boolean)?;
+            check(context.clone(), *if_then, target.clone())?;
+            check(context.clone(), *if_else, target.clone())?;
+            return Ok(());
         }
     }
 }
 
 // empty's gonna cause problems
-pub fn infer(context: Context, expression: Expression) -> Option<Type> {
+pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static str, Context, Type)> {
     match expression {
-        Expression::Annotation { expr, kind } => {
-            match check(context, *expr, kind.clone()) {
-                true => Some(kind),
-                false => None
-            }
-        },
-        Expression::Constant { term } => Some(term.kind),
+        // Bt-Ann
+        Expression::Annotation { expr, kind } => check(context, *expr, kind.clone()).map(|x| kind),
+        // Bt-True / Bt-False / etc
+        Expression::Constant { term } => Ok(term.kind),
+        // Bt-Var
         Expression::Variable { id } => {
             match context.get(&id) {
-                Some(term) => Some(term.clone().kind),
-                None => None
+                Some(term) => Ok(term.clone().kind),
+                None => Err(("failed to find variable in context", context, Type::Empty))
             }
         },
+        // Bt-App
         Expression::Application { func, arg } => {
-            // 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
-                    }
+            let expr = infer(context.clone(), *func)?;
+            match expr {
+                Type::Function { from, to } => {
+                    check(context, *arg, *from).map(|x| *to)
                 },
-                _ => None
+                _ => Err(("application abstraction is not a function type", context, Type::Empty))
             }
         },
-        // should not happen
-        Expression::Abstraction { param, func } => infer(context, *func),
+        Expression::Abstraction { param, func } => Err(("attempting to infer from an abstraction", context, Type::Empty)),
         // idk
         Expression::Conditional { if_cond, if_then, if_else } => {
-            if check(context.clone(), *if_cond, Type::Boolean) {
-                let kind = infer(context.clone(), *if_then);
-                if kind == infer(context, *if_else) {
-                    return kind;
-                }
+            check(context.clone(), *if_cond, Type::Boolean)?;
+            let if_then = infer(context.clone(), *if_then)?;
+            let if_else = infer(context.clone(), *if_else)?;
+            if if_then == if_else {
+                Ok(if_then)
+            } else {
+                Err(("if clauses of different types", context, Type::Empty))
             }
-            return None;
         }
     }
 }
 
 /// Evaluates an expression given a context (of variables) to a term.
 /// Panics on non-evaluatable code.
-pub fn execute(context: Context, expression: Expression) -> Result<Term, &'static str> {
+pub fn execute(context: Context, expression: Expression) -> Result<Term, (&'static str, Context)> {
     match expression {
         Expression::Annotation { expr, .. } => execute(context, *expr),
         Expression::Constant { term } => Ok(term),
         Expression::Variable { id } => {
             match context.get(&id) {
                 Some(term) => Ok(term.clone()),
-                None => Err("no such variable in context")
+                None => Err(("no such variable in context", context))
             }
         },
-        Expression::Abstraction { .. } => Err("attempting to execute an abstraction"),
+        Expression::Abstraction { .. } => Err(("attempting to execute an abstraction", context)),
         Expression::Application { func, arg } => {
             match *func {
                 Expression::Abstraction { param, func } => {
-                    let result = execute(context.clone(), *arg);
-                    match result {
-                        Ok(value) => {
-                            let mut context = context;
-                            context.insert(param, value);
-                            return execute(context, *func);
-                        },
-                        Err(e) => Err(e)
-                    }
+                    let value = execute(context.clone(), *arg)?;
+                    let mut context = context;
+                    context.insert(param, value);
+                    return execute(context, *func);
                 },
-                _ => Err("attempting to execute an application to nothing")
+                _ => Err(("attempting to execute an application to nothing", context))
             }
         },
         Expression::Conditional { if_cond, if_then, if_else } => {
             match execute(context.clone(), *if_cond) {
                 Ok(Term { val: 1, .. }) => execute(context, *if_then),
                 Ok(Term { val: 0, .. }) => execute(context, *if_else),
-                _ => Err("invalid type for a conditional")
+                _ => Err(("invalid type for a conditional", context))
             }
         }
     }