summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
blob: 89e86b9746dd036f1cef4ada5c53dee2570c7fb1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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, pending, shouldBe)

spec :: Spec
spec = it "evaluates Term" pending

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