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
|
import Test.HUnit
import Command
import TypeVar
import Term
import Theorem
import qualified Data.Set as Set
stdName :: String -> Name
stdName s = Name [] s
stdConst :: Const
stdConst = Const (stdName "const")
stdTypeVar :: Type
stdTypeVar = TypeVar (stdName "typevar")
stdVar :: String -> Var
stdVar s = Var (stdName s) stdTypeVar
stdVarTerm :: String -> Term
stdVarTerm s = TVar (stdVar s)
altVarTerm :: String -> Term
altVarTerm s = TVar (Var (stdName s) (TypeVar (stdName "alttypevar")))
name1 = TestCase (assertEqual "for (name \"abc\")"
(Just (Name [] "abc"))
(name "\"abc\""))
name2 = TestCase (assertEqual "for (name \"first.second.third\")"
(Just (Name ["first","second"] "third"))
(name "\"first.second.third\""))
name3 = TestCase (assertEqual "for (name \"firs\\t.se\\cond.\\t\\h\\ird\")"
(Just (Name ["first","second"] "third"))
(name "\"firs\\t.se\\cond.\\t\\h\\ird\""))
name4 = TestCase (assertEqual "for (name abc)" Nothing (name "abc"))
number1 = TestCase (assertEqual "for (number \"90\")" (Just 90) (number "90"))
number2 = TestCase (assertEqual "for (number \"0\")" (Just 0) (number "0"))
number3 = TestCase (assertEqual "for (number \"-1\")" (Just (-1)) (number "-1"))
number4 = TestCase (assertEqual "for (number \"-0\")" Nothing (number "-0"))
number5 = TestCase (assertEqual "for (number \"1.2\")" Nothing (number "1.2"))
assume1 = TestCase (assertEqual "for (assume (TConst ...)"
(Just (Theorem (Set.singleton (TConst stdConst typeBool))
(TConst stdConst typeBool)))
(assume (TConst stdConst typeBool)))
assume2 = TestCase (assertEqual "for (assume (TConst ...) --with wrong type"
Nothing
(assume (TConst stdConst stdTypeVar)))
axiom1 = TestCase (assertEqual "for (axiom (TConst ...) [])"
(Just (Theorem Set.empty (TConst stdConst stdTypeVar)))
(axiom (TConst stdConst stdTypeVar) []))
axiom2 = TestCase (assertEqual "for (axiom (TConst ...) [term1, term2] --term1 has wrong type"
Nothing
(axiom (TConst stdConst stdTypeVar)
[(TConst stdConst stdTypeVar),(TConst stdConst typeBool)]))
alphaEquiv1 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\yx -> x))"
False
(alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x")))
(TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x")))))
alphaEquiv2 = TestCase (assertEqual "for ((\\xy -> x) `alphaEquiv` (\\xy -> x))"
True
(alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x")))
(TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (stdVarTerm "x")))))
alphaEquiv3 = TestCase (assertEqual "for ((\\xyx -> x) `alphaEquiv` (\\yxx -> x))"
True
(alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "x"))))
(TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "x") (stdVarTerm "x"))))))
alphaEquiv4 = TestCase (assertEqual "for ((\\xyz -> y) `alphaEquiv` (\\zyx -> y))"
True
(alphaEquiv (TAbs (stdVarTerm "x") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "z") (stdVarTerm "y"))))
(TAbs (stdVarTerm "z") (TAbs (stdVarTerm "y") (TAbs (stdVarTerm "x") (stdVarTerm "y"))))))
alphaEquiv5 = TestCase (assertEqual "for ((\\x -> x) `alphaEquiv` (\\x -> x)) --x of lhs is different type to x of rhs"
False
(alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x"))
(TAbs (altVarTerm "x") (altVarTerm "x"))))
alphaEquiv6 = TestCase (assertEqual "for ((TAbs ...) `alphaEquiv` (TConst ...))"
False
(alphaEquiv (TAbs (stdVarTerm "x") (stdVarTerm "x"))
(TConst stdConst typeBool)))
main =
runTestTT $ TestList [name1,name2,name3,name4,
number1,number2,number3,number4,number5,
assume1,assume2,
axiom1,axiom2,
alphaEquiv1,alphaEquiv2,alphaEquiv3,alphaEquiv4,alphaEquiv5,alphaEquiv6]
|
