blob: d772fe0acd5c7f1783cf733f0d16d3a0ea19f09c (
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
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)
|
