begin bidirectional implementation

3 files changed, 47 insertions, 6 deletions

diff --git a/src/main.rs b/src/main.rs
index 6d74f54..8f93e51 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -30,7 +30,7 @@ fn main() {
 
                 input.clear();
                 stdin().read_line(&mut input).unwrap();
-                simple::check(Context::new(), parser::parse(&input));
+                simple::check(Context::new(), parser::parse(&input), Type::Empty);
             },
             "e" | "r" | "execute" | "run" => {
                 println!("enter expression to execute");
diff --git a/src/parser.rs b/src/parser.rs
index ef7e28d..917df66 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -92,6 +92,7 @@ pub fn parse_str(input: &str) -> Result<Expression, peg::error::ParseError<peg::
 }
 
 /// Parses a Nim-like language into an AST.
+#[allow(unused_variables)]
 pub fn parse_file(path: &str) -> Vec<Expression> {
     todo!();
 }
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 {