diff options
Diffstat (limited to 'src/simple.rs')
| -rw-r--r-- | src/simple.rs | 73 |
1 files changed, 39 insertions, 34 deletions
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 } } |