blob: eaff77cd3bd52c4f53323abb7670b28633e90714 (
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
82
83
|
{-# LANGUAGE TypeApplications #-}
module Minilang.Lambda.DeBruijnSpec where
import Minilang.Lambda.DeBruijn (DeBruijn (..), Env, builtinDeBruijnEnv, eval, toDeBruijn, eval')
import qualified Minilang.Lambda.Eval as Eval
import Test.Hspec (Spec, describe, it, shouldBe)
import Data.Text (Text)
spec :: Spec
spec = do
it "convert term to deBruijn representation" $ do
let term = Eval.Lam "x" (Eval.Lam "y" (Eval.Var "x"))
deBruijn = toDeBruijn term
deBruijn `shouldBe` Lam "x" (Lam "y" (Var "x" 1))
it "evaluates deBruijn term" $ do
let term = App (App (Lam "x" (Lam "y" (Var "x" 1))) (FV "z")) (FV "t")
eval @Text term `shouldBe` FV "z"
it "evaluates deBruijn term in env" $ do
let term = App (FV "z") (FV "t")
env = [("z", toDeBruijn $ Eval.Lam "x" (Eval.Var "x"))]
eval' env term `shouldBe` FV "t"
describe "built-in arithmetic" $ do
let benv = builtinDeBruijnEnv :: Env Text
it "(+ 3 4) reduces to FNum 7" $
eval' benv (App (App (FBuiltin "+") (FNum 3)) (FNum 4))
`shouldBe` FNum 7
it "(- 10 3) reduces to FNum 7" $
eval' benv (App (App (FBuiltin "-") (FNum 10)) (FNum 3))
`shouldBe` FNum 7
it "(* 2 5) reduces to FNum 10" $
eval' benv (App (App (FBuiltin "*") (FNum 2)) (FNum 5))
`shouldBe` FNum 10
it "(div 10 3) reduces to FNum 3" $
eval' benv (App (App (FBuiltin "div") (FNum 10)) (FNum 3))
`shouldBe` FNum 3
it "(mod 10 3) reduces to FNum 1" $
eval' benv (App (App (FBuiltin "mod") (FNum 10)) (FNum 3))
`shouldBe` FNum 1
it "(= 3 3) reduces to Church True" $
eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 3))
`shouldBe` Lam "f" (Lam "t" (Var "t" 0))
it "(= 3 4) reduces to Church False" $
eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 4))
`shouldBe` Lam "f" (Lam "t" (Var "f" 1))
it "(< 2 5) reduces to Church True" $
eval' benv (App (App (FBuiltin "<") (FNum 2)) (FNum 5))
`shouldBe` Lam "f" (Lam "t" (Var "t" 0))
it "(< 5 2) reduces to Church False" $
eval' benv (App (App (FBuiltin "<") (FNum 5)) (FNum 2))
`shouldBe` Lam "f" (Lam "t" (Var "f" 1))
it "(neg 7) reduces to FNum -7" $
eval' benv (App (FBuiltin "neg") (FNum 7))
`shouldBe` FNum (-7)
it "(+ 1) partial: stays as a spine without reducing" $
eval' benv (App (FBuiltin "+") (FNum 1))
`shouldBe` App (FBuiltin "+") (FNum 1)
it "(div 1 0) stays stuck" $
eval' benv (App (App (FBuiltin "div") (FNum 1)) (FNum 0))
`shouldBe` App (App (FBuiltin "div") (FNum 1)) (FNum 0)
it "(+ x 1) with free x stays stuck" $
eval' benv (App (App (FBuiltin "+") (FV "x")) (FNum 1))
`shouldBe` App (App (FBuiltin "+") (FV "x")) (FNum 1)
it "lookup of '+' in builtin env yields FBuiltin" $
eval' benv (FV "+") `shouldBe` FBuiltin "+"
|
