aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2023-04-13 01:30:35 +0000
committerJJ2023-04-13 01:30:35 +0000
commit56f47bb2e5816de7630569a8825914d0620983cc (patch)
treecf413d589a389d3ddd8f9a9321aed7cb7d30c215
parentfb1c4cd2b8e2efe4b03e8c93f2a69d712a96aff7 (diff)
subtyping wip
-rw-r--r--src/ast.rs5
-rw-r--r--src/simple.rs41
-rw-r--r--src/util.rs1
-rw-r--r--tests/test_checking.rs4
4 files changed, 39 insertions, 12 deletions
diff --git a/src/ast.rs b/src/ast.rs
index 0a2afdb..bf34d19 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -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;
diff --git a/tests/test_checking.rs b/tests/test_checking.rs
index 0ec6acd..60bb6da 100644
--- a/tests/test_checking.rs
+++ b/tests/test_checking.rs
@@ -51,8 +51,8 @@ fn test_checking() {
assert!(check(Context::new(), parse_lambda(basic_application).unwrap(), Int).is_ok());
assert!(check(Context::new(), parse_lambda(correct_cond_abs).unwrap(), Func(Bool, Int)).is_ok());
assert!(check(Context::new(), parse_lambda(correct_cond).unwrap(), Nat).is_ok());
- assert!(check(Context::new(), parse_lambda(incorrect_branches).unwrap(), Empty).is_err());
- assert!(check(Context::new(), parse_lambda(incorrect_cond_abs).unwrap(), Empty).is_err());
+ assert!(check(Context::new(), parse_lambda(incorrect_branches).unwrap(), Unit).is_err());
+ 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(()));