Daniels Stand von 20081110
[darcs-mirror-polyfix.git] / TestItExt.hs
1 module TestItExt where
2 import Test.HUnit
3 import ExFindExtended
4 import Prelude hiding (Either(..))
5
6 -------------------------------------------------------------------------------------------------
7 ---TestBeispiele fuer ExFind---------------------------------------------------------------------
8 ---um alle Tests auszufuehren  runTestTT tests  aufrufen-----------------------------------------
9 ---fuer einzelne Tests runTestTT test1  bzw. die entsprechenden Nummer statt 1-------------------
10 ---fuer Anzeige der bei der Ableitung benutzten Regeln  getTerm bsp1  bzw. entsprechende Nr------
11 -------------------------------------------------------------------------------------------------
12
13 ---shortcuts---
14 fAll i = All (TypVar i)
15 fAllStar i = AllStar (TypVar i)
16 tau1 `arrow` tau2 = Arrow tau1 tau2
17 var i = TVar (TypVar i)
18
19 --Beispiele:
20
21 -- RFix
22 bsp1 = fAll 1 (var 1)
23 -- RAll, R->, RI, RFix
24 bsp2 = fAll 1 (List (var 1) `arrow` List (var 1))
25 -- RAll, RAllStar, R->, LFixArrowStar, AxStar
26 bsp3 = fAll 1 (fAllStar 2 ((var 1 `arrow` var 2) `arrow` var 2))
27 -- RAll, RAllStar, R->, LIArrow, LFixArrowStar, AxStar
28 bsp4 = fAll 1 (fAllStar 2 ((List (var 1) `arrow` var 2) `arrow` var 2))
29
30 -- test for LI
31 -- RAll, RAllStar, R->, R->, LI, LFixArrowStar, AxStar
32 bsp5 = fAll 1 (fAllStar 2 ((List (var 2)) `arrow` ((var 1 `arrow` var 2) `arrow` var 2)))
33
34 -- test for LFix
35 -- RAll, RAllStar, R->, R->, LFix, LFixArrowStar, AxStar
36 bsp6 = fAll 1 (fAllStar 2 ( var 1 `arrow` ((var 1 `arrow` var 2) `arrow` var 2)))
37
38 -- test for L->->
39 -- RAll, RAllStar, R->, L->-> (fst: LFix->*, Ax*) (snd: Ax*)
40 bsp7 = fAll 1 (fAllStar 2 (((( var 1 `arrow` var 2) `arrow` var 2) `arrow` var 2) `arrow` var 2))
41
42 -- test for La->*1
43 -- RAll, RAllStar, R->, L->-> (fst: LFix->*, La->*1, Ax*) (snd: Ax*)
44 bsp8 = fAll 1 (fAllStar 2 (((( var 1 `arrow` (var 2 `arrow` var 2)) `arrow` var 2) `arrow` var 2) `arrow` var 2))
45
46 -- test for La->*2
47 -- RAll, RAllStar, R->, R->, LFix->*, La->*2, Ax*
48 bsp9 = fAll 1 (fAllStar 2 (fAllStar 3 (((var 1 `arrow` var 2) `arrow` ((var 2 `arrow` var 3) `arrow` var 3)))))
49
50 bsp10 = fAll 1 (fAllStar 2 ((var 1 `arrow` (List (var 2))) `arrow` var 2))
51
52 -- test for LFix
53 -- RAll, RAllStar, R->, LFix->, LFix->*, Ax*
54 bsp11 = fAll 1 (fAllStar 2 ((var 2 `arrow` (var 1 `arrow` var 2)) `arrow` var 2))
55
56 bsp12 = fAll 1 (fAllStar 2 (fAllStar 3 (fAllStar 4 ((((var 3 `arrow` (var 1 `arrow` (List (var 2)))) `arrow` var 2) `arrow` var 3) `arrow` (((var 2 `arrow` (List (var 3))) `arrow` (var 3 `arrow` var 4) `arrow` (List (var 4))))))))
57
58 -----new examples for the extended algorithm-------
59 --test for LInt
60 --RAll, R->, R->, LInt, LFix->*, Ax*
61 bspEx1 = fAll 1 ((var 1 `arrow` Int) `arrow` (Int `arrow` Int))
62
63 --test for LP->
64 --RAll, R->, LP->, LFix->*, La->*1, Ax*
65 bspEx2 = fAll 1 (((TPair (var 1) Int) `arrow` Int) `arrow` Int)
66
67 --test for LP
68 --RAll, R->, LP, LInt, LFix->*, Ax*
69 bspEx3 = fAll 1 ((TPair (var 1 `arrow` Int) Int) `arrow` Int)
70
71 --test for LE->
72 --RAll, R->, LE->, LFix->*, Ax*
73 bspEx4 = fAll 1 (((TEither (var 1) Int) `arrow` Int) `arrow` Int)
74
75 --test for LE->
76 --RAll, R->, LE->, LFix->*, Ax*
77 bspEx5 = fAll 1 (((TEither Int (var 1)) `arrow` Int) `arrow` Int)
78
79 --test for LE1
80 bspEx6 = fAll 1 ((TEither (var 1 `arrow` Int) Int) `arrow` Int)
81
82 --test for LE2
83 bspEx7 = fAll 1 ((TEither Int (var 1 `arrow` Int)) `arrow` Int)
84
85 --another test for LE1
86 bspEx8 = fAll 1 (fAllStar 2 ((TEither (var 1 `arrow` var 2) (var 1 `arrow` Int)) `arrow` ((var 2 `arrow` Int) `arrow` Int)))
87
88 --test for RP1
89 bspEx9 = fAll 1 (TPair (var 1) (var 1))
90
91 --test for RP2
92 bspEx10 = fAll 1 (TPair Int (var 1))
93
94
95 --test for RE1
96 bspEx11 = fAll 1 (TEither (var 1) (var 1))
97
98 --test for RE2
99 bspEx12 = fAll 1 (TEither Int (var 1))
100
101 --test for LP*1
102 bspEx13 = fAll 1 ((var 1 `arrow` (TPair Int Int)) `arrow` Int)
103
104 --test for LP*2
105 bspEx14 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TPair (var 2) Int)) `arrow` Int))
106
107 --test for LE*1
108 bspEx15 = fAll 1 ((var 1 `arrow` (TEither Int Int)) `arrow` Int)
109
110 --test for LE*2
111 bspEx16 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TEither (var 2) Int)) `arrow` Int))
112
113
114
115 -----test cases using HUnit Test--------
116
117 run test = runTestTT test
118
119
120 test1 = TestCase $ assertEqual "a.a: " (Just (Bottom (All (TypVar 1) (TVar (TypVar 1))))) (testTerm bsp1)
121 test2 = TestCase $ assertEqual 
122                      "a.[a] -> [a]:" 
123                      (Just (TAbs (TypVar 1) (Abs (TermVar 1) (List (TVar (TypVar 1))) (Cons (Bottom (TVar (TypVar 1))) (Nil (TVar (TypVar 1)))))))
124                      (testTerm bsp2)
125
126 test3 = TestCase $ assertEqual 
127                      "a.b.(a -> b) -> b:"
128                      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1))))))))
129                      (testTerm bsp3)
130
131 test4 = TestCase $ assertEqual
132                      "a.b.([a] -> b) -> b:"
133                      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (List (TVar (TypVar 1))) (TVar (TypVar 2))) (App (Abs (TermVar 2) (TVar (TypVar 1)) (App (Var (TermVar 1)) (Cons (Var (TermVar 2)) (Nil (TVar (TypVar 1)))))) (Bottom (TVar (TypVar 1))))))))
134                      (testTerm bsp4)
135
136 test5 = TestCase $ assertEqual
137                      "a.b.[b] -> (a -> b) -> b"
138                      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (List (TVar (TypVar 2))) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1)))))))))
139                      (testTerm bsp5)
140
141 test6 = TestCase $ assertEqual
142                      "a.b.a -> (a -> b) -> b"
143                      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (TVar (TypVar 1)) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1)))))))))
144                      (testTerm bsp6)
145                      
146 test7 = TestCase $ assertEqual
147                      "a.b.(((a -> b) -> b) -> b) -> b"
148                      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (Arrow (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (TVar (TypVar 2))) (TVar (TypVar 2))) (App (Var (TermVar 1)) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1))))))))))
149                      (testTerm bsp7)
150
151 test8 = TestCase $ assertEqual
152                      "a.b.(((a -> (b -> b)) -> b) -> b) -> b"
153                      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (Arrow (Arrow (TVar (TypVar 1)) (Arrow (TVar (TypVar 2)) (TVar (TypVar 2)))) (TVar (TypVar 2))) (TVar (TypVar 2))) (App (Var (TermVar 1)) (Abs (TermVar 2) (Arrow (TVar (TypVar 1)) (Arrow (TVar (TypVar 2)) (TVar (TypVar 2)))) (App (App (Var (TermVar 2)) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))))))))))
154                      (testTerm bsp8)
155
156 test9 = TestCase $ assertEqual
157                      "a.b.(a -> b) -> (b -> c) -> c"
158                      (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (TAbs (TypVar 3) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (Abs (TermVar 2) (Arrow (TVar (TypVar 2)) (TVar (TypVar 3))) (App (Var (TermVar 2)) (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))))))))))
159                      (testTerm bsp9)
160
161 test10 = TestCase $ assertEqual
162                       "a.b.(a -> [b]) -> b"
163                       (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2)))) (Case (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))) (TermVar 2) (Var (TermVar 2)))))))
164                       (testTerm bsp10)
165
166 test11 = TestCase $ assertEqual
167                       "a.b.(b -> (a -> b)) -> b"
168                       (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 2)) (Arrow (TVar (TypVar 1)) (TVar (TypVar 2)))) (App (App (Var (TermVar 1)) (Bottom (TVar (TypVar 2)))) (Bottom (TVar (TypVar 1))))))))
169                       (testTerm bsp11)
170
171 test12 = TestCase $ assertEqual
172                       "a.b.c.d.((c -> (a -> [b]) -> b) -> c) -> (b -> [c]) -> (c -> d) -> [d]"
173                       (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (TAbs (TypVar 3) (TAbs (TypVar 4)
174                                (Abs (TermVar 1) (Arrow (Arrow (Arrow (TVar (TypVar 3)) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2))))) (TVar (TypVar 2))) (TVar (TypVar 3)))
175                                  (Abs (TermVar 2) (Arrow (Arrow (TVar (TypVar 2)) (List (TVar (TypVar 3)))) (Arrow (TVar (TypVar 3)) (TVar (TypVar 4))))
176                                (Cons (App 
177                                        (App (Var (TermVar 2)) 
178                                          (Abs (TermVar 3) (TVar (TypVar 2)) 
179                                            (Cons (App (Var (TermVar 1)) (Abs (TermVar 5) 
180                                                                           (Arrow (TVar (TypVar 3)) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2)))))
181                                                                           (Case (App (App (Var (TermVar 5)) (Bottom (TVar (TypVar 3)))) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))) (TermVar 7) (Var (TermVar 7)))
182                                                                         )
183                                                  ) 
184                                   (Nil (TVar (TypVar 3))))
185                                 )) (Bottom (TVar (TypVar 3)))) (Nil (TVar (TypVar 4)))))))))))
186                       (testTerm bsp12)
187
188 testList = [TestLabel "RFix-Test" test1, TestLabel "RAll,R->,RI-Test" test2, TestLabel "RAll*,LFix->*,Ax*-Test" test3, TestLabel "LI->-Test" test4, TestLabel "LI-Test" test5, TestLabel "LFix-Test" test6, TestLabel "L->->-Test" test7, TestLabel "La->*1" test8, TestLabel "La->*2" test9, TestLabel "LI*-Test" test10, TestLabel "LFix->-Test" test11, TestLabel "complex typ" test12 ]
189
190 tests = TestList testList
191
192 testEx1 = TestCase $ assertEqual
193                        "a.(a -> Int) -> Int -> Int"
194                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) Int) (Abs (TermVar 2) Int (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1))))))))
195                        (testTerm bspEx1)
196
197 testEx2 = TestCase $ assertEqual
198                        "a.((a,Int) -> Int) -> Int"
199                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TPair (TVar (TypVar 1)) Int) Int) (App (App (Abs (TermVar 2) (TVar (TypVar 1)) (Abs (TermVar 3) Int (App (Var (TermVar 1))  (Pair (Var (TermVar 2)) (Var (TermVar 3)))))) (Bottom (TVar (TypVar 1)))) (Bottom Int)))))
200                        (testTerm bspEx2)
201 testEx3 = TestCase $ assertEqual
202                        "a.((a -> Int),Int) -> Int"
203                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TPair (Arrow (TVar (TypVar 1)) Int) Int) (App (PCase (Var (TermVar 1)) (TermVar 4) (TermVar 5) (Var (TermVar 4))) (Bottom (TVar (TypVar 1)))))))
204                        (testTerm bspEx3)
205
206 testEx4 = TestCase $ assertEqual
207                        "a.((a+Int) -> Int) -> Int"
208                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TEither (TVar (TypVar 1)) Int) Int) (App (Abs (TermVar 2) (TVar (TypVar 1)) (App (Var (TermVar 1)) (Left (Var (TermVar 2))))) (Bottom (TVar (TypVar 1)))))))
209                        (testTerm bspEx4)
210
211 testEx5 = TestCase $ assertEqual
212                        "a.((Int+a) -> Int) -> Int"
213                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TEither Int (TVar (TypVar 1))) Int) (App (Abs (TermVar 3) (TVar (TypVar 1)) (App (Var (TermVar 1)) (Right (Var (TermVar 3))))) (Bottom (TVar (TypVar 1)))))))
214                        (testTerm bspEx5)
215
216 testEx6 = TestCase $ assertEqual
217                        "a.((a -> Int) + Int) -> Int"
218                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TEither (Arrow (TVar (TypVar 1)) Int) Int) (App (ECase (Var (TermVar 1)) (TermVar 2) (Var (TermVar 2)) (TermVar 3) (Bottom (Arrow (TVar (TypVar 1)) Int))) (Bottom (TVar (TypVar 1)))))))
219                        (testTerm bspEx6)
220
221 testEx7 = TestCase $ assertEqual
222                        "a.(Int + (a -> Int)) -> Int"
223                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (TEither Int (Arrow (TVar (TypVar 1)) Int)) (App (ECase (Var (TermVar 1)) (TermVar 4) (Bottom (Arrow (TVar (TypVar 1)) Int)) (TermVar 5) (Var (TermVar 5))) (Bottom (TVar (TypVar 1)))))))
224                        (testTerm bspEx7)
225
226 testEx8 = TestCase $ assertEqual
227                        "a.b.((a -> b) + (a -> Int)) -> (b -> Int) -> Int"
228                        (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (TEither (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))) (Arrow (TVar (TypVar 1)) Int)) (Abs (TermVar 2) (Arrow (TVar (TypVar 2)) Int) (App (Var (TermVar 2)) (App (ECase (Var (TermVar 1)) (TermVar 3) (Var (TermVar 3)) (TermVar 4) (Bottom (Arrow (TVar (TypVar 1)) (TVar (TypVar 2))))) (Bottom (TVar (TypVar 1))))))))))
229                        (testTerm bspEx8)
230
231 testEx9 = TestCase $ assertEqual
232                        "a.(a,a)"
233                        (Just (TAbs (TypVar 1) (Pair (Bottom (TVar (TypVar 1))) (Bottom (TVar (TypVar 1))))))
234                        (testTerm bspEx9)
235
236 testEx10 = TestCase $ assertEqual
237                        "a.(Int,a)"
238                        (Just (TAbs (TypVar 1) (Pair (Bottom Int) (Bottom (TVar (TypVar 1))))))
239                        (testTerm bspEx10)
240
241 testEx11 = TestCase $ assertEqual
242                        "a.(a+a)"
243                        (Just (TAbs (TypVar 1) (Left (Bottom (TVar (TypVar 1))) )))
244                        (testTerm bspEx11)
245
246 testEx12 = TestCase $ assertEqual
247                        "a.(a+a)"
248                        (Just (TAbs (TypVar 1) (Right (Bottom (TVar (TypVar 1))))))
249                        (testTerm bspEx12)
250
251 testEx13 = TestCase $ assertEqual
252                        "a.(a -> (Int,Int)) -> Int"
253                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TPair Int Int)) (PCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (TermVar 5) (Var (TermVar 5))))))
254                        (testTerm bspEx13)
255
256 testEx14 = TestCase $ assertEqual
257                        "a.b.(a -> (b,Int)) -> Int"
258                        (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TPair (TVar (TypVar 2)) Int)) (PCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (TermVar 5) (Var (TermVar 5)))))))
259                        (testTerm bspEx14)
260
261 testEx15 = TestCase $ assertEqual
262                        "a.(a -> (Int+Int)) -> Int"
263                        (Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TEither Int Int)) (ECase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 2) (Var (TermVar 2)) (TermVar 3) (Bottom Int)))))
264                        (testTerm bspEx15)
265
266 testEx16 = TestCase $ assertEqual
267                        "a.b.(a -> (b+Int)) -> Int"
268                        (Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (TEither (TVar (TypVar 2)) Int)) (ECase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (TermVar 4) (Bottom (TVar (TypVar 2))) (TermVar 5) (Var (TermVar 5)))))))
269                        (testTerm bspEx16)
270
271 exTestList = [TestLabel "LInt" testEx1, TestLabel "LP->" testEx2, TestLabel "LP" testEx3, TestLabel "LE-> (Left)" testEx4, TestLabel "LE-> (Right)" testEx5, TestLabel "LE1" testEx6, TestLabel "LE2" testEx7 , TestLabel "LE1 complex" testEx8, TestLabel "RP1" testEx9, TestLabel "RP2" testEx10, TestLabel "RE1" testEx11, TestLabel "RE2" testEx12, TestLabel "LP*1" testEx13, TestLabel "LP*2" testEx14, TestLabel "LE*1" testEx15, TestLabel "LE*2" testEx16]
272
273 exTests = TestList exTestList
274
275 allTests = TestList (testList ++ exTestList)
276
277
278 testbsp = ( fAll 1 ( ( ((List Int) `arrow` var 1 ) `arrow` Int ) `arrow` Int ) )