diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser.rs | 22 | ||||
| -rw-r--r-- | src/simple.rs | 73 | ||||
| -rw-r--r-- | src/util.rs | 2 |
3 files changed, 52 insertions, 45 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::*; |