diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.rs | 5 | ||||
| -rw-r--r-- | src/simple.rs | 41 | ||||
| -rw-r--r-- | src/util.rs | 1 |
3 files changed, 37 insertions, 10 deletions
@@ -25,14 +25,15 @@ pub type Value = u64; #[derive(Debug, Clone, PartialEq, Eq)] pub enum Type { Empty, + Error, Unit, Boolean, Natural, Integer, // Float, // String, - // Enum(Vec<Type>), - // Record(Vec<Type>), + Enum(Vec<Type>), + Record(HashMap<Identifier, Type>), Function{from: Box<Type>, to: Box<Type>}, } 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, + } +} diff --git a/src/util.rs b/src/util.rs index b2b3035..68a8a19 100644 --- a/src/util.rs +++ b/src/util.rs @@ -66,6 +66,7 @@ pub fn Func(from: Type, to: Type) -> Type { } pub const Empty: Type = Type::Empty; +pub const Error: Type = Type::Empty; pub const Unit: Type = Type::Unit; pub const Bool: Type = Type::Boolean; pub const Nat: Type = Type::Natural; |