From 488bbc6816cbbe8a0ab95ce6c6fd391e9c9351c4 Mon Sep 17 00:00:00 2001
From: JJ
Date: Sun, 9 Apr 2023 17:33:33 -0700
Subject: bidirectional wtf

---
 src/simple.rs | 50 ++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 44 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/simple.rs b/src/simple.rs
index cedc016..30a609b 100644
--- a/src/simple.rs
+++ b/src/simple.rs
@@ -14,16 +14,32 @@ pub fn check(context: Context, expression: Expression, target: Type) -> bool {
                 None => false,
             }
         },
-        Expression::Abstraction { param, func } => todo!(),
-        Expression::Application { func, arg } => todo!(),
-        Expression::Conditional { if_cond, if_then, if_else } => todo!(),
+        // fixme: i don't think this works
+        Expression::Abstraction { param, func } => {
+            todo!()
+        },
+        Expression::Application { func, arg } => {
+            match *func {
+                Expression::Abstraction { param, func } => {
+                    let mut context = context;
+                    context.insert(param, Term { val: 0, kind: arg.kind });
+                    return check(context, *func, target);
+                },
+                _ => false
+            }
+        },
+        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)
+        },
     }
 }
 
 // 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 } => Some(kind),
         Expression::Constant { term } => Some(term.kind),
         Expression::Variable { id } => {
             match context.get(&id) {
@@ -31,8 +47,30 @@ pub fn infer(context: Context, expression: Expression) -> Option<Type> {
                 None => None
             }
         },
-        Expression::Abstraction { param, func } => return None,
-        Expression::Application { func, arg } => return 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
+                    }
+                },
+                _ => 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);
-- 
cgit v1.2.3-70-g09d2