diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main.rs | 23 | ||||
| -rw-r--r-- | src/simple.rs | 108 |
2 files changed, 72 insertions, 59 deletions
diff --git a/src/main.rs b/src/main.rs index 8f93e51..bff203b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -21,16 +21,28 @@ fn main() { input.clear(); stdin().read_line(&mut input).unwrap(); - simple::infer(Context::new(), parser::parse(&input)); + match simple::infer(Context::new(), parser::parse(&input)) { + Ok(term) => println!("infers! {:?}", term), + Err(e) => println!("{:?}", e), + } }, - "c" | "t" | "check" | "typecheck" => { + "c" | "t" | "check" => { println!("enter fully annotated expression to typecheck"); print!("\x1b[1m====> \x1b[22m"); stdout().flush().unwrap(); input.clear(); stdin().read_line(&mut input).unwrap(); - simple::check(Context::new(), parser::parse(&input), Type::Empty); + let kind = simple::infer(Context::new(), parser::parse(&input)); + match kind { + Ok(kind) => { + match simple::check(Context::new(), parser::parse(&input), kind) { + Ok(_) => println!("checks!"), + Err(e) => println!("{:?}", e), + } + }, + Err(_) => println!("failed to infer high-level type!") + } }, "e" | "r" | "execute" | "run" => { println!("enter expression to execute"); @@ -39,7 +51,10 @@ fn main() { input.clear(); stdin().read_line(&mut input).unwrap(); - println!("{:?}", simple::execute(Context::new(), parser::parse(&input))); + match simple::execute(Context::new(), parser::parse(&input)) { + Ok(term) => println!("{:?}", term), + Err(e) => println!("{:?}", e) + } }, _ => println!("invalid option {}. please try again.", input.trim()) } diff --git a/src/simple.rs b/src/simple.rs index e794f93..4419680 100644 --- a/src/simple.rs +++ b/src/simple.rs @@ -4,18 +4,27 @@ use crate::ast::*; -pub fn check(context: Context, expression: Expression, target: Type) -> bool { +pub fn check(context: Context, expression: Expression, target: Type) -> Result<(), (&'static str, Context, Type)> { match expression { - // should never happen - Expression::Annotation { expr, kind } => (kind == target) && check(context, *expr, kind), - Expression::Constant { term } => term.kind == target, + Expression::Annotation { expr, kind } => Err(("attempting to typecheck an annotation", context, target)), + // Bt-CheckInfer + Expression::Constant { term } => { + if term.kind == target { + Ok(()) + } else { + Err(("constant is of wrong type", context, target)) + } + }, + // Bt-CheckInfer Expression::Variable { id } => { // in the future: extend to closures? nah probably not match context.get(&id) { - Some(term) if term.kind == target => true, - _ => false + Some(term) if term.kind == target => Ok(()), + Some(_) => Err(("variable is of wrong type", context, target)), + None => Err(("failed to find variable in context", context, target)) } }, + // Bt-Abs Expression::Abstraction { param, func } => { match target { Type::Function { from, to } => { @@ -23,99 +32,88 @@ pub fn check(context: Context, expression: Expression, target: Type) -> bool { context.insert(param, Term { val: 0, kind: *from }); // hack return check(context, *func, *to); }, - _ => false + _ => Err(("attempting to check an abstraction with a non-function type", context, target)) } }, - // should never happen - Expression::Application { func, arg } => check(context, *func, target), + Expression::Application { func, arg } => Err(("attempting to check an application", context, target)), + // T-If Expression::Conditional { if_cond, if_then, if_else } => { - check(context.clone(), *if_cond, Type::Boolean) && - check(context.clone(), *if_then, target.clone()) && - check(context.clone(), *if_else, target.clone()) + check(context.clone(), *if_cond, Type::Boolean)?; + check(context.clone(), *if_then, target.clone())?; + check(context.clone(), *if_else, target.clone())?; + return Ok(()); } } } // empty's gonna cause problems -pub fn infer(context: Context, expression: Expression) -> Option<Type> { +pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static str, Context, Type)> { match expression { - Expression::Annotation { expr, kind } => { - match check(context, *expr, kind.clone()) { - true => Some(kind), - false => None - } - }, - Expression::Constant { term } => Some(term.kind), + // Bt-Ann + Expression::Annotation { expr, kind } => check(context, *expr, kind.clone()).map(|x| kind), + // Bt-True / Bt-False / etc + Expression::Constant { term } => Ok(term.kind), + // Bt-Var Expression::Variable { id } => { match context.get(&id) { - Some(term) => Some(term.clone().kind), - None => None + Some(term) => Ok(term.clone().kind), + None => Err(("failed to find variable in context", context, Type::Empty)) } }, + // Bt-App Expression::Application { func, arg } => { - // Bt-App: - // \Gamma \derives t_1 \infer \tau_1 \to \tau_2, \Gamma \derives t_2 \check \tau_1 - // ------------------------------------------- - // \Gamma \derives t_1 t_2 \infer \tau_2 - match infer(context.clone(), *func) { - Some(Type::Function { from, to }) => { - match check(context, *arg, *from) { - true => Some(*to), - false => None - } + let expr = infer(context.clone(), *func)?; + match expr { + Type::Function { from, to } => { + check(context, *arg, *from).map(|x| *to) }, - _ => None + _ => Err(("application abstraction is not a function type", context, Type::Empty)) } }, - // should not happen - Expression::Abstraction { param, func } => infer(context, *func), + Expression::Abstraction { param, func } => Err(("attempting to infer from an abstraction", context, Type::Empty)), // idk Expression::Conditional { if_cond, if_then, if_else } => { - if check(context.clone(), *if_cond, Type::Boolean) { - let kind = infer(context.clone(), *if_then); - if kind == infer(context, *if_else) { - return kind; - } + 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) + } else { + Err(("if clauses of different types", context, Type::Empty)) } - return None; } } } /// Evaluates an expression given a context (of variables) to a term. /// Panics on non-evaluatable code. -pub fn execute(context: Context, expression: Expression) -> Result<Term, &'static str> { +pub fn execute(context: Context, expression: Expression) -> Result<Term, (&'static str, Context)> { 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") + None => Err(("no such variable in context", context)) } }, - Expression::Abstraction { .. } => Err("attempting to execute an abstraction"), + Expression::Abstraction { .. } => Err(("attempting to execute an abstraction", context)), Expression::Application { func, arg } => { match *func { Expression::Abstraction { param, func } => { - let result = execute(context.clone(), *arg); - match result { - Ok(value) => { - let mut context = context; - context.insert(param, value); - return execute(context, *func); - }, - Err(e) => Err(e) - } + 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") + _ => Err(("attempting to execute an application to nothing", context)) } }, Expression::Conditional { if_cond, if_then, if_else } => { match execute(context.clone(), *if_cond) { Ok(Term { val: 1, .. }) => execute(context, *if_then), Ok(Term { val: 0, .. }) => execute(context, *if_else), - _ => Err("invalid type for a conditional") + _ => Err(("invalid type for a conditional", context)) } } } |