diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/simple.rs | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/simple.rs b/src/simple.rs index 22708a4..dad9a84 100644 --- a/src/simple.rs +++ b/src/simple.rs @@ -6,11 +6,16 @@ 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 } => Err(("attempting to typecheck an annotation", context, target)), + Expression::Annotation { expr, kind } => match 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 { true => Ok(()), - false => Err(("constant is of wrong type", context, target)) + false => Ok(()) // all our constants are Empty for now + // false => Err(("constant is of wrong type", context, target)) }, // Bt-CheckInfer // in the future: extend to closures? nah probably not @@ -28,7 +33,11 @@ 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 } => Err(("attempting to check an application", context, target)), + Expression::Application { func, arg } => match infer(context.clone(), Expression::Application { func, arg })? == target { + true => Ok(()), + false => Err(("inferred type does not match target", context, target)) + }, // T-If Expression::Conditional { if_cond, if_then, if_else } => { check(context.clone(), *if_cond, Type::Boolean)?; |