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
|
package org.lambdanantes.lcgoji;
import org.junit.Test;
import org.lambdanantes.lcgoji.ast.Term;
import org.lambdanantes.lcgoji.ast.Var;
import static org.hamcrest.CoreMatchers.is;
import static org.junit.Assert.assertThat;
import static org.lambdanantes.lcgoji.LCEvaluator.evaluate;
import static org.lambdanantes.lcgoji.ast.Abs.IDENTITY;
import static org.lambdanantes.lcgoji.ast.Abs.λ;
import static org.lambdanantes.lcgoji.ast.App.apply;
import static org.lambdanantes.lcgoji.ast.Var.var;
public class LCEvaluatorTest {
Var x = var("x");
Var y = var("y");
Var z = var("z");
@Test
public void l_evaluation_d_une_variable_rend_la_meme_variable() {
// evaluate(x) == x
assertEvalTo(x, x);
}
@Test
public void l_evaluation_d_une_abstraction_rend_la_meme_abstraction() {
// evaluate(λx.x) == λx.x
assertEvalTo(IDENTITY, IDENTITY);
}
@Test
public void l_evaluation_de_l_application_de_deux_vars_rend_la_meme_application() {
// evaluate(x y) == x y
assertEvalTo(apply(x, y), apply(x, y));
}
@Test
public void l_evaluation_de_l_application_de_l_identite_sur_un_argument_rend_l_argument() {
// evaluate((λx.x) y) == y
assertEvalTo(apply(IDENTITY, y), y);
}
@Test
public void l_evaluation_de_l_application_d_une_abstraction_substitue_son_argument() {
// evaluate((λx.x x) y ) == y y
assertEvalTo(apply(λ("x", apply(x, x)), y), apply(y, y));
}
@Test
public void l_evaluation_de_l_application_d_une_abstraction_d_abstraction_substitue_recursivement_son_argument() {
// evaluate((λx.λy.x) z) == λy.z
assertEvalTo(apply(λ("x", λ("y", x)), z), λ("y", z));
}
@Test
public void l_evaluation_de_l_application_d_une_abstraction_ne_substitue_pas_ses_variables_libres() {
// evaluate((λx.y) z) == y
assertEvalTo(apply(λ("x", y), z), y);
}
@Test
public void l_evaluation_de_l_application_d_une_abstraction_d_abstraction_ne_substitue_pas_les_variables_redefinies() {
// evaluate((λx.λx.x) z) == λx.x
assertEvalTo(apply(λ("x", λ("x", x)), z), λ("x", x));
}
/////
private static void assertEvalTo(Term termToEvaluate, Term result) {
assertThat(evaluate(termToEvaluate), is(result));
}
}
|
