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
|
use rand::Rng;
use std::fs::read_to_string;
mod ast;
use ast::*;
mod parser;
use parser::*;
pub fn run(arg: &str) -> String {
let content = read_to_string(arg).unwrap();
let value = parse(&content.to_string());
let result = eval(&value);
result.to_string()
}
fn eval(arg: &Value) -> Value {
match arg {
Value::App(l, r) => {
let result = apply(&eval(l), r);
if is_reducible(&result) {
eval(&result)
} else {
result
}
}
other => other.clone(),
}
}
fn is_reducible(result: &Value) -> bool {
match result {
Value::App(l, r) => match **l {
Value::Lam(_, _) => true,
_ => is_reducible(l) || is_reducible(r),
},
Value::Lam(_, _) => false,
_ => false,
}
}
fn apply(l: &Value, r: &Value) -> Value {
if let Value::Lam(v, body) = l {
subst(v, body, r)
} else {
Value::App(Box::new(l.clone()), Box::new(r.clone()))
}
}
fn subst(var: &str, body: &Value, e: &Value) -> Value {
match body {
Value::Sym(x) if x == var => e.clone(),
Value::Lam(x, b) if x == var => {
let y = gensym();
let bd = subst(x, b, &Value::Sym(y.clone()));
Value::Lam(y, Box::new(bd))
}
Value::Lam(x, b) => Value::Lam(x.to_string(), Box::new(subst(var, b, e))),
Value::App(l, r) => Value::App(Box::new(subst(var, l, e)), Box::new(subst(var, r, e))),
other => other.clone(),
}
}
fn gensym() -> String {
let mut rng = rand::thread_rng();
let n1: u8 = rng.gen();
format!("x_{}", n1)
}
#[cfg(test)]
mod lambda_test {
use crate::{eval, parse, Value};
#[test]
fn evaluating_a_non_reducible_value_yields_itself() {
let value = parse("(foo 12)");
assert_eq!(value, eval(&value));
}
#[test]
fn evaluating_application_on_an_abstraction_reduces_it() {
let value = parse("((lam x x) 12)");
assert_eq!(Value::Num(12), eval(&value));
}
#[test]
fn substitution_occurs_within_abstraction_body() {
let value = parse("(((lam x (lam y x)) 13) 12)");
assert_eq!(Value::Num(13), eval(&value));
}
#[test]
fn substitution_occurs_within_application_body() {
let value = parse("(((lam x (lam y (y x))) 13) 12)");
assert_eq!(
Value::App(Box::new(Value::Num(12)), Box::new(Value::Num(13))),
eval(&value)
);
}
#[test]
fn substitution_does_not_capture_free_variables() {
let value = parse("(((lam x (lam x x)) 13) 12)");
assert_eq!(Value::Num(12), eval(&value));
}
#[test]
fn interpretation_applies_to_both_sides_of_application() {
let value = parse("((lam x x) ((lam x x) 12))");
assert_eq!(Value::Num(12), eval(&value));
}
#[test]
fn reduction_is_applied_until_normal_form_is_reached() {
let value = parse("((((lam y (lam x (lam y (x y)))) 13) (lam x x)) 11)");
assert_eq!(Value::Num(11), eval(&value));
}
#[test]
fn reduction_always_select_leftmost_outermost_redex() {
// this should not terminate if we evaluate the rightmost redex first
let value = parse("((lam x 1) ((lam x (x x)) (lam x (x x))))");
assert_eq!(Value::Num(1), eval(&value));
}
}
|
