summaryrefslogtreecommitdiff
path: root/src/simple.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/simple.rs')
-rw-r--r--src/simple.rs41
1 files changed, 33 insertions, 8 deletions
diff --git a/src/simple.rs b/src/simple.rs
index dad9a84..7fe8989 100644
--- a/src/simple.rs
+++ b/src/simple.rs
@@ -7,12 +7,12 @@ 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 infer(context.clone(), Expression::Annotation { expr, kind })? == 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))
},
// Bt-CheckInfer
- Expression::Constant { term } => match term.kind == target {
+ Expression::Constant { term } => match subtype(&term.kind, &target) {
true => Ok(()),
false => Ok(()) // all our constants are Empty for now
// false => Err(("constant is of wrong type", context, target))
@@ -20,7 +20,7 @@ pub fn check(context: Context, expression: Expression, target: Type) -> Result<(
// Bt-CheckInfer
// in the future: extend to closures? nah probably not
Expression::Variable { id } => match context.get(&id) {
- Some(term) if term.kind == target => Ok(()),
+ Some(term) if subtype(&term.kind, &target) => Ok(()),
Some(_) => Err(("variable is of wrong type", context, target)),
None => Err(("failed to find variable in context", context, target))
},
@@ -34,7 +34,7 @@ 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 infer(context.clone(), Expression::Application { func, arg })? == 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))
},
@@ -73,8 +73,8 @@ pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static
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)
+ if subtype(&if_then, &if_else) && subtype(&if_else, &if_then) {
+ Ok(if_then) // fixme: should be the join
} else {
Err(("if clauses of different types", context, Type::Empty))
}
@@ -82,8 +82,7 @@ pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static
}
}
-/// Evaluates an expression given a context (of variables) to a term.
-/// Panics on non-evaluatable code.
+/// Evaluates an expression given a context (of variables) to a term, or fails.
pub fn execute(context: Context, expression: Expression) -> Result<Term, (&'static str, Context)> {
match expression {
Expression::Annotation { expr, .. } => execute(context, *expr),
@@ -115,3 +114,29 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, (&'stat
}
}
}
+
+/// The subtyping relation between any two types.
+pub fn subtype(is: &Type, of: &Type) -> bool {
+ match (is, of) {
+ (Type::Record(is_fields), Type::Record(of_fields)) => {
+ // 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;
+ },
+ None => return false
+ }
+ }
+ return true;
+ },
+ (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,
+ }
+}