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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
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, shouldBe)
import Test.Hspec.QuickCheck (prop)
import Data.Text (pack)
import Test.QuickCheck (NonEmptyList (..), arbitrary, forAll, (===))
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 "integer literals" $ do
-- An integer literal is already a normal form: normalise must return it unchanged.
prop "any integer literal normalises to itself" $ \n ->
normalise (Num n) === Num (n :: Int)
-- eval on a bare Num must always produce the VNum value form, never a closure
-- or neutral, regardless of the integer's sign or magnitude.
prop "eval of any integer literal produces VNum" $ \n ->
eval [] (Num n) === VNum (n :: Int)
-- A number is not a function. Applying it to any argument must leave a stuck
-- neutral application: App (Num n) (normalise arg). We test this with free
-- variables as arguments, which are themselves already in normal form.
prop "an integer in function position produces a stuck application" $
forAll arbitrary $ \n ->
forAll (getNonEmpty <$> arbitrary) $ \x ->
normalise (App (Num n) (Var (pack x)))
=== App (Num (n :: Int)) (Var (pack x))
-- 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)
|
