blob: f1802da717d174a05089862c7870afe5ef892c38 (
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
{-# 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 "+"
describe "string literals and builtins" $ do
let benv = builtinDeBruijnEnv :: Env Text
it "FStr self-evaluates" $
eval' benv (FStr "hello") `shouldBe` FStr "hello"
it "(str-concat \"foo\" \"bar\") reduces to FStr \"foobar\"" $
eval' benv (App (App (FBuiltin "str-concat") (FStr "foo")) (FStr "bar"))
`shouldBe` FStr "foobar"
it "(str-length \"hello\") reduces to FNum 5" $
eval' benv (App (FBuiltin "str-length") (FStr "hello"))
`shouldBe` FNum 5
it "(str-slice 1 3 \"abcde\") reduces to FStr \"bc\"" $
eval' benv (App (App (App (FBuiltin "str-slice") (FNum 1)) (FNum 3)) (FStr "abcde"))
`shouldBe` FStr "bc"
it "(str= \"abc\" \"abc\") reduces to Church True" $
eval' benv (App (App (FBuiltin "str=") (FStr "abc")) (FStr "abc"))
`shouldBe` Lam "f" (Lam "t" (Var "t" 0))
it "(str= \"abc\" \"xyz\") reduces to Church False" $
eval' benv (App (App (FBuiltin "str=") (FStr "abc")) (FStr "xyz"))
`shouldBe` Lam "f" (Lam "t" (Var "f" 1))
it "(str< \"a\" \"b\") reduces to Church True" $
eval' benv (App (App (FBuiltin "str<") (FStr "a")) (FStr "b"))
`shouldBe` Lam "f" (Lam "t" (Var "t" 0))
it "(str-concat \"hello\") is partial: stays as App spine" $
eval' benv (App (FBuiltin "str-concat") (FStr "hello"))
`shouldBe` App (FBuiltin "str-concat") (FStr "hello")
|
