summaryrefslogtreecommitdiff
path: root/src/simple.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/simple.rs')
-rw-r--r--src/simple.rs50
1 files changed, 50 insertions, 0 deletions
diff --git a/src/simple.rs b/src/simple.rs
new file mode 100644
index 0000000..f71da46
--- /dev/null
+++ b/src/simple.rs
@@ -0,0 +1,50 @@
+// Simple bidirectional type checking
+
+use crate::ast::*;
+
+pub fn infer(context: Context, expression: Expression) {
+ todo!();
+}
+
+pub fn check(context: Context, expression: Expression) {
+ todo!();
+}
+
+/// Evaluates an expression given a context (of variables) to a term.
+/// Panics on non-evaluatable code.
+pub fn execute(context: Context, expression: Expression) -> Term {
+ match expression {
+ Expression::Annotation { expr, .. } => return execute(context, *expr),
+ Expression::Constant { term } => return term,
+ Expression::Variable { id } => return context[&id],
+ Expression::Abstraction { .. } => panic!(),
+ Expression::Application { func, arg } => {
+ match *func {
+ Expression::Abstraction { param, func } => {
+ let mut context = context;
+ context.insert(param, execute(context.clone(), *arg));
+ return execute(context, *func);
+ },
+ _ => panic!()
+ }
+ },
+ Expression::Conditional { if_cond, if_then, if_else } => {
+ match execute(context.clone(), *if_cond).val {
+ 1 => execute(context, *if_then),
+ 0 => execute(context, *if_else),
+ _ => panic!()
+ }
+ },
+ }
+}
+
+// intentionally small: i want to run into errors
+/// assumption: the count is instantiated to zero
+fn uniquify(count: &mut u8) -> String {
+ *count += 1;
+ if *count == 0 {
+ panic!("we've overflowed!");
+ } else {
+ return String::from(format!("{:X}", count));
+ }
+}