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