-
Notifications
You must be signed in to change notification settings - Fork 8
Expand file tree
/
Copy pathInternalTypeGen.hs
More file actions
211 lines (176 loc) · 7.25 KB
/
Copy pathInternalTypeGen.hs
File metadata and controls
211 lines (176 loc) · 7.25 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, TypeFamilies, LambdaCase, FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances, FunctionalDependencies #-}
module InternalTypeGen where
import Data.List (isInfixOf, elemIndex, nub, drop, reverse, intersect)
import Control.Monad
import Control.Monad.State
import Control.Monad.Logic
import Data.Data
import Text.Printf
import System.IO.Silently
import Control.Lens
import Debug.Trace
import qualified Test.LeanCheck.Function.ShowFunction as SF
import qualified Test.LeanCheck.Core as SF
import qualified Test.ChasingBottoms as CB
import qualified Test.SmallCheck.Series as SS
import qualified Test.QuickCheck as QC
defaultShowFunctionDepth = 4 :: Int
defaultMaxOutputLength = 10 :: CB.Nat
defaultSeriesLimit = 5 :: Int
instance Eq a => Eq (CB.Result a) where
(CB.Value a) == (CB.Value b) = a == b
CB.NonTermination == CB.NonTermination = True
(CB.Exception _) == (CB.Exception _) = True
_ == _ = False
isFailedResult :: CB.Result String -> Bool
isFailedResult result = case result of
CB.NonTermination -> True
CB.Exception _ -> True
CB.Value a | "_|_" `isInfixOf` a -> True
CB.Value a | "Exception" `isInfixOf` a -> True
_ -> False
data MyInt = MOne | Zero | One | Two | Other Int deriving (Eq)
instance Show MyInt where
show = show . toInt
toInt :: MyInt -> Int
toInt MOne = -1
toInt Zero = 0
toInt One = 1
toInt Two = 2
toInt (Other n) = n
toMyInt :: Int -> MyInt
toMyInt (-1) = MOne
toMyInt 0 = Zero
toMyInt 1 = One
toMyInt 2 = Two
toMyInt n = Other n
instance SF.Listable MyInt where
tiers = SF.cons0 MOne SF.\/
SF.cons0 Zero SF.\/
SF.cons0 One SF.\/
SF.cons0 Two SF.\/
SF.cons1 Other
instance Monad m => SS.Serial m MyInt where
series = SS.cons0 MOne SS.\/
SS.cons0 Zero SS.\/
SS.cons0 One SS.\/
SS.cons0 Two
instance Monad m => SS.CoSerial m MyInt where
coseries r = let rs = SS.limit defaultSeriesLimit r
in SS.alts0 rs >>- \z1 ->
SS.alts0 rs >>- \z2 ->
SS.alts0 rs >>- \z3 ->
SS.alts0 rs >>- \z4 ->
return $ \x ->
case x of
MOne -> z1
Zero -> z2
One -> z3
Two -> z4
newtype MyFun a b = MyFun (a -> b)
instance (QC.CoArbitrary a, QC.Arbitrary b) => QC.Arbitrary (MyFun a b) where
arbitrary = liftM MyFun QC.arbitrary
instance (QC.Arbitrary a, QC.CoArbitrary b) => QC.CoArbitrary (MyFun a b) where
coarbitrary (MyFun f) = QC.coarbitrary f
instance {-# OVERLAPPABLE #-} (SS.Serial m b, SS.CoSerial m a) => SS.Serial m (MyFun a b) where
series = SS.coseries SS.series >>-
\f -> return (MyFun f)
instance {-# OVERLAPPING #-} Monad m => SS.Serial m (MyFun Int Int) where
series = (SS.generate $ \_ -> map MyFun [\x -> x + 1
,\x -> x * x
,\x -> x * 3]) SS.\/
SS.newtypeCons MyFun
instance {-# OVERLAPPING #-} Monad m => SS.Serial m (MyFun MyInt Int) where
series = (SS.generate $ \_ -> map MyFun [\x -> toInt x + 1
,\x -> toInt x * toInt x
,\x -> toInt x * 3]) SS.\/
(SS.coseries SS.series >>-
\f -> return (MyFun f))
instance {-# OVERLAPPING #-} Monad m => SS.Serial m (MyFun [Int] [Int]) where
series = (SS.generate $ \_ -> map MyFun [\x -> x ++ x]) SS.\/
SS.newtypeCons MyFun
instance (SS.CoSerial m a, SS.Serial m a, SS.Serial m b, SS.CoSerial m b) => SS.CoSerial m (MyFun a b) where
coseries rs = SS.newtypeAlts rs >>- \f ->
return $ \(MyFun x) -> f x
instance {-# OVERLAPPABLE #-} (Show a, SF.Listable a, SF.ShowFunction b) => Show (MyFun a b) where
show (MyFun f) = "(" ++ SF.showFunctionLine defaultShowFunctionDepth f ++ ")"
instance {-# OVERLAPPING #-} (SF.ShowFunction b) => Show (MyFun MyInt b) where
show (MyFun f) = "(" ++ SF.showFunctionLine defaultShowFunctionDepth (\x -> f (toMyInt x)) ++ ")"
instance SF.ShowFunction MyInt where
bindtiers = SF.bindtiers . toInt
instance (Show a, SF.Listable a, SF.ShowFunction b) => SF.ShowFunction (MyFun a b) where
bindtiers (MyFun f) = SF.bindtiers f
class Unwrappable a b where
unwrap :: a -> b
wrap :: b -> a
instance {-# OVERLAPPABLE #-} (a ~ b) => Unwrappable a b where
unwrap = id
wrap = id
instance Unwrappable MyInt Int where
unwrap = toInt
wrap = toMyInt
instance (Unwrappable a c, Unwrappable b d) => Unwrappable (MyFun a b) (c -> d) where
unwrap (MyFun f) = \x -> unwrap (f (wrap x))
wrap f = MyFun $ \x -> wrap (f (unwrap x))
instance (Unwrappable a b) => Unwrappable [a] [b] where
unwrap = map unwrap
wrap = map wrap
instance {-# OVERLAPPING #-} (Unwrappable a b) => Unwrappable (Maybe a) (Maybe b) where
unwrap = fmap unwrap
wrap = fmap wrap
instance (Unwrappable a c, Unwrappable b d) => Unwrappable (a, b) (c, d) where
unwrap (x, y) = (unwrap x, unwrap y)
wrap (x, y) = (wrap x, wrap y)
showCBResult :: CB.Result String -> String
showCBResult = \case
CB.Value a | "_|_" `isInfixOf` a -> "bottom"
CB.Value a -> a
CB.NonTermination -> "diverge"
CB.Exception ex -> show ex
anyDuplicate :: Eq a => [a] -> Bool
-- anyDuplicate xs = length (nub xs) /= length xs
anyDuplicate [] = False
anyDuplicate (x:xs) = x `elem` xs
-- * instance defined in `Types.IOFormat`
data Example = Example {
inputs :: [String],
output :: String
} deriving(Eq, Show)
type ExampleGeneration m = StateT [Example] m
evaluateIOQC :: Show a => [String] -> a -> ExampleGeneration IO String
evaluateIOQC inputs val = do
let result = show val
modify ((Example inputs result):)
return result
evaluateIO :: Data a => Int -> [String] -> [a] -> ExampleGeneration IO ([CB.Result String])
evaluateIO timeInMicro inputs vals = do
results <- liftIO $ silence $ mapM (CB.timeOutMicro timeInMicro . eval) vals
let resultsStr = map showCBResult results
modify ((++) (map (Example inputs) resultsStr))
return results
where
evalStr val = CB.approxShow defaultMaxOutputLength val
io str = ((putStrLn str) >> return str)
eval val = io (evalStr val)
waitState :: Int -> [String] -> [String] -> [[String]] -> CB.Result String -> ExampleGeneration IO Bool
waitState numIOs args previousRets previousArgs ret = case (not $ isFailedResult ret) of
False -> pure False
_ -> do
ioState <- get
let retStr = showCBResult ret
when (retIsNotInState retStr ioState && paramsIsNotInState args ioState)
(modify ((:) (Example args retStr)))
state <- get
return ((length state) == numIOs)
where
retIsNotInState retStr state = not $ ((retStr `elem` (map output state)) || (retStr `elem` previousRets))
paramsIsNotInState params state = not (anyCommonArgs params (map inputs state ++ previousArgs))
-- modify 2020/04/22 by Zheng
-- only compare arguments in the same position, intersect is too strict
anyCommonArgs :: [String] -> [[String]] -> Bool
anyCommonArgs args inputs = or $ map (compare args) inputs
where
compare :: [String] -> [String] -> Bool
compare xs = any (uncurry (==)) . zip xs