minor cleanupscpsc539

4 files changed, 55 insertions, 48 deletions

diff --git a/src/parser.rs b/src/parser.rs
index add31d9..6e6a262 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -47,21 +47,23 @@ pub fn parse_lambda(input: &str) -> Result<Expression, peg::error::ParseError<pe
                     }
                 }
             }
-            // fucking awful but i don't know another way
-            // k:("empty" / "unit" / etc) returns ()
-            // and i can't seem to match and raise a parse error
-            // so ¯\_(ツ)_/¯
-            rule empty() -> Type = k:"empty" {Type::Empty}
-            rule unit() -> Type = k:"unit" {Type::Unit}
-            rule boolean() -> Type = k:"bool" {Type::Boolean}
-            rule natural() -> Type = k:"nat" {Type::Natural}
-            rule integer() -> Type = k:"int" {Type::Integer}
+            rule primitive() -> Type
+            = k:$("empty" / "unit" / "bool" / "nat" / "int") {
+                match k {
+                    "empty" => Type::Empty,
+                    "unit" => Type::Unit,
+                    "bool" => Type::Boolean,
+                    "nat" => Type::Natural,
+                    "int" => Type::Integer,
+                    _ => Type::Empty
+                }
+            }
             // fixme: brackets are necessary here
             rule function() -> Type = "(" f:kind() " "* "->" " "* t:kind() ")" {
                 Type::Function { from: Box::new(f), to: Box::new(t) }
             }
             rule kind() -> Type
