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