aboutsummaryrefslogtreecommitdiff
path: root/src/bidirectional.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/bidirectional.rs')
-rw-r--r--src/bidirectional.rs203
1 files changed, 103 insertions, 100 deletions
diff --git a/src/bidirectional.rs b/src/bidirectional.rs
index 493ae2f..d62267c 100644
--- a/src/bidirectional.rs
+++ b/src/bidirectional.rs
@@ -2,119 +2,122 @@
use crate::ast::*;
-/// Checking judgement: takes an expression and a type to check against and calls out to `infer` as needed.
-pub fn check(context: &Context, expression: Expression, target: &Type) -> Result<(), String> {
- match expression {
- // fall through to inference mode
- Expression::Annotation { expr, kind } => {
- let result = infer(context, Expression::Annotation { expr, kind })?;
- return match subtype(&result, &target) {
- true => Ok(()),
- false => Err(format!("inferred type {result} does not match target {target}"))
- }
- },
- // Bt-CheckInfer
- Expression::Constant { term } => match subtype(&convert(&term)?, &target) {
- true => Ok(()),
- false => Err(format!("constant is of wrong type, expected {target}"))
- // false => Ok(()) // all our constants are Empty for now
- },
- // Bt-CheckInfer
- Expression::Variable { id } => match context.get(&id) {
- Some(term) if subtype(&convert(term)?, &target) => Ok(()),
- Some(_) => Err(format!("variable {id} is of wrong type")),
- None => Err(format!("failed to find variable {id} in context"))
- },
- // Bt-Abs
- Expression::Abstraction { param, func } => match target {
- Type::Function { from, to } => {
- let mut context = context.clone();
- context.insert(param, default(from)?);
- return check(&context, *func, &to);
+impl Context {
+ /// Checking judgement: takes an expression and a type to check against and calls out to `infer` as needed.
+ pub fn check(&self, expression: Expression, target: &Type) -> Result<()> {
+ match expression {
+ // fall through to inference mode
+ Expression::Annotation { expr, kind } => {
+ let result = self.infer(Expression::Annotation { expr, kind })?;
+ return match result.subtype(&target) {
+ true => Ok(()),
+ false => Err(format!("inferred type {result} does not match target {target}").into())
+ }
},
- _ => Err(format!("attempting to check an abstraction with a non-function type {target}"))
- },
- // fall through to inference mode
- Expression::Application { func, arg } => {
- let result = &infer(context, Expression::Application { func, arg })?;
- return match subtype(&result, &target) {
+ // Bt-CheckInfer
+ Expression::Constant { term } => match &term.convert()?.subtype(&target) {
true => Ok(()),
- false => Err(format!("inferred type {result} does not match {target}"))
+ false => Err(format!("constant is of wrong type, expected {target}").into())
+ // false => Ok(()) // all our constants are Empty for now
+ },
+ // Bt-CheckInfer
+ Expression::Variable { id } => match self.get(&id) {
+ Some(term) if term.convert()?.subtype(&target) => Ok(()),
+ Some(_) => Err(format!("variable {id} is of wrong type").into()),
+ None => Err(format!("failed to find variable {id} in context").into())
+ },
+ // Bt-Abs
+ Expression::Abstraction { param, func } => match target {
+ Type::Function { from, to } => {
+ let mut context = self.clone();
+ context.insert(param, from.default()?);
+ return context.check(*func, &to);
+ },
+ _ => Err(format!("attempting to check an abstraction with a non-function type {target}").into())
+ },
+ // fall through to inference mode
+ Expression::Application { func, arg } => {
+ let result = &self.infer(Expression::Application { func, arg })?;
+ return match result.subtype(&target) {
+ true => Ok(()),
+ false => Err(format!("inferred type {result} does not match {target}").into())
+ }
+ },
+ // T-If
+ Expression::Conditional { if_cond, if_then, if_else } => {
+ self.check(*if_cond, &Type::Boolean)?;
+ self.check(*if_then, &target)?;
+ self.check(*if_else, &target)?;
+ return Ok(());
}
- },
- // T-If
- Expression::Conditional { if_cond, if_then, if_else } => {
- check(context, *if_cond, &Type::Boolean)?;
- check(context, *if_then, &target)?;
- check(context, *if_else, &target)?;
- return Ok(());
}
}
-}
-/// Inference judgement: takes an expression and attempts to infer the associated type.
-pub fn infer(context: &Context, expression: Expression) -> Result<Type, String> {
- match expression {
- // Bt-Ann
- Expression::Annotation { expr, kind } => check(context, *expr, &kind).map(|x| kind),
- // Bt-True / Bt-False / etc
- Expression::Constant { term } => convert(&term),
- // Bt-Var
- Expression::Variable { id } => match context.get(&id) {
- Some(term) => infer(&Context::new(), Expression::Constant { term: term.clone() }),
- None => Err(format!("failed to find variable in context {context:?}"))
- },
- // Bt-App
- Expression::Application { func, arg } => match infer(context, *func)? {
- Type::Function { from, to } => check(context, *arg, &*from).map(|x| *to),
- _ => Err(format!("application abstraction is not a function type"))
- },
- // 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(format!("attempting to infer from an abstraction")),
- // idk
- Expression::Conditional { if_cond, if_then, if_else } => {
- check(context, *if_cond, &Type::Boolean)?;
- let if_then = infer(context, *if_then)?;
- let if_else = infer(context, *if_else)?;
- if subtype(&if_then, &if_else) && subtype(&if_else, &if_then) {
- Ok(if_then) // fixme: should be the join
- } else {
- Err(format!("if clauses of different types: {if_then} and {if_else}"))
+ /// Inference judgement: takes an expression and attempts to infer the associated type.
+ pub fn infer(&self, expression: Expression) -> Result<Type> {
+ match expression {
+ // Bt-Ann
+ Expression::Annotation { expr, kind } => self.check(*expr, &kind).map(|x| kind),
+ // Bt-True / Bt-False / etc
+ Expression::Constant { term } => term.convert(),
+ // Bt-Var
+ Expression::Variable { id } => match self.get(&id) {
+ Some(term) => Context::new().infer(Expression::Constant { term: term.clone() }),
+ None => Err(format!("failed to find variable in context {self:?}").into())
+ },
+ // Bt-App
+ Expression::Application { func, arg } => match self.infer(*func)? {
+ Type::Function { from, to } => self.check(*arg, &*from).map(|x| *to),
+ _ => Err(format!("application abstraction is not a function type").into())
+ },
+ // 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(format!("attempting to infer from an abstraction").into()),
+ // idk
+ Expression::Conditional { if_cond, if_then, if_else } => {
+ self.check(*if_cond, &Type::Boolean)?;
+ let if_then = self.infer(*if_then)?;
+ let if_else = self.infer(*if_else)?;
+ if if_then.subtype(&if_else) && if_else.subtype(&if_then) {
+ Ok(if_then) // fixme: should be the join
+ } else {
+ Err(format!("if clauses of different types: {if_then} and {if_else}").into())
+ }
}
}
}
}
-/// 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;
+impl Type {
+ /// The subtyping relation between any two types.
+ pub fn subtype(&self, other: &Self) -> bool {
+ match (self, other) {
+ (Type::Struct(is_fields), Type::Struct(of_fields)) => {
+ // width, depth, and permutation
+ for (key, of_value) in of_fields {
+ match is_fields.get(key) {
+ Some(is_value) => {
+ if !is_value.subtype(of_value) {
+ return false;
+ }
}
+ None => return false
}
- None => return false
}
- }
- return true;
- },
- (Type::Enum(is_variants), Type::Enum(of_variants)) => false, // fixme
- (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
+ return true;
+ },
+ (Type::Union(is_variants), Type::Union(of_variants)) => false, // fixme
+ (Type::Function { from: is_from, to: is_to },
+ Type::Function { from: of_from, to: of_to }) => {
+ of_from.subtype(is_from) && is_to.subtype(of_to)
+ },
+ (Type::Natural, Type::Integer) => true, // obviously not, but let's pretend
+ (_, Type::Empty) => true,
+ (Type::Error, _) => true,
+ (_, _) if self == other => true,
+ (_, _) => false
+ }
}
}
-
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-10-16 10:26:37 +0000