diff options
| -rw-r--r-- | src/main.rs | 2 | ||||
| -rw-r--r-- | src/parser.rs | 1 | ||||
| -rw-r--r-- | src/simple.rs | 50 |
3 files changed, 47 insertions, 6 deletions
diff --git a/src/main.rs b/src/main.rs index 6d74f54..8f93e51 100644 --- a/src/main.rs +++ b/src/main.rs @@ -30,7 +30,7 @@ fn main() { input.clear(); stdin().read_line(&mut input).unwrap(); - simple::check(Context::new(), parser::parse(&input)); + simple::check(Context::new(), parser::parse(&input), Type::Empty); }, "e" | "r" | "execute" | "run" => { println!("enter expression to execute"); diff --git a/src/parser.rs b/src/parser.rs index ef7e28d..917df66 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -92,6 +92,7 @@ pub fn parse_str(input: &str) -> Result<Expression, peg::error::ParseError<peg:: } /// Parses a Nim-like language into an AST. +#[allow(unused_variables)] pub fn parse_file(path: &str) -> Vec<Expression> { todo!(); } diff --git a/src/simple.rs b/src/simple.rs index b7ef94a..cedc016 100644 --- a/src/simple.rs +++ b/src/simple.rs @@ -1,13 +1,48 @@ // Simple bidirectional type checking +#![allow(unused_variables)] + use crate::ast::*; -pub fn infer(context: Context, expression: Expression) { - todo!(); +pub fn check(context: Context, expression: Expression, target: Type) -> bool { + match expression { + Expression::Annotation { expr, kind } => kind == target, + Expression::Constant { term } => term.kind == target, + Expression::Variable { id } => { + match context.get(&id) { + Some(term) => term.kind == target, + None => false, + } + }, + Expression::Abstraction { param, func } => todo!(), + Expression::Application { func, arg } => todo!(), + Expression::Conditional { if_cond, if_then, if_else } => todo!(), + } } -pub fn check(context: Context, expression: Expression) { - todo!(); +// empty's gonna cause problems +pub fn infer(context: Context, expression: Expression) -> Option<Type> { + match expression { + Expression::Annotation { expr, kind } => Some(kind), + Expression::Constant { term } => Some(term.kind), + Expression::Variable { id } => { + match context.get(&id) { + Some(term) => Some(term.kind), + None => None + } + }, + Expression::Abstraction { param, func } => return None, + Expression::Application { func, arg } => return None, + Expression::Conditional { if_cond, if_then, if_else } => { + if infer(context.clone(), *if_cond) == Some(Type::Boolean) { + let kind = infer(context.clone(), *if_then); + if infer(context, *if_else) == kind { + return kind; + } + } + return None; + }, + } } /// Evaluates an expression given a context (of variables) to a term. @@ -16,7 +51,12 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, &'stati match expression { Expression::Annotation { expr, .. } => execute(context, *expr), Expression::Constant { term } => Ok(term), - Expression::Variable { id } => context.get(&id).ok_or("no such variable in context").map(|x| *x), + Expression::Variable { id } => { + match context.get(&id) { + Some(term) => Ok(*term), + None => Err("no such variable in context") + } + }, Expression::Abstraction { .. } => Err("attempting to execute an abstraction"), Expression::Application { func, arg } => { match *func { |