aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorJJ2023-04-06 22:55:54 +0000
committerJJ2023-04-06 22:55:54 +0000
commit5e09660164f7749eb73c133deea718bacdfe6ac6 (patch)
treea3008b330829722748c5fa0fe83855b5591574b4 /src
parenta5c2add97c11237b3f0a224b1ec90dcf447cc2b5 (diff)
begin bidirectional implementation
Diffstat (limited to 'src')
-rw-r--r--src/main.rs2
-rw-r--r--src/parser.rs1
-rw-r--r--src/simple.rs50
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 {