-             = k:(function() / empty() / unit() / boolean() / natural() / integer()) {
+             = k:(function() / primitive()) {
                 k
             }
             rule ann() -> Expression
diff --git a/src/simple.rs b/src/simple.rs
index 7fe8989..6a40b67 100644
--- a/src/simple.rs
+++ b/src/simple.rs
@@ -6,10 +6,13 @@ use crate::ast::*;
 
 pub fn check(context: Context, expression: Expression, target: Type) -> Result<(), (&'static str, Context, Type)> {
     match expression {
-        // Expression::Annotation { expr, kind } => Err(("attempting to typecheck an annotation", context, target)),
-        Expression::Annotation { expr, kind } => match subtype(&infer(context.clone(), Expression::Annotation { expr, kind })?, &target) {
-            true => Ok(()),
-            false => Err(("inferred type from annotation does not match target", context, target))
+        // fall through to inference mode
+        Expression::Annotation { expr, kind } => {
+            let result = infer(context.clone(), Expression::Annotation { expr, kind })?;
+            return match subtype(&result, &target) {
+                true => Ok(()),
+                false => Err(("inferred type does not match target", context, target))
+            }
         },
         // Bt-CheckInfer
         Expression::Constant { term } => match subtype(&term.kind, &target) {
@@ -18,7 +21,6 @@ pub fn check(context: Context, expression: Expression, target: Type) -> Result<(
             // false => Err(("constant is of wrong type", context, target))
         },
         // Bt-CheckInfer
-        // in the future: extend to closures? nah probably not
         Expression::Variable { id } => match context.get(&id) {
             Some(term) if subtype(&term.kind, &target) => Ok(()),
             Some(_) => Err(("variable is of wrong type", context, target)),
@@ -33,10 +35,13 @@ pub fn check(context: Context, expression: Expression, target: Type) -> Result<(
             },
             _ => Err(("attempting to check an abstraction with a non-function type", context, target))
         },
-        // Expression::Application { func, arg } => Err(("attempting to check an application", context, target)),
-        Expression::Application { func, arg } => match subtype(&infer(context.clone(), Expression::Application { func, arg })?, &target) {
-            true => Ok(()),
-            false => Err(("inferred type does not match target", context, target))
+        // fall through to inference mode
+        Expression::Application { func, arg } => {
+            let result = &infer(context.clone(), Expression::Application { func, arg })?;
+            return match subtype(&result, &target) {
+                true => Ok(()),
+                false => Err(("inferred type does not match target", context, target))
+            }
         },
         // T-If
         Expression::Conditional { if_cond, if_then, if_else } => {
@@ -48,7 +53,6 @@ pub fn check(context: Context, expression: Expression, target: Type) -> Result<(
     }
 }
 
-// empty's gonna cause problems
 pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static str, Context, Type)> {
     match expression {
         // Bt-Ann
@@ -62,12 +66,14 @@ pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static
         },
         // Bt-App
         Expression::Application { func, arg } => match infer(context.clone(), *func)? {
-            Type::Function { from, to } => {
-                check(context, *arg, *from).map(|x| *to)
-            },
+            Type::Function { from, to } => check(context, *arg, *from).map(|x| *to),
             _ => Err(("application abstraction is not a function type", context, Type::Empty))
         },
-        Expression::Abstraction { param, func } => Err(("attempting to infer from an abstraction", context, Type::Empty)),
+        // inference from an abstraction is always an error
+        // we could try and infer the func without adding the parameter to scope:
+        // but this is overwhelmingly likely to be an error, so just report it now.
+        Expression::Abstraction { param, func } =>
+            Err(("attempting to infer from an abstraction", context, Type::Empty)),
         // idk
         Expression::Conditional { if_cond, if_then, if_else } => {
             check(context.clone(), *if_cond, Type::Boolean)?;
@@ -87,23 +93,19 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, (&'stat
     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", context))
-            }
+        Expression::Variable { id } => match context.get(&id) {
+            Some(term) => Ok(term.clone()),
+            None => Err(("no such variable in context", context))
         },
         Expression::Abstraction { .. } => Err(("attempting to execute an abstraction", context)),
-        Expression::Application { func, arg } => {
-            match *func {
-                Expression::Abstraction { param, func } => {
-                    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", context))
+        Expression::Application { func, arg } => match *func {
+            Expression::Abstraction { param, func } => {
+                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", context))
         },
         Expression::Conditional { if_cond, if_then, if_else } => {
             match execute(context.clone(), *if_cond) {
@@ -122,21 +124,24 @@ pub fn subtype(is: &Type, of: &Type) -> bool {
             // width, depth, and permutation
             for (key, of_value) in of_fields {
                 match is_fields.get(key) {
-                    Some(is_value) => if !subtype(is_value, of_value) {
-                        return false;
-                    },
+                    Some(is_value) => {
+                        if !subtype(is_value, of_value) {
+                            return false;
+                        }
+                    }
                     None => return false
                 }
             }
             return true;
         },
-        (Type::Function { from: is_from, to: is_to }, Type::Function { from: of_from, to: of_to }) => {
+        (Type::Function { from: is_from, to: is_to },
+         Type::Function { from: of_from, to: of_to }) => {
             subtype(of_from, is_from) && subtype(is_to, of_to)
-        }
+        },
         (Type::Natural, Type::Integer) => true, // obviously not, but let's pretend
         (_, Type::Empty) => true,
         (Type::Error, _) => true,
         (_, _) if is == of => true,
-        (_, _) => false,
+        (_, _) => false
     }
 }
diff --git a/src/util.rs b/src/util.rs
index 68a8a19..5011ac7 100644
--- a/src/util.rs
+++ b/src/util.rs
@@ -1,4 +1,4 @@
-#![allow(non_snake_case)]
+#![allow(non_snake_case, non_upper_case_globals)]
 
 use crate::ast::*;
 
diff --git a/tests/test_checking.rs b/tests/test_checking.rs
index 60bb6da..a4b5fd3 100644
--- a/tests/test_checking.rs
+++ b/tests/test_checking.rs
@@ -55,7 +55,7 @@ fn test_checking() {
     assert!(check(Context::new(), parse_lambda(incorrect_cond_abs).unwrap(), Error).is_err());
 
     // more fun
-    assert_eq!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Int, Func(Int, Int)))), Ok(()));
-    assert_eq!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Nat, Func(Nat, Nat)))), Ok(()));
-    assert_eq!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Unit, Func(Unit, Unit)))), Ok(()));
+    assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Int, Func(Int, Int)))).is_ok());
+    assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Nat, Func(Nat, Nat)))).is_ok());
+    assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Unit, Func(Unit, Unit)))).is_ok());
 }