(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)))))