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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
use proptest::{
prelude::*,
string::{string_regex, RegexGeneratorStrategy},
};
use serde::{Deserialize, Serialize};
use std::fmt::{self, Display};
#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum Type {
Num,
Bool,
Arr(Box<Type>, Box<Type>),
}
impl Display for Type {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "Type")
}
}
#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum TypeError {
UnknownType(Value),
UnboundVariable(String),
}
#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
pub enum Value {
Num(i32),
Bool(bool),
Sym(String),
App(Box<Value>, Box<Value>),
Lam(String, Box<Value>),
Def(String, Box<Value>),
Let(String, Box<Value>, Box<Value>),
// typed abstraction
TLam(String, Type, Box<Value>),
// reified type
// this is unsound as we are not in a dependently typed language
// but useful to unify external representation (AST). In theory,
// we should separate AST from Terms
Type(Type)
}
use Value::*;
impl Value {
/// Return the spine of an application
fn spine(&self) -> Vec<Value> {
match self {
App(l, r) => {
let mut spine = l.spine();
spine.push(*r.clone());
spine
}
_ => vec![self.clone()],
}
}
}
impl Display for Value {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Value::Num(i) => write!(f, "{}", i),
Value::Bool(b) => write!(f, "{}", b),
Value::Sym(s) => write!(f, "{}", s),
Value::App(_, _) => {
let app = self
.spine()
.iter()
.map(|v| v.to_string())
.collect::<Vec<String>>()
.join(" ");
write!(f, "({})", app)
}
Value::Lam(var, body) => write!(f, "(lam {} {})", var, body),
Value::Def(var, value) => write!(f, "(def {} {})", var, value),
Value::Let(var, value, body) => write!(f, "(let ({} {}) {})", var, value, body),
Value::TLam(var,typ, body) => write!(f, "(tlam ({} {}) {})", var, typ, body),
Value::Type(typ) => write!(f, ":{}", typ),
}
}
}
pub const IDENTIFIER: &str = "\\pL(\\pL|\\pN)*";
pub fn identifier() -> RegexGeneratorStrategy<String> {
string_regex(IDENTIFIER).unwrap()
}
pub fn ascii_identifier() -> RegexGeneratorStrategy<String> {
string_regex("[a-zA-Z][a-zA-Z0-9]*").unwrap()
}
impl Arbitrary for Value {
type Parameters = ();
type Strategy = BoxedStrategy<Self>;
fn arbitrary_with(_args: ()) -> Self::Strategy {
let any_num = any::<i32>().prop_map(Num);
let any_bool = any::<bool>().prop_map(Bool);
let leaf = prop_oneof![
any_num,
any_bool,
// see https://unicode.org/reports/tr18/#General_Category_Property for one letter unicode categories
identifier().prop_map(Sym),
];
let expr = leaf.prop_recursive(4, 128, 5, move |inner| {
prop_oneof![
(inner.clone(), inner.clone()).prop_map(|(l, r)| App(Box::new(l), Box::new(r))),
(identifier(), inner.clone()).prop_map(|(var, body)| Lam(var, Box::new(body))),
(identifier(), inner.clone(), inner.clone()).prop_map(|(var, body, expr)| {
Value::Let(var, Box::new(body), Box::new(expr))
}),
]
});
prop_oneof![
expr.clone(),
(identifier(), expr).prop_map(|(var, body)| Def(var, Box::new(body)))
]
.boxed()
}
}
#[cfg(test)]
mod ast_tests {
use super::Value::{self, *};
use proptest::collection::vec;
use proptest::prelude::*;
proptest! {
#[test]
fn display_multiple_applications_as_a_sequence(atoms in vec("[a-z]".prop_map(Sym), 2..10)) {
let init = atoms.first().unwrap().clone();
let value = atoms.iter().skip(1).fold(init, |acc, expr| {
Value::App(Box::new(acc.clone()), Box::new(expr.clone()))
});
assert_eq!(value.to_string(),
format!("({})",
atoms.iter().map(|v| v.to_string()).collect::<Vec<String>>().join(" ")));
}
#[test]
fn can_serialize_and_deserialize(value in any::<Value>()) {
let serialized = serde_json::to_string(&value).unwrap();
let deserialized: Value = serde_json::from_str(&serialized).unwrap();
assert_eq!(value, deserialized);
}
}
#[test]
fn can_represent_let_expression_in_json() {
let let_expr = Let(
"x".to_string(),
Box::new(Num(42)),
Box::new(Sym("x".to_string())),
);
let serialized = serde_json::to_string(&let_expr).unwrap();
let expected = r#"{"Let":["x",{"Num":42},{"Sym":"x"}]}"#;
assert_eq!(serialized, expected);
}
}
|
