diff options
| -rw-r--r-- | src/ast.rs | 9 | ||||
| -rw-r--r-- | src/simple.rs | 77 |
2 files changed, 43 insertions, 43 deletions
@@ -12,16 +12,17 @@ pub enum Expression { Annotation{expr: Box<Expression>, kind: Type}, Constant{term: Term}, Variable{id: Identifier}, + // note: we keep parameters as an Identifier because we annotate the WHOLE Abstraction Abstraction{param: Identifier, func: Box<Expression>}, Application{func: Box<Expression>, arg: Box<Expression>}, Conditional{if_cond: Box<Expression>, if_then: Box<Expression>, if_else: Box<Expression>} } // _every_ type in our language is represented as this and interpreted as a type. -// how to store more data than fits... hmm +// how to store more data than fits... hmm... a problem for later pub type Value = u64; -#[derive(Debug, Copy, Clone, PartialEq, Eq)] +#[derive(Debug, Clone, PartialEq, Eq)] pub enum Type { Empty, Unit, @@ -32,11 +33,11 @@ pub enum Type { // String, // Enum(Vec<Type>), // Record(Vec<Type>), - // Function{from: Box<Type>, to: Box<Type>}, + Function{from: Box<Type>, to: Box<Type>}, } // this means that functions cannot have types? unless we put them as empty values ig -#[derive(Debug, Copy, Clone, PartialEq, Eq)] +#[derive(Debug, Clone, PartialEq, Eq)] pub struct Term { pub val: Value, pub kind: Type, // currently useless / redundant: will be useful for casting diff --git a/src/simple.rs b/src/simple.rs index 30a609b..e794f93 100644 --- a/src/simple.rs +++ b/src/simple.rs @@ -6,80 +6,79 @@ use crate::ast::*; pub fn check(context: Context, expression: Expression, target: Type) -> bool { match expression { - Expression::Annotation { expr, kind } => kind == target, + // should never happen + Expression::Annotation { expr, kind } => (kind == target) && check(context, *expr, kind), Expression::Constant { term } => term.kind == target, Expression::Variable { id } => { + // in the future: extend to closures? nah probably not match context.get(&id) { - Some(term) => term.kind == target, - None => false, + Some(term) if term.kind == target => true, + _ => false } }, - // fixme: i don't think this works Expression::Abstraction { param, func } => { - todo!() - }, - Expression::Application { func, arg } => { - match *func { - Expression::Abstraction { param, func } => { + match target { + Type::Function { from, to } => { let mut context = context; - context.insert(param, Term { val: 0, kind: arg.kind }); - return check(context, *func, target); + context.insert(param, Term { val: 0, kind: *from }); // hack + return check(context, *func, *to); }, _ => false } }, + // should never happen + Expression::Application { func, arg } => check(context, *func, target), Expression::Conditional { if_cond, if_then, if_else } => { check(context.clone(), *if_cond, Type::Boolean) && - check(context.clone(), *if_then, target) && - check(context.clone(), *if_else, target) - }, + check(context.clone(), *if_then, target.clone()) && + check(context.clone(), *if_else, target.clone()) + } } } // empty's gonna cause problems pub fn infer(context: Context, expression: Expression) -> Option<Type> { match expression { - Expression::Annotation { expr, kind } => Some(kind), + Expression::Annotation { expr, kind } => { + match check(context, *expr, kind.clone()) { + true => Some(kind), + false => None + } + }, Expression::Constant { term } => Some(term.kind), Expression::Variable { id } => { match context.get(&id) { - Some(term) => Some(term.kind), + Some(term) => Some(term.clone().kind), None => None } }, - // this is probably bad. we don't know what type param is since it's a raw identifier. - // to fix: probably either require param to be annotated (good idea?), or - // allow arbitrary expressions (bad idea?) - // edit: turns out the typed lambda calculus actually REQUIREs annotations on parameters lmao - Expression::Abstraction { param, func } => { - let mut context = context; - context.insert(param, Term { val: 0, kind: Type::Empty}); // even worse hack - return infer(context, *func); - }, Expression::Application { func, arg } => { - match *func { - Expression::Abstraction { param, func } => { - match infer(context.clone(), *arg) { - Some(arg) => { - let mut context = context; - context.insert(param, Term { val: 0, kind: arg }); // hack - return infer(context, *func); - }, - None => None + // 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 } }, _ => None } }, + // should not happen + Expression::Abstraction { param, func } => infer(context, *func), + // idk Expression::Conditional { if_cond, if_then, if_else } => { - if infer(context.clone(), *if_cond) == Some(Type::Boolean) { + if check(context.clone(), *if_cond, Type::Boolean) { let kind = infer(context.clone(), *if_then); - if infer(context, *if_else) == kind { + if kind == infer(context, *if_else) { return kind; } } return None; - }, + } } } @@ -91,7 +90,7 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, &'stati Expression::Constant { term } => Ok(term), Expression::Variable { id } => { match context.get(&id) { - Some(term) => Ok(*term), + Some(term) => Ok(term.clone()), None => Err("no such variable in context") } }, @@ -118,6 +117,6 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, &'stati Ok(Term { val: 0, .. }) => execute(context, *if_else), _ => Err("invalid type for a conditional") } - }, + } } } |