{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
#define NEWTYPEABLE MIN_VERSION_base(4,7,0)
#if NEWTYPEABLE
{-# LANGUAGE Safe #-}
#else
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Trustworthy #-}
#endif
#endif
module Test.SmallCheck.Property (
forAll, exists, existsUnique, over, (==>), monadic, changeDepth, changeDepth1,
Property,
PropertySuccess(..), PropertyFailure(..), runProperty, TestQuality(..), Argument, Reason, Depth, Testable(..),
) where
import Test.SmallCheck.Series
import Test.SmallCheck.SeriesMonad
import Test.SmallCheck.Property.Result
import Control.Arrow (first)
import Control.Monad (liftM, mzero)
import Control.Monad.Logic (MonadLogic, runLogicT, ifte, once, msplit, lnot)
import Control.Monad.Reader (Reader, runReader, lift, ask, local, reader)
import Control.Applicative (pure, (<$>), (<$))
import Data.Typeable (Typeable(..))
#if !NEWTYPEABLE
import Data.Typeable (Typeable1, mkTyConApp, typeOf)
#if MIN_VERSION_base(4,4,0)
import Data.Typeable (mkTyCon3)
#else
import Data.Typeable (mkTyCon)
#endif
#endif
newtype Property m = Property { forall (m :: * -> *).
Property m -> Reader (Env m) (PropertySeries m)
unProperty :: Reader (Env m) (PropertySeries m) }
#if NEWTYPEABLE
deriving Typeable
#endif
data PropertySeries m =
PropertySeries
{ forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples :: Series m PropertySuccess
, forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples :: Series m PropertyFailure
, forall (m :: * -> *).
PropertySeries m -> Series m (Property m, [Argument])
searchClosest :: Series m (Property m, [Argument])
}
data Env m =
Env
{ forall (m :: * -> *). Env m -> Quantification
quantification :: Quantification
, forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook :: TestQuality -> m ()
}
data Quantification
= Forall
| Exists
| ExistsUnique
data TestQuality
= GoodTest
| BadTest
deriving (TestQuality -> TestQuality -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TestQuality -> TestQuality -> Bool
$c/= :: TestQuality -> TestQuality -> Bool
== :: TestQuality -> TestQuality -> Bool
$c== :: TestQuality -> TestQuality -> Bool
Eq, Eq TestQuality
TestQuality -> TestQuality -> Bool
TestQuality -> TestQuality -> Ordering
TestQuality -> TestQuality -> TestQuality
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TestQuality -> TestQuality -> TestQuality
$cmin :: TestQuality -> TestQuality -> TestQuality
max :: TestQuality -> TestQuality -> TestQuality
$cmax :: TestQuality -> TestQuality -> TestQuality
>= :: TestQuality -> TestQuality -> Bool
$c>= :: TestQuality -> TestQuality -> Bool
> :: TestQuality -> TestQuality -> Bool
$c> :: TestQuality -> TestQuality -> Bool
<= :: TestQuality -> TestQuality -> Bool
$c<= :: TestQuality -> TestQuality -> Bool
< :: TestQuality -> TestQuality -> Bool
$c< :: TestQuality -> TestQuality -> Bool
compare :: TestQuality -> TestQuality -> Ordering
$ccompare :: TestQuality -> TestQuality -> Ordering
Ord, Int -> TestQuality
TestQuality -> Int
TestQuality -> [TestQuality]
TestQuality -> TestQuality
TestQuality -> TestQuality -> [TestQuality]
TestQuality -> TestQuality -> TestQuality -> [TestQuality]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: TestQuality -> TestQuality -> TestQuality -> [TestQuality]
$cenumFromThenTo :: TestQuality -> TestQuality -> TestQuality -> [TestQuality]
enumFromTo :: TestQuality -> TestQuality -> [TestQuality]
$cenumFromTo :: TestQuality -> TestQuality -> [TestQuality]
enumFromThen :: TestQuality -> TestQuality -> [TestQuality]
$cenumFromThen :: TestQuality -> TestQuality -> [TestQuality]
enumFrom :: TestQuality -> [TestQuality]
$cenumFrom :: TestQuality -> [TestQuality]
fromEnum :: TestQuality -> Int
$cfromEnum :: TestQuality -> Int
toEnum :: Int -> TestQuality
$ctoEnum :: Int -> TestQuality
pred :: TestQuality -> TestQuality
$cpred :: TestQuality -> TestQuality
succ :: TestQuality -> TestQuality
$csucc :: TestQuality -> TestQuality
Enum, Int -> TestQuality -> ShowS
[TestQuality] -> ShowS
TestQuality -> Argument
forall a.
(Int -> a -> ShowS) -> (a -> Argument) -> ([a] -> ShowS) -> Show a
showList :: [TestQuality] -> ShowS
$cshowList :: [TestQuality] -> ShowS
show :: TestQuality -> Argument
$cshow :: TestQuality -> Argument
showsPrec :: Int -> TestQuality -> ShowS
$cshowsPrec :: Int -> TestQuality -> ShowS
Show)
#if !NEWTYPEABLE
instance Typeable1 m => Typeable (Property m)
where
typeOf _ =
mkTyConApp
#if MIN_VERSION_base(4,4,0)
(mkTyCon3 "smallcheck" "Test.SmallCheck.Property" "Property")
#else
(mkTyCon "smallcheck Test.SmallCheck.Property Property")
#endif
[typeOf (undefined :: m ())]
#endif
unProp :: Env t -> Property t -> PropertySeries t
unProp :: forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env t
q (Property Reader (Env t) (PropertySeries t)
p) = forall r a. Reader r a -> r -> a
runReader Reader (Env t) (PropertySeries t)
p Env t
q
runProperty
:: Monad m
=> Depth
-> (TestQuality -> m ())
-> Property m
-> m (Maybe PropertyFailure)
runProperty :: forall (m :: * -> *).
Monad m =>
Int
-> (TestQuality -> m ()) -> Property m -> m (Maybe PropertyFailure)
runProperty Int
depth TestQuality -> m ()
hook Property m
prop =
(\LogicT m PropertyFailure
l -> forall (m :: * -> *) a r.
LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT LogicT m PropertyFailure
l (\PropertyFailure
x m (Maybe PropertyFailure)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just PropertyFailure
x) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a. Int -> Series m a -> LogicT m a
runSeries Int
depth forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples forall a b. (a -> b) -> a -> b
$
forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r a. Reader r a -> r -> a
runReader (forall (m :: * -> *).
Quantification -> (TestQuality -> m ()) -> Env m
Env Quantification
Forall TestQuality -> m ()
hook) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
Property m -> Reader (Env m) (PropertySeries m)
unProperty Property m
prop
atomicProperty :: Series m PropertySuccess -> Series m PropertyFailure -> PropertySeries m
atomicProperty :: forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
s Series m PropertyFailure
f =
let prop :: PropertySeries m
prop = forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
s Series m PropertyFailure
f (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure PropertySeries m
prop, []))
in PropertySeries m
prop
makeAtomic :: Property m -> Property m
makeAtomic :: forall (m :: * -> *). Property m -> Property m
makeAtomic (Property Reader (Env m) (PropertySeries m)
prop) =
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reader (Env m) (PropertySeries m)
prop forall a b. (a -> b) -> a -> b
$ \PropertySeries m
ps ->
forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty (forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples PropertySeries m
ps) (forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples PropertySeries m
ps)
over
:: (Show a, Testable m b)
=> Series m a -> (a -> b) -> Property m
over :: forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
over = forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
testFunction
monadic :: Testable m a => m a -> Property m
monadic :: forall (m :: * -> *) a. Testable m a => m a -> Property m
monadic m a
a =
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Env m
env ->
let pair :: Series m (PropertySeries m)
pair = forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Testable m a => a -> Property m
freshContext forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
a in
forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty
(forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Series m (PropertySeries m)
pair)
(forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Series m (PropertySeries m)
pair)
class Monad m => Testable m a where
test :: a -> Property m
instance Monad m => Testable m Bool where
test :: Bool -> Property m
test Bool
b = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Env m
env ->
let
success :: Series m PropertySuccess
success = do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe Argument -> PropertySuccess
PropertyTrue forall a. Maybe a
Nothing else forall (m :: * -> *) a. MonadPlus m => m a
mzero
failure :: Series m PropertyFailure
failure = Maybe Argument -> PropertyFailure
PropertyFalse forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertySuccess
success
in forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
success Series m PropertyFailure
failure
instance Monad m => Testable m (Either Reason Reason) where
test :: Either Argument Argument -> Property m
test Either Argument Argument
r = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Env m
env ->
let
success :: Series m PropertySuccess
success = do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadPlus m => m a
mzero) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Argument -> PropertySuccess
PropertyTrue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) Either Argument Argument
r
failure :: Series m PropertyFailure
failure = do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Argument -> PropertyFailure
PropertyFalse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) (forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadPlus m => m a
mzero) Either Argument Argument
r
in forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
success Series m PropertyFailure
failure
instance (Serial m a, Show a, Testable m b) => Testable m (a->b) where
test :: (a -> b) -> Property m
test = forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
testFunction forall (m :: * -> *) a. Serial m a => Series m a
series
instance (Monad m, m ~ n) => Testable n (Property m) where
test :: Property m -> Property n
test = forall a. a -> a
id
testFunction
:: (Show a, Testable m b)
=> Series m a -> (a -> b) -> Property m
testFunction :: forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
testFunction Series m a
s a -> b
f = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Env m
env ->
let
closest :: Series m (Property m, [Argument])
closest = do
a
x <- Series m a
s
(Property m
p, [Argument]
args) <- forall (m :: * -> *).
PropertySeries m -> Series m (Property m, [Argument])
searchClosest forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
test forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
forall (m :: * -> *) a. Monad m => a -> m a
return (Property m
p, forall a. Show a => a -> Argument
show a
x forall a. a -> [a] -> [a]
: [Argument]
args)
in
case forall (m :: * -> *). Env m -> Quantification
quantification Env m
env of
Quantification
Forall -> forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
success Series m PropertyFailure
failure Series m (Property m, [Argument])
closest
where
failure :: Series m PropertyFailure
failure = do
a
x <- Series m a
s
PropertyFailure
failure <- forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
test forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
let arg :: Argument
arg = forall a. Show a => a -> Argument
show a
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
case PropertyFailure
failure of
CounterExample [Argument]
args PropertyFailure
etc -> [Argument] -> PropertyFailure -> PropertyFailure
CounterExample (Argument
argforall a. a -> [a] -> [a]
:[Argument]
args) PropertyFailure
etc
PropertyFailure
_ -> [Argument] -> PropertyFailure -> PropertyFailure
CounterExample [Argument
arg] PropertyFailure
failure
success :: Series m PropertySuccess
success = Maybe Argument -> PropertySuccess
PropertyTrue forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertyFailure
failure
Quantification
Exists -> forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
success Series m PropertyFailure
failure Series m (Property m, [Argument])
closest
where
success :: Series m PropertySuccess
success = do
a
x <- Series m a
s
PropertySuccess
s <- forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
test forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
let arg :: Argument
arg = forall a. Show a => a -> Argument
show a
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
case PropertySuccess
s of
Exist [Argument]
args PropertySuccess
etc -> [Argument] -> PropertySuccess -> PropertySuccess
Exist (Argument
argforall a. a -> [a] -> [a]
:[Argument]
args) PropertySuccess
etc
PropertySuccess
_ -> [Argument] -> PropertySuccess -> PropertySuccess
Exist [Argument
arg] PropertySuccess
s
failure :: Series m PropertyFailure
failure = PropertyFailure
NotExist forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertySuccess
success
Quantification
ExistsUnique -> forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
success Series m PropertyFailure
failure Series m (Property m, [Argument])
closest
where
search :: Series m [([Argument], PropertySuccess)]
search = forall (m :: * -> *) a. MonadLogic m => Int -> m a -> m [a]
atMost Int
2 forall a b. (a -> b) -> a -> b
$ do
(Property m
prop, [Argument]
args) <- Series m (Property m, [Argument])
closest
PropertySuccess
ex <- forall (m :: * -> *) a. MonadLogic m => m a -> m a
once forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
test Property m
prop
forall (m :: * -> *) a. Monad m => a -> m a
return ([Argument]
args, PropertySuccess
ex)
success :: Series m PropertySuccess
success =
Series m [([Argument], PropertySuccess)]
search forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\[([Argument], PropertySuccess)]
examples ->
case [([Argument], PropertySuccess)]
examples of
[([Argument]
x,PropertySuccess
s)] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Argument] -> PropertySuccess -> PropertySuccess
ExistUnique [Argument]
x PropertySuccess
s
[([Argument], PropertySuccess)]
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
failure :: Series m PropertyFailure
failure =
Series m [([Argument], PropertySuccess)]
search forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\[([Argument], PropertySuccess)]
examples ->
case [([Argument], PropertySuccess)]
examples of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return PropertyFailure
NotExist
([Argument]
x1,PropertySuccess
s1):([Argument]
x2,PropertySuccess
s2):[([Argument], PropertySuccess)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Argument]
-> PropertySuccess
-> [Argument]
-> PropertySuccess
-> PropertyFailure
AtLeastTwo [Argument]
x1 PropertySuccess
s1 [Argument]
x2 PropertySuccess
s2
[([Argument], PropertySuccess)]
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
atMost :: MonadLogic m => Int -> m a -> m [a]
atMost :: forall (m :: * -> *) a. MonadLogic m => Int -> m a -> m [a]
atMost Int
n m a
m
| Int
n forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
Maybe (a, m a)
m' <- forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit m a
m
case Maybe (a, m a)
m' of
Maybe (a, m a)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return []
Just (a
x,m a
rest) ->
(a
xforall a. a -> [a] -> [a]
:) forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` forall (m :: * -> *) a. MonadLogic m => Int -> m a -> m [a]
atMost (Int
nforall a. Num a => a -> a -> a
-Int
1) m a
rest
quantify :: Quantification -> Property m -> Property m
quantify :: forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
q (Property Reader (Env m) (PropertySeries m)
a) =
forall (m :: * -> *). Property m -> Property m
makeAtomic forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env m
env -> Env m
env { quantification :: Quantification
quantification = Quantification
q }) Reader (Env m) (PropertySeries m)
a
freshContext :: Testable m a => a -> Property m
freshContext :: forall (m :: * -> *) a. Testable m a => a -> Property m
freshContext = forall (m :: * -> *) a. Testable m a => a -> Property m
forAll
forAll :: Testable m a => a -> Property m
forAll :: forall (m :: * -> *) a. Testable m a => a -> Property m
forAll = forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
Forall forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Testable m a => a -> Property m
test
exists :: Testable m a => a -> Property m
exists :: forall (m :: * -> *) a. Testable m a => a -> Property m
exists = forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
Exists forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Testable m a => a -> Property m
test
existsUnique :: Testable m a => a -> Property m
existsUnique :: forall (m :: * -> *) a. Testable m a => a -> Property m
existsUnique = forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
ExistsUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Testable m a => a -> Property m
test
infixr 0 ==>
(==>) :: (Testable m c, Testable m a) => c -> a -> Property m
c
cond ==> :: forall (m :: * -> *) c a.
(Testable m c, Testable m a) =>
c -> a -> Property m
==> a
prop = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ do
Env m
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
let
counterExample :: Series m PropertyFailure
counterExample = forall (m :: * -> *) a. MonadLogic m => m a -> m a
once forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
freshContext c
cond
where env' :: Env m
env' = Env m
env { testHook :: TestQuality -> m ()
testHook = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return () }
consequent :: PropertySeries m
consequent = forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
freshContext a
prop
badTestHook :: Series m ()
badTestHook = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
BadTest
success :: Series m PropertySuccess
success =
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte Series m PropertyFailure
counterExample
(\PropertyFailure
ex -> do
Series m ()
badTestHook
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PropertyFailure -> PropertySuccess
Vacuously PropertyFailure
ex
)
(forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples PropertySeries m
consequent)
failure :: Series m PropertyFailure
failure =
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte Series m PropertyFailure
counterExample
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
BadTest
forall (m :: * -> *) a. MonadPlus m => m a
mzero
)
(forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples PropertySeries m
consequent)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
success Series m PropertyFailure
failure
changeDepth :: Testable m a => (Depth -> Depth) -> a -> Property m
changeDepth :: forall (m :: * -> *) a.
Testable m a =>
(Int -> Int) -> a -> Property m
changeDepth Int -> Int
modifyDepth a
a = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (PropertySeries m -> PropertySeries m
changeDepthPS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
Property m -> Reader (Env m) (PropertySeries m)
unProperty (forall (m :: * -> *) a. Testable m a => a -> Property m
test a
a))
where
changeDepthPS :: PropertySeries m -> PropertySeries m
changeDepthPS (PropertySeries Series m PropertySuccess
ss Series m PropertyFailure
sf Series m (Property m, [Argument])
sc) =
forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries
(forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m PropertySuccess
ss)
(forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m PropertyFailure
sf)
(forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (m :: * -> *) a.
Testable m a =>
(Int -> Int) -> a -> Property m
changeDepth Int -> Int
modifyDepth) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m (Property m, [Argument])
sc)
changeDepth1 :: (Show a, Serial m a, Testable m b) => (Depth -> Depth) -> (a -> b) -> Property m
changeDepth1 :: forall a (m :: * -> *) b.
(Show a, Serial m a, Testable m b) =>
(Int -> Int) -> (a -> b) -> Property m
changeDepth1 Int -> Int
modifyDepth = forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
over forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth forall (m :: * -> *) a. Serial m a => Series m a
series