summaryrefslogtreecommitdiff
path: root/lambda-calcul/clojure/test/lccl/lc
diff options
context:
space:
mode:
authorArnaud Bailly <arnaud.bailly@iohk.io>2025-01-25 10:45:41 +0100
committerArnaud Bailly <arnaud.bailly@iohk.io>2025-01-25 10:45:41 +0100
commit7752d73216578d5961751b5d0535088d384b4aa6 (patch)
tree786e46fe1276e93ade0a48398cd4c9ac13081707 /lambda-calcul/clojure/test/lccl/lc
parentd6f68e919db51d366c8ca3c1509bea12aa81d692 (diff)
downloadlambda-nantes-7752d73216578d5961751b5d0535088d384b4aa6.tar.gz
Move λ-calcul workshop code to subdirectory
Diffstat (limited to 'lambda-calcul/clojure/test/lccl/lc')
-rw-r--r--lambda-calcul/clojure/test/lccl/lc/evaluator_test.clj46
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)))))
+