/
Property.hs
369 lines (311 loc) · 10.4 KB
/
Property.hs
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
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
-- vim:fdm=marker:foldtext=foldtext()
--------------------------------------------------------------------
-- |
-- Module : Test.SmallCheck.Property
-- Copyright : (c) Colin Runciman et al.
-- License : BSD3
-- Maintainer: Roman Cheplyaka <roma@ro-che.info>
--
-- Properties and tools to construct them.
--------------------------------------------------------------------
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeFamilies,
ScopedTypeVariables, DeriveDataTypeable #-}
-- CPP is for Typeable1 vs Typeable
{-# LANGUAGE CPP #-}
-- Are we using new, polykinded and derivable Typeable yet?
#define NEWTYPEABLE MIN_VERSION_base(4,7,0)
#if NEWTYPEABLE
{-# LANGUAGE Safe #-}
#else
-- Trustworthy is needed because of the hand-written Typeable instance
{-# LANGUAGE Trustworthy #-}
#endif
module Test.SmallCheck.Property (
-- * Constructors
forAll, exists, existsUnique, over, (==>), monadic, changeDepth, changeDepth1,
-- * Property's entrails
Property,
PropertySuccess(..), PropertyFailure(..), runProperty, TestQuality(..), Argument, Reason, Depth, Testable(..),
) where
import Test.SmallCheck.Series
import Test.SmallCheck.Series.Types
import Test.SmallCheck.Property.Result
import Control.Monad
import Control.Monad.Logic
import Control.Monad.Reader
import Control.Applicative
import Data.Typeable
------------------------------
-- Property-related types
------------------------------
--{{{
-- | The type of properties over the monad @m@
newtype Property m = Property { unProperty :: Reader (Env m) (PropertySeries m) }
#if NEWTYPEABLE
deriving Typeable
#endif
data PropertySeries m =
PropertySeries
{ searchExamples :: Series m PropertySuccess
, searchCounterExamples :: Series m PropertyFailure
, searchClosest :: Series m (Property m, [Argument])
}
data Env m =
Env
{ quantification :: Quantification
, testHook :: TestQuality -> m ()
}
data Quantification
= Forall
| Exists
| ExistsUnique
data TestQuality
= GoodTest
| BadTest
deriving (Eq, Ord, Enum, Show)
#if !NEWTYPEABLE
-- Typeable here is not polykinded yet, and also GHC doesn't know how to
-- derive this.
instance Typeable1 m => Typeable (Property m)
where
typeOf _ =
mkTyConApp
(mkTyCon3 "smallcheck" "Test.SmallCheck.Property" "Property")
[typeOf (undefined :: m ())]
#endif
-- }}}
------------------------------------
-- Property runners and constructors
------------------------------------
--{{{
unProp :: Env t -> Property t -> PropertySeries t
unProp q (Property p) = runReader p q
runProperty
:: Monad m
=> Depth
-> (TestQuality -> m ())
-> Property m
-> m (Maybe PropertyFailure)
runProperty depth hook prop =
(\l -> runLogicT l (\x _ -> return $ Just x) (return Nothing)) $
runSeries depth $
searchCounterExamples $
flip runReader (Env Forall hook) $
unProperty prop
atomicProperty
:: Monad m
=> Series m PropertySuccess
-> Series m PropertyFailure
-> PropertySeries m
atomicProperty s f =
let prop = PropertySeries s f (pure (Property $ pure prop, []))
in prop
makeAtomic :: Monad m => Property m -> Property m
makeAtomic (Property prop) =
Property $ flip fmap prop $ \ps ->
atomicProperty (searchExamples ps) (searchCounterExamples ps)
-- | @'over' s $ \\x -> p x@ makes @x@ range over the 'Series' @s@ (by
-- default, all variables range over the 'series' for their types).
--
-- Note that, unlike the quantification operators, this affects only the
-- variable following the operator and not subsequent variables.
--
-- 'over' does not affect the quantification context.
over
:: (Show a, Testable m b)
=> Series m a -> (a -> b) -> Property m
over = testFunction
-- | Execute a monadic test
monadic :: Testable m a => m a -> Property m
monadic a =
Property $ reader $ \env ->
let pair = unProp env . freshContext <$> lift a in
atomicProperty
(searchExamples =<< pair)
(searchCounterExamples =<< pair)
-- }}}
-------------------------------
-- Testable class and instances
-------------------------------
-- {{{
-- | Class of tests that can be run in a monad. For pure tests, it is
-- recommended to keep their types polymorphic in @m@ rather than
-- specialising it to 'Identity'.
class Monad m => Testable m a where
test :: a -> Property m
instance Monad m => Testable m Bool where
test b = Property $ reader $ \env ->
let
success = do
lift $ testHook env GoodTest
if b then return $ PropertyTrue Nothing else mzero
failure = PropertyFalse Nothing <$ lnot success
in atomicProperty success failure
-- | Works like the 'Bool' instance, but includes an explanation of the result.
--
-- 'Left' and 'Right' correspond to test failure and success
-- respectively.
instance Monad m => Testable m (Either Reason Reason) where
test r = Property $ reader $ \env ->
let
success = do
lift $ testHook env GoodTest
either (const mzero) (pure . PropertyTrue . Just) r
failure = do
lift $ testHook env GoodTest
either (pure . PropertyFalse . Just) (const mzero) r
in atomicProperty success failure
instance (Serial m a, Show a, Testable m b) => Testable m (a->b) where
test = testFunction series
instance (Monad m, m ~ n) => Testable n (Property m) where
test = id
testFunction
:: (Show a, Testable m b)
=> Series m a -> (a -> b) -> Property m
testFunction s f = Property $ reader $ \env ->
let
closest = do
x <- s
(p, args) <- searchClosest $ unProp env $ test $ f x
return (p, show x : args)
in
case quantification env of
Forall -> PropertySeries success failure closest
-- {{{
where
failure = do
x <- s
failure <- searchCounterExamples $ unProp env $ test $ f x
let arg = show x
return $
case failure of
CounterExample args etc -> CounterExample (arg:args) etc
_ -> CounterExample [arg] failure
success = PropertyTrue Nothing <$ lnot failure
-- }}}
Exists -> PropertySeries success failure closest
-- {{{
where
success = do
x <- s
s <- searchExamples $ unProp env $ test $ f x
let arg = show x
return $
case s of
Exist args etc -> Exist (arg:args) etc
_ -> Exist [arg] s
failure = NotExist <$ lnot success
-- }}}
ExistsUnique -> PropertySeries success failure closest
-- {{{
where
search = atMost 2 $ do
(prop, args) <- closest
ex <- once $ searchExamples $ unProp env $ test prop
return (args, ex)
success =
search >>=
\examples ->
case examples of
[(x,s)] -> return $ ExistUnique x s
_ -> mzero
failure =
search >>=
\examples ->
case examples of
[] -> return NotExist
(x1,s1):(x2,s2):_ -> return $ AtLeastTwo x1 s1 x2 s2
_ -> mzero
-- }}}
atMost :: MonadLogic m => Int -> m a -> m [a]
atMost n m
| n <= 0 = return []
| otherwise = do
m' <- msplit m
case m' of
Nothing -> return []
Just (x,rest) ->
(x:) `liftM` atMost (n-1) rest
-- }}}
------------------------------
-- Test constructors
------------------------------
-- {{{
quantify :: Monad m => Quantification -> Property m -> Property m
quantify q (Property a) =
makeAtomic $ Property $ local (\env -> env { quantification = q }) a
freshContext :: Testable m a => a -> Property m
freshContext = forAll
-- | Set the universal quantification context
forAll :: Testable m a => a -> Property m
forAll = quantify Forall . test
-- | Set the existential quantification context
exists :: Testable m a => a -> Property m
exists = quantify Exists . test
-- | Set the uniqueness quantification context.
--
-- Bear in mind that ∃! (x, y): p x y is not the same as ∃! x: ∃! y: p x y.
--
-- For example, ∃! x: ∃! y: |x| = |y| is true (it holds only when x=0), but ∃! (x,y): |x| = |y| is false (there are many such pairs).
--
-- As is customary in mathematics,
-- @'existsUnique' $ \\x y -> p x y@ is equivalent to
-- @'existsUnique' $ \\(x,y) -> p x y@ and not to
-- @'existsUnique' $ \\x -> 'existsUnique' $ \\y -> p x y@
-- (the latter, of course, may be explicitly written when desired).
--
-- That is, all the variables affected by the same uniqueness context are
-- quantified simultaneously as a tuple.
existsUnique :: Testable m a => a -> Property m
existsUnique = quantify ExistsUnique . test
-- | The '==>' operator can be used to express a restricting condition
-- under which a property should hold. It corresponds to implication in the
-- classical logic.
--
-- Note that '==>' resets the quantification context for its operands to
-- the default (universal).
infixr 0 ==>
(==>) :: (Testable m c, Testable m a) => c -> a -> Property m
cond ==> prop = Property $ do
env <- ask
let
counterExample = once $ searchCounterExamples $ unProp env' $ freshContext cond
-- NB: we do not invoke the test hook in the antecedent
where env' = env { testHook = const $ return () }
consequent = unProp env $ freshContext prop
badTestHook = lift $ testHook env BadTest
success =
ifte counterExample
-- then
(\ex -> do
badTestHook
return $ Vacuously ex
)
-- else
(searchExamples consequent)
failure =
ifte counterExample
-- then
(const $ do
lift $ testHook env BadTest
mzero
)
-- else
(searchCounterExamples consequent)
return $ atomicProperty success failure
-- | Run property with a modified depth. Affects all quantified variables
-- in the property.
changeDepth :: Testable m a => (Depth -> Depth) -> a -> Property m
changeDepth modifyDepth a = Property (changeDepthPS <$> unProperty (test a))
where
changeDepthPS (PropertySeries ss sf sc) =
PropertySeries
(localDepth modifyDepth ss)
(localDepth modifyDepth sf)
((\(prop, args) -> (changeDepth modifyDepth prop, args)) <$>
localDepth modifyDepth sc)
-- | Quantify the function's argument over its 'series', but adjust the
-- depth. This doesn't affect any subsequent variables.
changeDepth1 :: (Show a, Serial m a, Testable m b) => (Depth -> Depth) -> (a -> b) -> Property m
changeDepth1 modifyDepth = over $ localDepth modifyDepth series
-- }}}