aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2023-04-11 02:29:23 +0000
committerJJ2023-04-11 02:29:23 +0000
commit0629c20b6bff68d2719f414a830afe2b8ce5eac1 (patch)
treeb425dedc57b98b8f4d45f2cbf8449a159d4e8188
parentbe249407be3e4f63548bab9e0cc23ee1daf82a4a (diff)
bidirectional working
-rw-r--r--src/main.rs23
-rw-r--r--src/simple.rs108
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))
}
}
}