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
|
use crate::ast::Value;
use proptest::prelude::*;
use proptest::prop_oneof;
use std::collections::BTreeMap;
type Name = String;
#[derive(Debug, Clone, PartialEq)]
enum Type {
Int,
Bool,
}
fn any_type() -> impl Strategy<Value = Type> {
prop_oneof![Just(Type::Int), Just(Type::Bool),]
}
struct Context {
context: BTreeMap<Name, Type>,
}
impl Context {
pub fn empty() -> Self {
Context {
context: BTreeMap::new(),
}
}
pub fn bind(&mut self, sym: Name, ty: Type) -> &mut Self {
self.context.insert(sym, ty);
self
}
pub fn type_of(&self, val: &Value) -> Option<Type> {
use Value::*;
match val {
Num(_) => Some(Type::Int),
Bool(_) => Some(Type::Bool),
Sym(s) => self.context.get(s).cloned(),
_ => None,
}
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::ast::Value::*;
use proptest::prelude::*;
proptest! {
#[test]
fn any_int_value_has_type_int(n in any::<i32>().prop_map(Num)) {
let ctx = Context::empty();
let ty = ctx.type_of(&n);
assert_eq!(Some(Type::Int), ty);
}
#[test]
fn any_bool_value_has_type_Bool(n in any::<bool>().prop_map(Bool)) {
let ctx = Context::empty();
let ty = ctx.type_of(&n);
assert_eq!(Some(Type::Bool), ty);
}
#[test]
fn any_bound_variable_has_bound_type(s in crate::ast::identifier(), t in any_type()) {
let mut ctx = Context::empty();
ctx.bind(s.clone(), t.clone());
let ty = ctx.type_of(&Sym(s));
assert_eq!(Some(t), ty);
}
#[test]
fn any_unbound_variable_has_no_type(s in crate::ast::identifier()) {
let mut ctx = Context::empty();
let ty = ctx.type_of(&Sym(s));
assert_eq!(None, ty);
}
#[test]
fn def_symbol_has_type_of_its_body(s in crate::ast::identifier(), t in any_type()) {
}
}
}
|
