summaryrefslogtreecommitdiff
path: root/java/LCEvaluatorTest.java
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud.bailly@iohk.io>2024-10-12 10:07:07 +0200
committerArnaud Bailly <arnaud.bailly@iohk.io>2024-10-12 10:07:07 +0200
commit0ab73e47af2bba3fb2ff6a4bf08ada4a3309bf3e (patch)
tree05e2b9ebd60e5c8175f086e1de73657032d9c2fc /java/LCEvaluatorTest.java
parent3363ab2da764825558c859f4419ff99528ed2274 (diff)
downloadlambda-nantes-0ab73e47af2bba3fb2ff6a4bf08ada4a3309bf3e.tar.gz
Add java evaluator
Diffstat (limited to 'java/LCEvaluatorTest.java')
-rw-r--r--java/LCEvaluatorTest.java74
1 files changed, 74 insertions, 0 deletions
diff --git a/java/LCEvaluatorTest.java b/java/LCEvaluatorTest.java
new file mode 100644
index 0000000..ec2f027
--- /dev/null
+++ b/java/LCEvaluatorTest.java
@@ -0,0 +1,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));
+ }
+}