1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
// Simple bidirectional type checking
#![allow(unused_variables)]
use crate::ast::*;
pub fn check(context: Context, expression: Expression, target: Type) -> Result<(), (&'static str, Context, Type)> {
match expression {
Expression::Annotation { expr, kind } => Err(("attempting to typecheck an annotation", context, target)),
// Bt-CheckInfer
Expression::Constant { term } => match term.kind == target {
true => Ok(()),
false => Err(("constant is of wrong type", context, target))
},
// Bt-CheckInfer
// in the future: extend to closures? nah probably not
Expression::Variable { id } => match context.get(&id) {
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 } => {
let mut context = context;
context.insert(param, Term { val: 0, kind: *from }); // hack
return check(context, *func, *to);
},
_ => Err(("attempting to check an abstraction with a non-function type", context, 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())?;
return Ok(());
}
}
}
// empty's gonna cause problems
pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static str, Context, Type)> {
match expression {
// 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) => Ok(term.clone().kind),
None => Err(("failed to find variable in context", context, Type::Empty))
},
// Bt-App
Expression::Application { func, arg } => match infer(context.clone(), *func)? {
Type::Function { from, to } => {
check(context, *arg, *from).map(|x| *to)
},
_ => Err(("application abstraction is not a function type", context, Type::Empty))
},
Expression::Abstraction { param, func } => Err(("attempting to infer from an abstraction", context, Type::Empty)),
// idk
Expression::Conditional { if_cond, if_then, if_else } => {
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))
}
}
}
}
/// 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, 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", context))
}
},
Expression::Abstraction { .. } => Err(("attempting to execute an abstraction", context)),
Expression::Application { func, arg } => {
match *func {
Expression::Abstraction { param, func } => {
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", 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", context))
}
}
}
}
|
