module EvaluationSpec (spec) where

import Evaluation (beta, subst)
import Parser (Expr (Abstraction, Application, Variable))
import Test.Hspec

spec :: Spec
spec = do
  describe "subst" $ do
    it "cannot substitute mismatched variables" $
      subst (Variable "x") "y" (Variable "z") `shouldBe` Variable "x"
    it "can substitute matched variables" $
      subst (Variable "x") "x" (Variable "z") `shouldBe` Variable "z"
    it "can substitute nested variables" $
      subst absWithZ "z" absI `shouldBe` absWithZMaker absI
  describe "beta reduction" $ do
    -- Normal forms (no redex)
    it "returns Nothing for a bare variable" $
      beta (Variable "x") `shouldBe` Nothing
    it "returns Nothing for a bare abstraction" $
      beta absI `shouldBe` Nothing
    it "returns Nothing when application has no lambda on left" $
      beta (Application (Variable "x") (Variable "y")) `shouldBe` Nothing

    -- Basic reductions
    it "reduces identity: (λi. i) y → y" $
      beta (Application absI (Variable "y"))
        `shouldBe` Just (Variable "y")
    it "reduces constant function: (λx. z) y → z" $
      beta (Application (Abstraction "x" (Variable "z")) (Variable "y"))
        `shouldBe` Just (Variable "z")

    -- Self-application
    it "(λx. x x)(λi. i) → (λi. i)(λi. i)" $
      beta (Application selfApp absI)
        `shouldBe` Just (Application absI absI)
    it "(λi. i)(λi. i) → (λi. i)" $
      beta (Application absI absI)
        `shouldBe` Just absI

    -- Redex not at top level
    it "reduces redex in function position: ((λi. i) y) z → y z" $
      beta (Application (Application absI (Variable "y")) (Variable "z"))
        `shouldBe` Just (Application (Variable "y") (Variable "z"))
    it "reduces redex inside lambda body: λz. (λi. i) y → λz. y" $
      beta (Abstraction "z" (Application absI (Variable "y")))
        `shouldBe` Just (Abstraction "z" (Variable "y"))
  where
    absWithZMaker z = Abstraction "x" (Application z (Variable "x"))
    absWithZ = absWithZMaker (Variable "z")
    absI = Abstraction "i" (Variable "i")
    selfApp = Abstraction "x" (Application (Variable "x") (Variable "x"))