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 ) )