free-theorems-counterexamples-0.3: Language/Haskell/FreeTheorems/Variations/CounterExamples/Test/TestItExt.hs
module Language.Haskell.FreeTheorems.Variations.CounterExamples.Test.TestItExt where
import Test.HUnit
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Internal.ExFindExtended
import Prelude hiding (Either(..))
import Language.Haskell.FreeTheorems.Variations.CounterExamples.Parser.ParseType (parseType)
-------------------------------------------------------------------------------------------------
---TestBeispiele fuer ExFind---------------------------------------------------------------------
---um alle Tests auszufuehren runTestTT tests aufrufen-----------------------------------------
---fuer einzelne Tests runTestTT test1 bzw. die entsprechenden Nummer statt 1-------------------
---fuer Anzeige der bei der Ableitung benutzten Regeln getTerm bsp1 bzw. entsprechende Nr------
-------------------------------------------------------------------------------------------------
---shortcuts---
fAll i = All (TypVar i)
fAllStar i = AllStar (TypVar i)
tau1 `arrow` tau2 = Arrow tau1 tau2
var i = TVar (TypVar i)
--Beispiele:
-- RFix
bsp1 = fAll 1 (var 1)
-- RAll, R->, RI, RFix
bsp2 = fAll 1 (List (var 1) `arrow` List (var 1))
-- RAll, RAllStar, R->, LFixArrowStar, AxStar
bsp3 = fAll 1 (fAllStar 2 ((var 1 `arrow` var 2) `arrow` var 2))
-- RAll, RAllStar, R->, LIArrow, LFixArrowStar, AxStar
bsp4 = fAll 1 (fAllStar 2 ((List (var 1) `arrow` var 2) `arrow` var 2))
-- test for LI
-- RAll, RAllStar, R->, R->, LI, LFixArrowStar, AxStar
bsp5 = fAll 1 (fAllStar 2 ((List (var 2)) `arrow` ((var 1 `arrow` var 2) `arrow` var 2)))
-- test for LFix
-- RAll, RAllStar, R->, R->, LFix, LFixArrowStar, AxStar
bsp6 = fAll 1 (fAllStar 2 ( var 1 `arrow` ((var 1 `arrow` var 2) `arrow` var 2)))
-- test for L->->
-- RAll, RAllStar, R->, L->-> (fst: LFix->*, Ax*) (snd: Ax*)
bsp7 = fAll 1 (fAllStar 2 (((( var 1 `arrow` var 2) `arrow` var 2) `arrow` var 2) `arrow` var 2))
-- test for La->*1
-- RAll, RAllStar, R->, L->-> (fst: LFix->*, La->*1, Ax*) (snd: Ax*)
bsp8 = fAll 1 (fAllStar 2 (((( var 1 `arrow` (var 2 `arrow` var 2)) `arrow` var 2) `arrow` var 2) `arrow` var 2))
-- test for La->*2
-- RAll, RAllStar, R->, R->, LFix->*, La->*2, Ax*
bsp9 = fAll 1 (fAllStar 2 (fAllStar 3 (((var 1 `arrow` var 2) `arrow` ((var 2 `arrow` var 3) `arrow` var 3)))))
bsp10 = fAll 1 (fAllStar 2 ((var 1 `arrow` (List (var 2))) `arrow` var 2))
-- test for LFix
-- RAll, RAllStar, R->, LFix->, LFix->*, Ax*
bsp11 = fAll 1 (fAllStar 2 ((var 2 `arrow` (var 1 `arrow` var 2)) `arrow` var 2))
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))))))))
-----new examples for the extended algorithm-------
--test for LInt
--RAll, R->, R->, LInt, LFix->*, Ax*
bspEx1 = fAll 1 ((var 1 `arrow` Int) `arrow` (Int `arrow` Int))
--test for LP->
--RAll, R->, LP->, LFix->*, La->*1, Ax*
bspEx2 = fAll 1 (((TPair (var 1) Int) `arrow` Int) `arrow` Int)
--test for LP
--RAll, R->, LP, LInt, LFix->*, Ax*
bspEx3 = fAll 1 ((TPair (var 1 `arrow` Int) Int) `arrow` Int)
--test for LE->
--RAll, R->, LE->, LFix->*, Ax*
bspEx4 = fAll 1 (((TEither (var 1) Int) `arrow` Int) `arrow` Int)
--test for LE->
--RAll, R->, LE->, LFix->*, Ax*
bspEx5 = fAll 1 (((TEither Int (var 1)) `arrow` Int) `arrow` Int)
--test for LE1
bspEx6 = fAll 1 ((TEither (var 1 `arrow` Int) Int) `arrow` Int)
--test for LE2
bspEx7 = fAll 1 ((TEither Int (var 1 `arrow` Int)) `arrow` Int)
--another test for LE1
bspEx8 = fAll 1 (fAllStar 2 ((TEither (var 1 `arrow` var 2) (var 1 `arrow` Int)) `arrow` ((var 2 `arrow` Int) `arrow` Int)))
--test for RP1
bspEx9 = fAll 1 (TPair (var 1) (var 1))
--test for RP2
bspEx10 = fAll 1 (TPair Int (var 1))
--test for RE1
bspEx11 = fAll 1 (TEither (var 1) (var 1))
--test for RE2
bspEx12 = fAll 1 (TEither Int (var 1))
--test for LP*1
bspEx13 = fAll 1 ((var 1 `arrow` (TPair Int Int)) `arrow` Int)
--test for LP*2
bspEx14 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TPair (var 2) Int)) `arrow` Int))
--test for LE*1
bspEx15 = fAll 1 ((var 1 `arrow` (TEither Int Int)) `arrow` Int)
--test for LE*2
bspEx16 = fAll 1 (fAllStar 2 ((var 1 `arrow` (TEither (var 2) Int)) `arrow` Int))
-----test cases using HUnit Test--------
run test = runTestTT test
test1 = TestCase $ assertEqual "a.a: " (Just (Bottom (All (TypVar 1) (TVar (TypVar 1))))) (testTerm bsp1)
test2 = TestCase $ assertEqual
"a.[a] -> [a]:"
(Just (TAbs (TypVar 1) (Abs (TermVar 1) (List (TVar (TypVar 1))) (Cons (Bottom (TVar (TypVar 1))) (Nil (TVar (TypVar 1)))))))
(testTerm bsp2)
test3 = TestCase $ assertEqual
"a.b.(a -> b) -> b:"
(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))))))))
(testTerm bsp3)
test4 = TestCase $ assertEqual
"a.b.([a] -> b) -> b:"
(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))))))))
(testTerm bsp4)
test5 = TestCase $ assertEqual
"a.b.[b] -> (a -> b) -> b"
(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)))))))))
(testTerm bsp5)
test6 = TestCase $ assertEqual
"a.b.a -> (a -> b) -> b"
(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)))))))))
(testTerm bsp6)
test7 = TestCase $ assertEqual
"a.b.(((a -> b) -> b) -> b) -> b"
(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))))))))))
(testTerm bsp7)
test8 = TestCase $ assertEqual
"a.b.(((a -> (b -> b)) -> b) -> b) -> b"
(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))))))))))
(testTerm bsp8)
test9 = TestCase $ assertEqual
"a.b.(a -> b) -> (b -> c) -> c"
(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)))))))))))
(testTerm bsp9)
test10 = TestCase $ assertEqual
"a.b.(a -> [b]) -> b"
(Just (TAbs (TypVar 1) (TAbs (TypVar 2) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2)))) (LCase (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))) (TermVar 2) (Var (TermVar 2)))))))
(testTerm bsp10)
test11 = TestCase $ assertEqual
"a.b.(b -> (a -> b)) -> b"
(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))))))))
(testTerm bsp11)
test12 = TestCase $ assertEqual
"a.b.c.d.((c -> (a -> [b]) -> b) -> c) -> (b -> [c]) -> (c -> d) -> [d]"
(Just (TAbs (TypVar 1) (TAbs (TypVar 2) (TAbs (TypVar 3) (TAbs (TypVar 4)
(Abs (TermVar 1) (Arrow (Arrow (Arrow (TVar (TypVar 3)) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2))))) (TVar (TypVar 2))) (TVar (TypVar 3)))
(Abs (TermVar 2) (Arrow (Arrow (TVar (TypVar 2)) (List (TVar (TypVar 3)))) (Arrow (TVar (TypVar 3)) (TVar (TypVar 4))))
(Cons (App
(App (Var (TermVar 2))
(Abs (TermVar 3) (TVar (TypVar 2))
(Cons (App (Var (TermVar 1)) (Abs (TermVar 5)
(Arrow (TVar (TypVar 3)) (Arrow (TVar (TypVar 1)) (List (TVar (TypVar 2)))))
(LCase (App (App (Var (TermVar 5)) (Bottom (TVar (TypVar 3)))) (Bottom (TVar (TypVar 1)))) (Bottom (TVar (TypVar 2))) (TermVar 7) (Var (TermVar 7)))
)
)
(Nil (TVar (TypVar 3))))
)) (Bottom (TVar (TypVar 3)))) (Nil (TVar (TypVar 4)))))))))))
(testTerm bsp12)
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 ]
tests = TestList testList
testEx1 = TestCase $ assertEqual
"a.(a -> Int) -> Int -> Int"
(Just (TAbs (TypVar 1) (Abs (TermVar 1) (Arrow (TVar (TypVar 1)) Int) (Abs (TermVar 2) Int (App (Var (TermVar 1)) (Bottom (TVar (TypVar 1))))))))
(testTerm bspEx1)
testEx2 = TestCase $ assertEqual
"a.((a,Int) -> Int) -> Int"
(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)))))
(testTerm bspEx2)
testEx3 = TestCase $ assertEqual
"a.((a -> Int),Int) -> Int"
(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)))))))
(testTerm bspEx3)
testEx4 = TestCase $ assertEqual
"a.((a+Int) -> Int) -> Int"
(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)))))))
(testTerm bspEx4)
testEx5 = TestCase $ assertEqual
"a.((Int+a) -> Int) -> Int"
(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)))))))
(testTerm bspEx5)
testEx6 = TestCase $ assertEqual
"a.((a -> Int) + Int) -> Int"
(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)))))))
(testTerm bspEx6)
testEx7 = TestCase $ assertEqual
"a.(Int + (a -> Int)) -> Int"
(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)))))))
(testTerm bspEx7)
testEx8 = TestCase $ assertEqual
"a.b.((a -> b) + (a -> Int)) -> (b -> Int) -> Int"
(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))))))))))
(testTerm bspEx8)
testEx9 = TestCase $ assertEqual
"a.(a,a)"
(Just (TAbs (TypVar 1) (Pair (Bottom (TVar (TypVar 1))) (Bottom (TVar (TypVar 1))))))
(testTerm bspEx9)
testEx10 = TestCase $ assertEqual
"a.(Int,a)"
(Just (TAbs (TypVar 1) (Pair (Bottom Int) (Bottom (TVar (TypVar 1))))))
(testTerm bspEx10)
testEx11 = TestCase $ assertEqual
"a.(a+a)"
(Just (TAbs (TypVar 1) (Left (Bottom (TVar (TypVar 1))) )))
(testTerm bspEx11)
testEx12 = TestCase $ assertEqual
"a.(a+a)"
(Just (TAbs (TypVar 1) (Right (Bottom (TVar (TypVar 1))))))
(testTerm bspEx12)
testEx13 = TestCase $ assertEqual
"a.(a -> (Int,Int)) -> Int"
(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))))))
(testTerm bspEx13)
testEx14 = TestCase $ assertEqual
"a.b.(a -> (b,Int)) -> Int"
(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)))))))
(testTerm bspEx14)
testEx15 = TestCase $ assertEqual
"a.(a -> (Int+Int)) -> Int"
(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)))))
(testTerm bspEx15)
testEx16 = TestCase $ assertEqual
"a.b.(a -> (b+Int)) -> Int"
(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)))))))
(testTerm bspEx16)
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]
exTests = TestList exTestList
allTests = TestList (testList ++ exTestList)
testbsp = ( fAll 1 ( ( ((List Int) `arrow` var 1 ) `arrow` Int ) `arrow` Int ) )