module Minilang.Lambda.EvalSpec (spec) where

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

spec :: Spec
spec = do
  let fix =
        Lam
          "f"
          ( App
              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
          )
  let omega = App fix fix
  let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z")
  let fst' = Lam "x" (Lam "y" (Var "x"))

  describe "call-by-value eval" $ do
    it "evaluates 'x' as itself" $ do
      let term = Var "x"
      eval term [] `shouldBe` V "x"
    it "evaluates '((λ x. x) y)' as 'y'" $ do
      let term = App (Lam "x" (Var "x")) (Var "y")
      eval term [] `shouldBe` V "y"
    it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do
      let snd' = Lam "x" (Lam "y" (Var "y"))
      let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y")
      eval term [] `shouldBe` Ap (V "t") (V "y")
    it "evaluates '((λ x y. x) z t)' as 'z'" $ do
      let term = App (App fst' (Var "z")) (Var "t")
      eval term [] `shouldBe` V "z"
    it "diverges on evaluating argument bound to ω" $
      shouldDiverge $
        eval term []

  describe "call-by-need eval" $ do
    it "evaluates 'x' as itself" $ do
      evalNeed (Var "x") [] `shouldBe` V "x"
    it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
      evalNeed term [] `shouldBe` V "z"
    it "diverges on evaluating ω" $
      shouldDiverge $
        evalNeed omega []

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