aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser.rs22
-rw-r--r--src/simple.rs73
-rw-r--r--src/util.rs2
-rw-r--r--tests/test_checking.rs6
4 files changed, 55 insertions, 48 deletions
diff --git a/src/parser.rs b/src/parser.rs
index add31d9..6e6a262 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -47,21 +47,23 @@ pub fn parse_lambda(input: &str) -> Result<Expression, peg::error::ParseError<pe
}
}
}
- // fucking awful but i don't know another way
- // k:("empty" / "unit" / etc) returns ()
- // and i can't seem to match and raise a parse error
- // so ¯\_(ツ)_/¯
- rule empty() -> Type = k:"empty" {Type::Empty}
- rule unit() -> Type = k:"unit" {Type::Unit}
- rule boolean() -> Type = k:"bool" {Type::Boolean}
- rule natural() -> Type = k:"nat" {Type::Natural}
- rule integer() -> Type = k:"int" {Type::Integer}
+ rule primitive() -> Type
+ = k:$("empty" / "unit" / "bool" / "nat" / "int") {
+ match k {
+ "empty" => Type::Empty,
+ "unit" => Type::Unit,
+ "bool" => Type::Boolean,
+ "nat" => Type::Natural,
+ "int" => Type::Integer,
+ _ => Type::Empty
+ }
+ }
// fixme: brackets are necessary here
rule function() -> Type = "(" f:kind() " "* "->" " "* t:kind() ")" {
Type::Function { from: Box::new(f), to: Box::new(t) }
}
rule kind() -> Type
- = k:(function() / empty() / unit() / boolean() / natural() / integer()) {
+ = k:(function() / primitive()) {
k
}
rule ann() -> Expression
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
}
}
diff --git a/src/util.rs b/src/util.rs
index 68a8a19..5011ac7 100644
--- a/src/util.rs
+++ b/src/util.rs
@@ -1,4 +1,4 @@
-#![allow(non_snake_case)]
+#![allow(non_snake_case, non_upper_case_globals)]
use crate::ast::*;
diff --git a/tests/test_checking.rs b/tests/test_checking.rs
index 60bb6da..a4b5fd3 100644
--- a/tests/test_checking.rs
+++ b/tests/test_checking.rs
@@ -55,7 +55,7 @@ fn test_checking() {
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(()));
- assert_eq!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Nat, Func(Nat, Nat)))), Ok(()));
- assert_eq!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Unit, Func(Unit, Unit)))), Ok(()));
+ assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Int, Func(Int, Int)))).is_ok());
+ assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Nat, Func(Nat, Nat)))).is_ok());
+ assert!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Unit, Func(Unit, Unit)))).is_ok());
}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-11-21 23:08:54 +0000