A cunning interpreter for the pure untyped λ-calculus.
severen.dev
1-- SPDX-FileCopyrightText: 2022 Severen Redwood <sev@severen.dev>
2-- SPDX-License-Identifier: CC0-1.0
3
4module UnitTests (unitTests) where
5
6import Sly.Eval (hnf, whnf)
7import Sly.Syntax
8 ( Term (..),
9 fromChurchBool,
10 fromChurchNat,
11 toChurchBool,
12 toChurchNat,
13 )
14import Test.Hspec
15import Test.Tasty
16import Test.Tasty.Hspec
17
18unitTests :: IO TestTree
19unitTests = testSpec "Unit Tests" do
20 describe "Church Numerals" do
21 it "0 == \\s z -> z" do
22 let zero = Abs "s" $ Abs "z" (Var "z")
23 toChurchNat 0 `shouldBe` zero
24 fromChurchNat zero `shouldBe` Just 0
25
26 it "1 == \\s z -> s z" do
27 let one = Abs "s" $ Abs "z" $ App (Var "s") (Var "z")
28 toChurchNat 1 `shouldBe` one
29 fromChurchNat one `shouldBe` Just 1
30
31 it "2 == \\s z -> s (s z)" do
32 let two =
33 Abs "s" $
34 Abs "z" $
35 App (Var "s") (App (Var "s") (Var "z"))
36 toChurchNat 2 `shouldBe` two
37 fromChurchNat two `shouldBe` Just 2
38
39 describe "Church Booleans" do
40 it "#t == \\t f -> t" do
41 let true = Abs "t" $ Abs "f" (Var "t")
42 toChurchBool True `shouldBe` true
43 fromChurchBool true `shouldBe` Just True
44
45 it "#f == \\t f -> f" do
46 let false = Abs "t" $ Abs "f" (Var "f")
47 toChurchBool False `shouldBe` false
48 fromChurchBool false `shouldBe` Just False
49
50 describe "Evaluator" do
51 let x = (Var "x")
52 in do
53 it "hnf x == x" $ hnf x `shouldBe` x
54 it "whnf x == x" $ whnf x `shouldBe` x
55
56 let f = Abs "x" $ App (Var "x") (Var "y")
57 in do
58 it "hnf (\\x -> x y) == \\x -> x y" $ hnf f `shouldBe` f
59 it "whnf (\\x -> x y) == \\x -> x y" $ whnf f `shouldBe` f
60
61 let t = App (Var "x") (Var "y")
62 in do
63 it "hnf (x y) == x y" $ hnf t `shouldBe` t
64 it "whnf (x y) == x y" $ whnf t `shouldBe` t
65
66 let f = Var "f"
67 g = Abs "x" $ App (Var "f") (Var "x")
68 y = Var "y"
69 t = App g y
70 in do
71 it "hnf ((\\x -> f x) y) == f y" $ hnf t `shouldBe` App f y
72 it "whnf ((\\x -> f x) y) == f y" $ whnf t `shouldBe` App f y