Skip to content

Commit

Permalink
minor cleanups
Browse files Browse the repository at this point in the history
  • Loading branch information
@omentic
omentic committed Apr 13, 2023
1 parent 56f47bb commit 188631f
Show file tree
Hide file tree
Showing 4 changed files with 55 additions and 48 deletions.
22 changes: 12 additions & 10 deletions src/parser.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
73 changes: 39 additions & 34 deletions src/simple.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand All @@ -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)),
Expand All @@ -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 } => {
Expand All @@ -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
Expand All @@ -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)?;
Expand All @@ -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) {
Expand All @@ -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
}
}
2 changes: 1 addition & 1 deletion src/util.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#![allow(non_snake_case)]
#![allow(non_snake_case, non_upper_case_globals)]

use crate::ast::*;

Expand Down
6 changes: 3 additions & 3 deletions tests/test_checking.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}

0 comments on commit 188631f

Please sign in to comment.