1 files changed, 46 insertions, 0 deletions
diff --git a/lambda-calcul/clojure/test/lccl/lc/evaluator_test.clj b/lambda-calcul/clojure/test/lccl/lc/evaluator_test.clj
new file mode 100644
index 0000000..d1e9c41
--- /dev/null
+++ b/lambda-calcul/clojure/test/lccl/lc/evaluator_test.clj
@@ -0,0 +1,46 @@
+(ns lccl.lc.evaluator-test
+  (:require
+   [clojure.test :refer [deftest testing is]]
+   [lccl.lc.ast :refer [->Var ->Abs ->App IDENTITY]]
+   [lccl.lc.evaluator :refer [substitute evaluate]]))
+
+(def x (->Var "x"))
+(def y (->Var "y"))
+(def z (->Var "z"))
+
+(defn- assertEvalTo
+  [termToEvaluate result]
+  (is (= result (evaluate termToEvaluate))))
+
+(deftest evaluation
+  (testing "l'evaluation d'une variable rend la même variable"
+    ; evaluate(x) == x
+    (assertEvalTo x x))
+  (testing "l'evaluation d'une abstraction rend la même abstraction"
+    ; evaluate(λx.x) == λx.x
+    (assertEvalTo IDENTITY IDENTITY))
+  (testing "l'evaluation de l'application de deux vars rend la même abstraction"
+    ; evaluate(x y) == x y
+    (assertEvalTo (->App x y) (->App x y)))
+  (testing "l'evaluation de l'application de l'identite sur un argument rend l'argument"
+    ;  evaluate((λx.x) y) == y
+    (assertEvalTo (->App IDENTITY y) y))
+  (testing "l'evaluation de l'application d'une abstraction substitue son argument"
+    ;  evaluate((λx.x x) y) == y y
+    (assertEvalTo (->App (->Abs "x" (->App x x)) y) (->App y y)))
+  (testing "l'evaluation de l'application d'une abstraction d'abstraction substitue recursivement son argument"
+    ;  evaluate((λx.λy.x) z) == λy.z
+    (assertEvalTo (->App (->Abs "x" (->Abs "y" x)) z) (->Abs "y" z)))
+  (testing "l'evaluation de l'application d'une abstraction ne substitue pas ses variables libres"
+    ;  evaluate((λx.y) z) == y
+    (assertEvalTo (->App (->Abs "x" y) z) y))
+  (testing "l'evaluation de l'application d'une abstraction d'abstraction ne substitue pas les variables redéfinies"
+    ;  evaluate((λx.λx.x) z) == λx.x
+    (assertEvalTo (->App (->Abs "x" (->Abs "x" x)) z) (->Abs "x" x)))
+  )
+
+(deftest substitution
+  (testing "la substitution d'une variable rend la même variable"
+      ; substitute(x x, y) == y y
+    (is (= y (substitute x "x" y)))))
+