blob: d1e9c41dcb7245e1738601c7b2b1ad89cf65fe62 (
plain)
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
|
(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)))))
|
