-- 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 CPP #-}{-# LANGUAGE DeriveDataTypeable #-}{-# LANGUAGE FlexibleInstances #-}{-# LANGUAGE MultiParamTypeClasses #-}{-# LANGUAGE NoImplicitPrelude #-}{-# LANGUAGE ScopedTypeVariables #-}{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE TypeOperators #-}-- 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
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Trustworthy #-}
#endif
#endif
moduleTest.SmallCheck.Property(-- * ConstructorsforAll ,exists ,existsUnique ,over ,(==>) ,monadic ,changeDepth ,changeDepth1 ,-- * Property's entrailsProperty ,PropertySuccess (..),PropertyFailure (..),runProperty ,TestQuality (..),Argument ,Reason ,Depth ,Testable (..),)whereimportControl.Applicative(pure,(<$>),(<$))importControl.Arrow(first)importControl.Monad(Monad,liftM,mzero,return,(=<<),(>>=))importControl.Monad.Logic(MonadLogic,runLogicT,ifte,once,msplit,lnot)importControl.Monad.Reader(Reader,runReader,lift,ask,local,reader)importData.Bool(Bool,otherwise)importData.Either(Either,either)importData.Eq(Eq)importData.Function(($),flip,(.),const,id)importData.Functor(fmap)importData.Int(Int)importData.Maybe(Maybe(Nothing,Just))importData.Ord(Ord,(<=))importData.Typeable(Typeable)importPrelude(Enum,(-))importTest.SmallCheck.Property.Result importTest.SmallCheck.Series importTest.SmallCheck.SeriesMonad importText.Show(Show,show)
#if MIN_VERSION_base(4,17,0)
importData.Type.Equality(type(~))
#endif

#if !NEWTYPEABLE
importData.Typeable(Typeable1,mkTyConApp,typeOf)importPrelude(undefined)
#if MIN_VERSION_base(4,4,0)
importData.Typeable(mkTyCon3)
#else
importData.Typeable(mkTyCon)
#endif
#endif
-------------------------------- Property-related types--------------------------------{{{-- | The type of properties over the monad @m@.---- @since 1.0newtypeProperty m =Property {forall (m :: * -> *).
Property m -> Reader (Env m) (PropertySeries m)
unProperty ::Reader(Env m )(PropertySeries m )}
#if NEWTYPEABLE
derivingTypeable
#endif
dataPropertySeries 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 ])}dataEnv m =Env {forall (m :: * -> *). Env m -> Quantification
quantification ::Quantification ,forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook ::TestQuality ->m ()}dataQuantification =Forall |Exists |ExistsUnique -- | @since 1.0dataTestQuality =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
-- Typeable here is not polykinded yet, and also GHC doesn't know how to-- derive this.instanceTypeable1m=>Typeable(Propertym)wheretypeOf_=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
-- }}}-------------------------------------- Property runners and constructors--------------------------------------{{{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
runReaderReader (Env t) (PropertySeries t)
p Env t
q runProperty ::Monadm =>Depth ->(TestQuality ->m ())->Property m ->m (MaybePropertyFailure )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
runLogicTLogicT m PropertyFailure
l (\PropertyFailure
x m (Maybe PropertyFailure)
_->forall (m :: * -> *) a. Monad m => a -> m a
returnforall a b. (a -> b) -> a -> b
$forall a. a -> Maybe a
JustPropertyFailure
x )(forall (m :: * -> *) a. Monad m => a -> m a
returnforall 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
flipforall 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 =letprop :: 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
purePropertySeries m
prop ,[]))inPropertySeries 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
flipforall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmapReader (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' 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.---- @since 1.0over ::(Showa ,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 -- | Execute a monadic test.---- @since 1.0monadic ::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
readerforall a b. (a -> b) -> a -> b
$\Env m
env ->letpair :: 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
liftm a
a inforall (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 )-- }}}--------------------------------- 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 'Data.Functor.Identity'.---- @since 1.0classMonadm =>Testable m a where-- | @since 1.0test ::a ->Property m instanceMonadm =>Testable m Boolwheretest :: 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
readerforall a b. (a -> b) -> a -> b
$\Env m
env ->letsuccess :: Series m PropertySuccess
success =doforall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
liftforall a b. (a -> b) -> a -> b
$forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest ifBool
b thenforall (m :: * -> *) a. Monad m => a -> m a
returnforall a b. (a -> b) -> a -> b
$Maybe Argument -> PropertySuccess
PropertyTrue forall a. Maybe a
Nothingelseforall (m :: * -> *) a. MonadPlus m => m a
mzerofailure :: Series m PropertyFailure
failure =Maybe Argument -> PropertyFailure
PropertyFalse forall a. Maybe a
Nothingforall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnotSeries m PropertySuccess
success inforall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
success Series m PropertyFailure
failure -- | Works like the 'Data.Bool.Bool' instance, but includes an explanation of the result.---- 'Data.Either.Left' and 'Data.Either.Right' correspond to test failure and success-- respectively.---- @since 1.1instanceMonadm =>Testable m (EitherReason Reason )wheretest :: 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
readerforall a b. (a -> b) -> a -> b
$\Env m
env ->letsuccess :: Series m PropertySuccess
success =doforall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
liftforall 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
constforall (m :: * -> *) a. MonadPlus m => m a
mzero)(forall (f :: * -> *) a. Applicative f => a -> f a
pureforall 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 =doforall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
liftforall 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
pureforall 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
constforall (m :: * -> *) a. MonadPlus m => m a
mzero)Either Argument Argument
r inforall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
success Series m PropertyFailure
failure instance(Serial m a ,Showa ,Testable m b )=>Testable m (a ->b )wheretest :: (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(Monadm ,m ~n )=>Testable n (Property m )wheretest :: Property m -> Property n
test =forall a. a -> a
idtestFunction ::(Showa ,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
readerforall a b. (a -> b) -> a -> b
$\Env m
env ->letclosest :: Series m (Property m, [Argument])
closest =doa
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
showa
x forall a. a -> [a] -> [a]
:[Argument]
args )incaseforall (m :: * -> *). Env m -> Quantification
quantification Env m
env ofQuantification
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 -- {{{wherefailure :: Series m PropertyFailure
failure =doa
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 letarg :: Argument
arg =forall a. Show a => a -> Argument
showa
x forall (m :: * -> *) a. Monad m => a -> m a
returnforall a b. (a -> b) -> a -> b
$casePropertyFailure
failure ofCounterExample [Argument]
args PropertyFailure
etc ->[Argument] -> PropertyFailure -> PropertyFailure
CounterExample (Argument
arg forall 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
Nothingforall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnotSeries 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 -- {{{wheresuccess :: Series m PropertySuccess
success =doa
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 letarg :: Argument
arg =forall a. Show a => a -> Argument
showa
x forall (m :: * -> *) a. Monad m => a -> m a
returnforall a b. (a -> b) -> a -> b
$casePropertySuccess
s ofExist [Argument]
args PropertySuccess
etc ->[Argument] -> PropertySuccess -> PropertySuccess
Exist (Argument
arg forall 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 ()
lnotSeries 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 -- {{{wheresearch :: Series m [([Argument], PropertySuccess)]
search =forall (m :: * -> *) a. MonadLogic m => Int -> m a -> m [a]
atMost Int
2forall 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
onceforall 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
returnforall a b. (a -> b) -> a -> b
$[Argument] -> PropertySuccess -> PropertySuccess
ExistUnique [Argument]
x PropertySuccess
s [([Argument], PropertySuccess)]
_->forall (m :: * -> *) a. MonadPlus m => m a
mzerofailure :: 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
returnPropertyFailure
NotExist ([Argument]
x1 ,PropertySuccess
s1 ):([Argument]
x2 ,PropertySuccess
s2 ):[([Argument], PropertySuccess)]
_->forall (m :: * -> *) a. Monad m => a -> m a
returnforall 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 ::MonadLogicm =>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=doMaybe (a, m a)
m' <-forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplitm a
m caseMaybe (a, m a)
m' ofMaybe (a, m a)
Nothing->forall (m :: * -> *) a. Monad m => a -> m a
return[]Just(a
x ,m a
rest )->(a
x forall 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
n forall a. Num a => a -> a -> a
-Int
1)m a
rest -- }}}-------------------------------- Test constructors-------------------------------- {{{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 -- | Set the universal quantification context.---- @since 1.0forAll ::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 -- | Set the existential quantification context.---- @since 1.0exists ::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 -- | Set the uniqueness quantification context.---- Bear in mind that \( \exists! x, y\colon p,円 x ,円 y \)-- is not the same as \( \exists! x \colon \exists! y \colon p ,円 x ,円 y \).---- For example, \( \exists! x \colon \exists! y \colon |x| = |y| \)-- is true (it holds only when \(x=y=0\)),-- but \( \exists! x, y \colon |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.---- @since 1.0existsUnique ::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 -- | 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).---- @since 1.0infixr0==> (==>) ::(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
$doEnv m
env <-forall r (m :: * -> *). MonadReader r m => m r
askletcounterExample :: Series m PropertyFailure
counterExample =forall (m :: * -> *) a. MonadLogic m => m a -> m a
onceforall 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 -- NB: we do not invoke the test hook in the antecedentwhereenv' :: Env m
env' =Env m
env {testHook :: TestQuality -> m ()
testHook =forall a b. a -> b -> a
constforall 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
liftforall 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
ifteSeries m PropertyFailure
counterExample -- then(\PropertyFailure
ex ->doSeries m ()
badTestHook forall (m :: * -> *) a. Monad m => a -> m a
returnforall a b. (a -> b) -> a -> b
$PropertyFailure -> PropertySuccess
Vacuously PropertyFailure
ex )-- else(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
ifteSeries m PropertyFailure
counterExample -- then(forall a b. a -> b -> a
constforall a b. (a -> b) -> a -> b
$doforall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
liftforall 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)-- else(forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples PropertySeries m
consequent )forall (m :: * -> *) a. Monad m => a -> m a
returnforall 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 -- | Run property with a modified depth. Affects all quantified variables-- in the property.---- @since 1.0changeDepth ::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 ))wherechangeDepthPS :: 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 )-- | Quantify the function's argument over its 'series', but adjust the-- depth. This doesn't affect any subsequent variables.---- @since 1.0changeDepth1 ::(Showa ,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 -- }}}