module Minilang.Lambda.EvalSpec (spec) where import Control.Concurrent (threadDelay) import Control.Concurrent.Async (race_) import Minilang.Lambda.Eval (Term (..), eval, evalNeed) import Test.Hspec (Spec, describe, it, shouldBe) spec :: Spec spec = do let fix = Lam "x" (App (Var "x") (Var "x")) let omega = App fix fix let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z") describe "call-by-value eval" $ do it "evaluates 'x' as itself" $ do let term = Var "x" eval term [] `shouldBe` Var "x" it "evaluates '((λ x. x) y)' as 'y'" $ do let term = App (Lam "x" (Var "x")) (Var "y") eval term [] `shouldBe` Var "y" it "evaluates '((λ x y. y) y z t)' as '(z t)'" $ do let snd' = Lam "x" (Lam "y" (Var "y")) let term = App (App (App snd' (Var "y")) (Var "z")) (Var "t") eval term [] `shouldBe` App (Var "z") (Var "t") 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` Var "x" it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do evalNeed term [] `shouldBe` Var "z" it "diverges on evaluating ω" $ shouldDiverge $ evalNeed omega [] shouldDiverge :: Term -> IO () shouldDiverge t = race_ (t `seq` fail "Did not diverge") (threadDelay 1000000)