1
//! Here we implement a simple lambda calculus interpreter.
2
//! The beta-reduction rule has the side effect of increasing a counter in the metadata.
3

            
4
use std::collections::HashSet;
5
use tree_morph::*;
6
use uniplate::derive::Uniplate;
7

            
8
#[derive(Debug, Clone, PartialEq, Eq, Uniplate)]
9
#[uniplate()]
10
enum Expr {
11
    Abs(u32, Box<Expr>),
12
    App(Box<Expr>, Box<Expr>),
13
    Var(u32),
14
}
15

            
16
impl Expr {
17
29
    fn free_vars(&self) -> HashSet<u32> {
18
29
        match self {
19
20
            Expr::Var(x) => {
20
20
                let mut set = HashSet::new();
21
20
                set.insert(*x);
22
20
                set
23
            }
24
3
            Expr::App(m, n) => {
25
3
                let mut set = m.free_vars();
26
3
                set.extend(n.free_vars());
27
3
                set
28
            }
29
6
            Expr::Abs(x, m) => {
30
6
                let mut set = m.free_vars();
31
6
                set.remove(x);
32
6
                set
33
            }
34
        }
35
29
    }
36

            
37
2
    fn vars(&self) -> HashSet<u32> {
38
2
        match self {
39
2
            Expr::Var(x) => {
40
2
                let mut set = HashSet::new();
41
2
                set.insert(*x);
42
2
                set
43
            }
44
            Expr::App(m, n) => {
45
                let mut set = m.vars();
46
                set.extend(n.vars());
47
                set
48
            }
49
            Expr::Abs(x, m) => {
50
                let mut set = m.vars();
51
                set.insert(*x);
52
                set
53
            }
54
        }
55
2
    }
56
}
57

            
58
// Create a fresh unused variable
59
1
fn fresh(vars: &HashSet<u32>) -> u32 {
60
1
    *vars.iter().max().unwrap_or(&0) + 1
61
1
}
62

            
63
// Capture-avoiding substitution
64
15
fn subst(expr: &Expr, x: u32, f: &Expr) -> Expr {
65
15
    if !expr.free_vars().contains(&x) {
66
4
        return expr.clone(); // x is bound or unused
67
11
    }
68
11

            
69
11
    match expr {
70
7
        Expr::Var(y) => {
71
7
            if *y == x {
72
7
                f.clone()
73
            } else {
74
                Expr::Var(*y)
75
            }
76
        }
77
2
        Expr::App(m, n) => Expr::App(Box::new(subst(m, x, f)), Box::new(subst(n, x, f))),
78
2
        Expr::Abs(y, g) => {
79
2
            if *y == x {
80
                Expr::Abs(*y, g.clone()) // binding occurrence
81
2
            } else if !f.free_vars().contains(y) {
82
1
                Expr::Abs(*y, Box::new(subst(g, x, f))) // substitution is safe
83
            } else {
84
1
                let z = fresh(&f.vars().union(&f.vars()).cloned().collect());
85
1
                let new_g = subst(g, *y, &Expr::Var(z));
86
1
                Expr::Abs(z, Box::new(subst(&new_g, x, f))) // capture avoidance
87
            }
88
        }
89
    }
90
15
}
91

            
92
// Beta-reduction
93
21
fn beta_reduce(expr: &Expr) -> Option<Expr> {
94
21
    if let Expr::App(m, n) = expr {
95
10
        if let Expr::Abs(x, g) = m.as_ref() {
96
8
            return Some(subst(&g, *x, n));
97
2
        }
98
11
    }
99
13
    None
100
21
}
101

            
102
21
fn transform_beta_reduce(cmd: &mut Commands<Expr, u32>, expr: &Expr, _: &u32) -> Option<Expr> {
103
21
    let retval = beta_reduce(expr);
104
21
    if retval.is_some() {
105
8
        cmd.mut_meta(|m| *m += 1);
106
13
    }
107
21
    retval
108
21
}
109

            
110
#[test]
111
1
fn test_simple_application() {
112
1
    // (\x. x) 1 -> 1
113
1
    let expr = Expr::App(
114
1
        Box::new(Expr::Abs(0, Box::new(Expr::Var(0)))),
115
1
        Box::new(Expr::Var(1)),
116
1
    );
117
1
    let (result, meta) = reduce(transform_beta_reduce, expr, 0);
118
1
    assert_eq!(result, Expr::Var(1));
119
1
    assert_eq!(meta, 1);
120
1
}
121

            
122
#[test]
123
1
fn test_nested_application() {
124
1
    // ((\x. x) (\y. y)) 1 -> 1
125
1
    let expr = Expr::App(
126
1
        Box::new(Expr::App(
127
1
            Box::new(Expr::Abs(0, Box::new(Expr::Var(0)))),
128
1
            Box::new(Expr::Abs(1, Box::new(Expr::Var(1)))),
129
1
        )),
130
1
        Box::new(Expr::Var(2)),
131
1
    );
132
1
    let (result, meta) = reduce(transform_beta_reduce, expr, 0);
133
1
    assert_eq!(result, Expr::Var(2));
134
1
    assert_eq!(meta, 2);
135
1
}
136

            
137
#[test]
138
1
fn test_capture_avoiding_substitution() {
139
1
    // (\x. (\y. x)) 1 -> (\y. 1)
140
1
    let expr = Expr::App(
141
1
        Box::new(Expr::Abs(0, Box::new(Expr::Abs(1, Box::new(Expr::Var(0)))))),
142
1
        Box::new(Expr::Var(1)),
143
1
    );
144
1
    let (result, meta) = reduce(transform_beta_reduce, expr, 0);
145
1
    assert_eq!(result, Expr::Abs(2, Box::new(Expr::Var(1))));
146
1
    assert_eq!(meta, 1);
147
1
}
148

            
149
#[test]
150
1
fn test_double_reduction() {
151
1
    // (\x. (\y. y)) 1 -> (\y. y)
152
1
    let expr = Expr::App(
153
1
        Box::new(Expr::Abs(0, Box::new(Expr::Abs(1, Box::new(Expr::Var(1)))))),
154
1
        Box::new(Expr::Var(2)),
155
1
    );
156
1
    let (result, meta) = reduce(transform_beta_reduce, expr, 0);
157
1
    assert_eq!(result, Expr::Abs(1, Box::new(Expr::Var(1))));
158
1
    assert_eq!(meta, 1);
159
1
}
160

            
161
#[test]
162
1
fn test_id() {
163
1
    // (\x. x) -> (\x. x)
164
1
    let expr = Expr::Abs(0, Box::new(Expr::Var(0)));
165
1
    let (expr, meta) = reduce(transform_beta_reduce, expr, 0);
166
1
    assert_eq!(expr, Expr::Abs(0, Box::new(Expr::Var(0))));
167
1
    assert_eq!(meta, 0);
168
1
}
169

            
170
#[test]
171
1
fn test_no_reduction() {
172
1
    // x -> x
173
1
    let expr = Expr::Var(1);
174
1
    let (result, meta) = reduce(transform_beta_reduce, expr.clone(), 0);
175
1
    assert_eq!(result, expr);
176
1
    assert_eq!(meta, 0);
177
1
}
178

            
179
#[test]
180
1
fn test_complex_expression() {
181
1
    // (((\x. (\y. x y)) (\z. z)) (\w. w)) -> (\y. (\w. w) y) -> (\w. w)
182
1
    let expr = Expr::App(
183
1
        Box::new(Expr::App(
184
1
            Box::new(Expr::Abs(
185
1
                0,
186
1
                Box::new(Expr::Abs(
187
1
                    1,
188
1
                    Box::new(Expr::App(Box::new(Expr::Var(0)), Box::new(Expr::Var(1)))),
189
1
                )),
190
1
            )),
191
1
            Box::new(Expr::Abs(2, Box::new(Expr::Var(2)))),
192
1
        )),
193
1
        Box::new(Expr::Abs(3, Box::new(Expr::Var(3)))),
194
1
    );
195
1
    let (result, meta) = reduce(transform_beta_reduce, expr, 0);
196
1
    assert_eq!(result, Expr::Abs(3, Box::new(Expr::Var(3))));
197
1
    assert_eq!(meta, 3);
198
1
}