module Minilang.Lambda.EvalSpec (spec) where

import Control.Concurrent (threadDelay)
import Control.Concurrent.Async (race_)
import Minilang.Lambda.Eval (Term (..), Value, eval, normalise)
import Test.Hspec (Spec, describe, it, pending, shouldBe)

spec :: Spec
spec = do
  let y =
        Lam
          "f"
          ( App
              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
          )
      z =
        Lam
          "f"
          ( App
              (Lam "x" (App (Var "f") (Lam "y" (App (App (Var "x") (Var "x")) (Var "y")))))
              (Lam "x" (App (Var "f") (Lam "y" (App (App (Var "x") (Var "x")) (Var "y")))))
          )

      omega =
        App (Lam "x" (App (Var "x") (Var "x"))) (Lam "x" (App (Var "x") (Var "x")))

      fst' = Lam "x" (Lam "y" (Var "x"))
      snd' = Lam "x" (Lam "y" (Var "y"))

  describe "call-by-value eval" $ do
    it "evaluates 'x' as itself" $ do
      let term = Var "x"
      normalise term `shouldBe` Var "x"
    it "evaluates '((λ x. x) y)' as 'y'" $ do
      let term = App (Lam "x" (Var "x")) (Var "y")
      normalise term `shouldBe` Var "y"
    it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do
      let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y")
      normalise term `shouldBe` App (Var "t") (Var "y")
    it "evaluates '((λ x y. x) z t)' as 'z'" $ do
      let term = App (App fst' (Var "z")) (Var "t")
      normalise term `shouldBe` Var "z"
    it "diverges on evaluating ω" $
      shouldDiverge $
        normalise omega
    it "diverges on evaluating ω applied to a function that use it" $
      shouldDiverge $
        normalise (App fst' omega)
    it "diverges on evaluating ω applied to a function that do not use it" $
      shouldDiverge $
        normalise (App snd' omega)
  describe "Church numerals" $ do
    let zero = Lam "s" (Lam "z" (Var "z"))
        one = Lam "s" (Lam "z" (App (Var "s") (Var "z")))
        two = Lam "s" (Lam "z" (App "s" (App (Var "s") (Var "z"))))
        succ' = Lam "n" (Lam "s" (Lam "z" (App (Var "s") (App (App (Var "n") (Var "s")) (Var "z")))))
        add' = Lam "j" (Lam "k" (Lam "s" (Lam "z" (App (App "j" "s") (App (App "k" "s") "z")))))

    it "normalises successor" $
      normalise (App succ' zero)
        `shouldBe` one

    it "adds two numerals" $
      normalise (App (App add' one) one)
        `shouldBe` two

  -- describe "call-by-name eval" $ do
  --   it "evaluates 'x' as itself" $ do
  --     normalise' (Var "x") `shouldBe` Var "x"
  --   it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
  --     normalise' (App (App snd' omega) "z") `shouldBe` Var "z"
  --   it "diverges on evaluating ω" $
  --     shouldDiverge $
  --       normalise' omega

shouldDiverge :: Term -> IO ()
shouldDiverge t =
  race_
    (t `seq` fail "Did not diverge")
    (threadDelay 1000000)