Danies Ă„nderungen von 20081114
[darcs-mirror-polyfix.git] / TestGen.hs
1 -- |This module uses "Test.Quickcheck" to test the PolyFix package by generating randomly 100 different types
2 -- running ExFind with that type and then simplifying the generated free theorem
3 -- to a antilogy of the kind \"() = _|_\" or \"0 = _|_\".
4 module TestGen where
5 import Test.QuickCheck
6 --import ParseType (parseType')
7 import SimpleFT  (freeTheorem)
8 import Expr (specialize,BoolExpr(..),Expr(..))
9 import ExFindExtended (getCompleteRaw, showTerm, showUsedTermCont,Typ(..),TypVar(..),showTyp,printTyp,testTerm)
10
11 import Foreign
12 --import Language.Haskell.FreeTheorems.Parser.Haskell98 as FTP
13 --import Language.Haskell.FreeTheorems
14 --      ( runChecks
15 --      , check
16 --      , filterSignatures
17 --      , prettyTheorem
18 --      , asTheorem
19 --      , interpret
20 --      , unfoldLifts
21 --      , prettyUnfoldedLift
22 --      , LanguageSubset(BasicSubset)
23 --      )
24 import Term2Expr (term2Expr, termCond2Exprs, insertTermsInCondition)
25
26 import List (sort,nub)
27 import Control.Monad (liftM, liftM2)
28 import Debug.Trace
29 import TestItExt
30
31 testrun typ = case getCompleteRaw typ of
32               Left _  -> Left "Error in type."
33               Right p ->  Right (insertTermsInCondition p (specialize (freeTheorem typ)))
34
35 -- *Generation of example types
36
37 newtype UnpointedVar = UnpointedVar Int
38 newtype PointedVar = PointedVar Int
39
40 -- |restricting the range of unpointed type variables
41 --instance Arbitrary UnpointedVar where
42 --  arbitrary = oneof [1,2,3]
43
44 -- |restricting the range of pointed type variables
45 --instance Arbitrary PointedVar where
46 --  arbitrary = oneof [4,5,6]
47
48 -- |TypVar generator
49 instance Arbitrary TypVar where
50 --  arbitrary = oneof [UnpointedVar arbitrary, PointedVar arbitrary]
51   arbitrary = oneof [return (TypVar 1), return (TypVar 2), return(TypVar 3), return(TypVar 4), return (TypVar 5), return (TypVar 6)]
52
53 -- |recursive type generator
54 instance Arbitrary Typ where
55   arbitrary = quantify (sized typ')
56     where typ' 0 = frequency [(1, return Int), (6, liftM TVar arbitrary)]
57           typ' n | n>0 =
58                frequency [(1, liftM TVar arbitrary), (2,liftM2 Arrow subtyp1 subtyp1), (1,liftM List subtyp2), 
59                       (1,return Int), (1,liftM2 TPair subtyp1 subtyp1), (1,liftM2 TEither subtyp1 subtyp1)]
60             where subtyp1 = typ' (n `div` 2)
61                   subtyp2 = typ' (n-1)
62           quantify t = do {tau <- t;
63                            return (addquantifiers tau (usedvars tau []))
64                           }
65           usedvars tau vars = case tau of
66                                 TVar (TypVar i) -> (i:vars)
67                                 Arrow t1 t2     -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
68                                 List t1         -> (usedvars t1 []) ++ vars
69                                 Int             -> vars
70                                 TPair t1 t2     -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
71                                 TEither t1 t2   -> (usedvars t1 []) ++ (usedvars t2 []) ++ vars
72 --                              _               -> vars
73           addquantifiers tau l =  case reverse.sort.nub $ l of
74                                     []   -> tau
75                                     x:xs -> if x < 4 
76                                             then addquantifiers (AllStar (TypVar x) tau) xs
77                                             else addquantifiers (All (TypVar x) tau) xs
78
79
80 -- *test properties
81 -- |returns only True if the free theorem with the example produced leads to the contradiction "() == _|_"
82 -- or "0 == _|_"
83 prop_CompletelySolved::Typ -> Bool
84 prop_CompletelySolved typ = 
85     case getCompleteRaw typ of
86       Left _  -> False
87       Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
88                    Equal Zero Bottom  -> True
89                    Equal EUnit Bottom -> True
90                    _                  -> False
91
92
93 -- |returns only True if the free theorem with the example produced leads to the an expression of the form "expr1 == expr2"
94 prop_DownToEqual typ =
95     case getCompleteRaw typ of
96       Left _  -> False
97       Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
98                    Equal _ _  -> True
99                    _          -> False
100
101 prop_Test typ = trace (showTyp typ) True
102
103 --prop_Classified :: Typ -> IO Property
104 prop_Classified typ = 
105 --    do {print typ;
106 --error (showTyp typ)
107 --      return (
108         trace (showTyp typ)
109         (classify (noTerm) "No Term." $
110         classify (equal) "Reduced to Equal" $
111         classify (precond) "Still with Precondition" $
112         classify (true) "True" $
113         True)
114 --       }
115   where noTerm = case testTerm typ of
116                    Nothing -> True
117                    _       -> False
118         equal = if not noTerm 
119                 then
120                   case getCompleteRaw typ of
121                     Left _  -> False
122                     Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
123                                  Equal _ _  -> True
124                                  _          -> False
125                 else False
126         precond = if not noTerm 
127                   then
128                     case getCompleteRaw typ of
129                       Left _  -> False
130                       Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
131                                    Equal _ _  -> False
132                                    And []     -> False
133                                    _          -> True
134                   else False
135         true    = if not noTerm 
136                   then
137                     case getCompleteRaw typ of
138                       Left _  -> False
139                       Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of                              
140                                    And []     -> True
141                                    _          -> False
142                   else False
143
144 check_Classified typ test = case test of
145                              1 -> noTerm
146                              2 -> equal
147                              3 -> precond
148                              4 -> true
149   where noTerm = case testTerm typ of
150                    Nothing -> True
151                    _       -> False
152         equal = if not noTerm 
153                 then
154                   case getCompleteRaw typ of
155                     Left _  -> False
156                     Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
157                                  Equal _ _  -> True
158                                  _          -> False
159                 else False
160         precond = if not noTerm 
161                   then
162                     case getCompleteRaw typ of
163                       Left _  -> False
164                       Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of
165                                    Equal _ _  -> False
166                                    And []     -> False
167                                    _          -> True
168                   else False
169         true    = if not noTerm 
170                   then
171                     case getCompleteRaw typ of
172                       Left _  -> False
173                       Right p -> case (insertTermsInCondition p (specialize (freeTheorem typ))) of                              
174                                    And []     -> True
175                                    _          -> False
176                   else False
177
178 prop_HowManyTerms typ =
179     classify (findsTerm)  "Term" $
180     classify (not findsTerm) "No Term" $
181     True
182   where findsTerm = if (testTerm typ) == Nothing then False else True
183
184 mainTest = quickCheck prop_Classified