-- 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

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 Control.Applicative (pure, (<$>), (<$))
import Control.Arrow (first)
import Control.Monad (Monad, liftM, mzero, return, (=<<), (>>=))
import Control.Monad.Logic (MonadLogic, runLogicT, ifte, once, msplit, lnot)
import Control.Monad.Reader (Reader, runReader, lift, ask, local, reader)
import Data.Bool (Bool, otherwise)
import Data.Either (Either, either)
import Data.Eq (Eq)
import Data.Function (($), flip, (.), const, id)
import Data.Functor (fmap)
import Data.Int (Int)
import Data.Maybe (Maybe (Nothing, Just))
import Data.Ord (Ord, (<=))
import Data.Typeable (Typeable)
import Prelude (Enum, (-))
import Test.SmallCheck.Property.Result
import Test.SmallCheck.Series
import Test.SmallCheck.SeriesMonad
import Text.Show (Show, show)

#if MIN_VERSION_base(4,17,0)
import Data.Type.Equality (type (~))
#endif

#if !NEWTYPEABLE
import Data.Typeable (Typeable1, mkTyConApp, typeOf)
import Prelude (undefined)
#if MIN_VERSION_base(4,4,0)
import Data.Typeable (mkTyCon3)
#else
import Data.Typeable (mkTyCon)
#endif
#endif

------------------------------
-- Property-related types
------------------------------
--{{{

-- | The type of properties over the monad @m@.
--
-- @since 1.0
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

-- | @since 1.0
data TestQuality
  = GoodTest
  | BadTest
  deriving (TestQuality -> TestQuality -> Bool
(TestQuality -> TestQuality -> Bool)
-> (TestQuality -> TestQuality -> Bool) -> Eq TestQuality
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TestQuality -> TestQuality -> Bool
== :: TestQuality -> TestQuality -> Bool
$c/= :: TestQuality -> TestQuality -> Bool
/= :: TestQuality -> TestQuality -> Bool
Eq, Eq TestQuality
Eq TestQuality =>
(TestQuality -> TestQuality -> Ordering)
-> (TestQuality -> TestQuality -> Bool)
-> (TestQuality -> TestQuality -> Bool)
-> (TestQuality -> TestQuality -> Bool)
-> (TestQuality -> TestQuality -> Bool)
-> (TestQuality -> TestQuality -> TestQuality)
-> (TestQuality -> TestQuality -> TestQuality)
-> Ord 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
$ccompare :: TestQuality -> TestQuality -> Ordering
compare :: TestQuality -> TestQuality -> Ordering
$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
>= :: TestQuality -> TestQuality -> Bool
$cmax :: TestQuality -> TestQuality -> TestQuality
max :: TestQuality -> TestQuality -> TestQuality
$cmin :: TestQuality -> TestQuality -> TestQuality
min :: TestQuality -> TestQuality -> TestQuality
Ord, Int -> TestQuality
TestQuality -> Int
TestQuality -> [TestQuality]
TestQuality -> TestQuality
TestQuality -> TestQuality -> [TestQuality]
TestQuality -> TestQuality -> TestQuality -> [TestQuality]
(TestQuality -> TestQuality)
-> (TestQuality -> TestQuality)
-> (Int -> TestQuality)
-> (TestQuality -> Int)
-> (TestQuality -> [TestQuality])
-> (TestQuality -> TestQuality -> [TestQuality])
-> (TestQuality -> TestQuality -> [TestQuality])
-> (TestQuality -> TestQuality -> TestQuality -> [TestQuality])
-> Enum 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
$csucc :: TestQuality -> TestQuality
succ :: TestQuality -> TestQuality
$cpred :: TestQuality -> TestQuality
pred :: TestQuality -> TestQuality
$ctoEnum :: Int -> TestQuality
toEnum :: Int -> TestQuality
$cfromEnum :: TestQuality -> Int
fromEnum :: TestQuality -> Int
$cenumFrom :: TestQuality -> [TestQuality]
enumFrom :: TestQuality -> [TestQuality]
$cenumFromThen :: TestQuality -> TestQuality -> [TestQuality]
enumFromThen :: TestQuality -> TestQuality -> [TestQuality]
$cenumFromTo :: TestQuality -> TestQuality -> [TestQuality]
enumFromTo :: TestQuality -> TestQuality -> [TestQuality]
$cenumFromThenTo :: TestQuality -> TestQuality -> TestQuality -> [TestQuality]
enumFromThenTo :: TestQuality -> TestQuality -> TestQuality -> [TestQuality]
Enum, Int -> TestQuality -> ShowS
[TestQuality] -> ShowS
TestQuality -> Argument
(Int -> TestQuality -> ShowS)
-> (TestQuality -> Argument)
-> ([TestQuality] -> ShowS)
-> Show TestQuality
forall a.
(Int -> a -> ShowS) -> (a -> Argument) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TestQuality -> ShowS
showsPrec :: Int -> TestQuality -> ShowS
$cshow :: TestQuality -> Argument
show :: TestQuality -> Argument
$cshowList :: [TestQuality] -> ShowS
showList :: [TestQuality] -> ShowS
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
#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) = Reader (Env t) (PropertySeries t) -> Env t -> PropertySeries t
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 -> LogicT m PropertyFailure
-> (PropertyFailure
    -> m (Maybe PropertyFailure) -> m (Maybe PropertyFailure))
-> m (Maybe PropertyFailure)
-> m (Maybe PropertyFailure)
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)
_ -> Maybe PropertyFailure -> m (Maybe PropertyFailure)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe PropertyFailure -> m (Maybe PropertyFailure))
-> Maybe PropertyFailure -> m (Maybe PropertyFailure)
forall a b. (a -> b) -> a -> b
$ PropertyFailure -> Maybe PropertyFailure
forall a. a -> Maybe a
Just PropertyFailure
x) (Maybe PropertyFailure -> m (Maybe PropertyFailure)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe PropertyFailure
forall a. Maybe a
Nothing)) (LogicT m PropertyFailure -> m (Maybe PropertyFailure))
-> LogicT m PropertyFailure -> m (Maybe PropertyFailure)
forall a b. (a -> b) -> a -> b
$
  Int -> Series m PropertyFailure -> LogicT m PropertyFailure
forall (m :: * -> *) a. Int -> Series m a -> LogicT m a
runSeries Int
depth (Series m PropertyFailure -> LogicT m PropertyFailure)
-> Series m PropertyFailure -> LogicT m PropertyFailure
forall a b. (a -> b) -> a -> b
$
  PropertySeries m -> Series m PropertyFailure
forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples (PropertySeries m -> Series m PropertyFailure)
-> PropertySeries m -> Series m PropertyFailure
forall a b. (a -> b) -> a -> b
$
  (Reader (Env m) (PropertySeries m) -> Env m -> PropertySeries m)
-> Env m -> Reader (Env m) (PropertySeries m) -> PropertySeries m
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reader (Env m) (PropertySeries m) -> Env m -> PropertySeries m
forall r a. Reader r a -> r -> a
runReader (Quantification -> (TestQuality -> m ()) -> Env m
forall (m :: * -> *).
Quantification -> (TestQuality -> m ()) -> Env m
Env Quantification
Forall TestQuality -> m ()
hook) (Reader (Env m) (PropertySeries m) -> PropertySeries m)
-> Reader (Env m) (PropertySeries m) -> PropertySeries m
forall a b. (a -> b) -> a -> b
$
  Property m -> Reader (Env m) (PropertySeries m)
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 = Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
s Series m PropertyFailure
f ((Property m, [Argument]) -> Series m (Property m, [Argument])
forall a. a -> Series m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ PropertySeries m -> Reader (Env m) (PropertySeries m)
forall a. a -> ReaderT (Env m) Identity a
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) =
  Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ ((PropertySeries m -> PropertySeries m)
 -> Reader (Env m) (PropertySeries m)
 -> Reader (Env m) (PropertySeries m))
-> Reader (Env m) (PropertySeries m)
-> (PropertySeries m -> PropertySeries m)
-> Reader (Env m) (PropertySeries m)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (PropertySeries m -> PropertySeries m)
-> Reader (Env m) (PropertySeries m)
-> Reader (Env m) (PropertySeries m)
forall a b.
(a -> b)
-> ReaderT (Env m) Identity a -> ReaderT (Env m) Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reader (Env m) (PropertySeries m)
prop ((PropertySeries m -> PropertySeries m)
 -> Reader (Env m) (PropertySeries m))
-> (PropertySeries m -> PropertySeries m)
-> Reader (Env m) (PropertySeries m)
forall a b. (a -> b) -> a -> b
$ \PropertySeries m
ps ->
    Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty (PropertySeries m -> Series m PropertySuccess
forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples PropertySeries m
ps) (PropertySeries m -> Series m PropertyFailure
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.0
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 = Series m a -> (a -> b) -> Property m
forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
testFunction

-- | Execute a monadic test.
--
-- @since 1.0
monadic :: Testable m a => m a -> Property m
monadic :: forall (m :: * -> *) a. Testable m a => m a -> Property m
monadic m a
a =
  Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
forall a. (Env m -> a) -> ReaderT (Env m) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m))
-> (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
forall a b. (a -> b) -> a -> b
$ \Env m
env ->

    let pair :: Series m (PropertySeries m)
pair = Env m -> Property m -> PropertySeries m
forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env (Property m -> PropertySeries m)
-> (a -> Property m) -> a -> PropertySeries m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
freshContext (a -> PropertySeries m)
-> Series m a -> Series m (PropertySeries m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> Series m a
forall (m :: * -> *) a. Monad m => m a -> Series m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
a in

    Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty
      (PropertySeries m -> Series m PropertySuccess
forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples (PropertySeries m -> Series m PropertySuccess)
-> Series m (PropertySeries m) -> Series m PropertySuccess
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Series m (PropertySeries m)
pair)
      (PropertySeries m -> Series m PropertyFailure
forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples (PropertySeries m -> Series m PropertyFailure)
-> Series m (PropertySeries m) -> Series m PropertyFailure
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.0
class Monad m => Testable m a where
  -- | @since 1.0
  test :: a -> Property m

instance Monad m => Testable m Bool where
  test :: Bool -> Property m
test Bool
b = Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
forall a. (Env m -> a) -> ReaderT (Env m) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m))
-> (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
forall a b. (a -> b) -> a -> b
$ \Env m
env ->
    let
      success :: Series m PropertySuccess
success = do
        m () -> Series m ()
forall (m :: * -> *) a. Monad m => m a -> Series m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> Series m ()) -> m () -> Series m ()
forall a b. (a -> b) -> a -> b
$ Env m -> TestQuality -> m ()
forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
        if Bool
b then PropertySuccess -> Series m PropertySuccess
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropertySuccess -> Series m PropertySuccess)
-> PropertySuccess -> Series m PropertySuccess
forall a b. (a -> b) -> a -> b
$ Maybe Argument -> PropertySuccess
PropertyTrue Maybe Argument
forall a. Maybe a
Nothing else Series m PropertySuccess
forall a. Series m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      failure :: Series m PropertyFailure
failure = Maybe Argument -> PropertyFailure
PropertyFalse Maybe Argument
forall a. Maybe a
Nothing PropertyFailure -> Series m () -> Series m PropertyFailure
forall a b. a -> Series m b -> Series m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Series m PropertySuccess -> Series m ()
forall a. Series m a -> Series m ()
forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertySuccess
success
    in Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
forall (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.1
instance Monad m => Testable m (Either Reason Reason) where
  test :: Either Argument Argument -> Property m
test Either Argument Argument
r = Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
forall a. (Env m -> a) -> ReaderT (Env m) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m))
-> (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
forall a b. (a -> b) -> a -> b
$ \Env m
env ->
    let
      success :: Series m PropertySuccess
success = do
        m () -> Series m ()
forall (m :: * -> *) a. Monad m => m a -> Series m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> Series m ()) -> m () -> Series m ()
forall a b. (a -> b) -> a -> b
$ Env m -> TestQuality -> m ()
forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
        (Argument -> Series m PropertySuccess)
-> (Argument -> Series m PropertySuccess)
-> Either Argument Argument
-> Series m PropertySuccess
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Series m PropertySuccess -> Argument -> Series m PropertySuccess
forall a b. a -> b -> a
const Series m PropertySuccess
forall a. Series m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero) (PropertySuccess -> Series m PropertySuccess
forall a. a -> Series m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PropertySuccess -> Series m PropertySuccess)
-> (Argument -> PropertySuccess)
-> Argument
-> Series m PropertySuccess
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Argument -> PropertySuccess
PropertyTrue (Maybe Argument -> PropertySuccess)
-> (Argument -> Maybe Argument) -> Argument -> PropertySuccess
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Argument -> Maybe Argument
forall a. a -> Maybe a
Just) Either Argument Argument
r
      failure :: Series m PropertyFailure
failure = do
        m () -> Series m ()
forall (m :: * -> *) a. Monad m => m a -> Series m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> Series m ()) -> m () -> Series m ()
forall a b. (a -> b) -> a -> b
$ Env m -> TestQuality -> m ()
forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
        (Argument -> Series m PropertyFailure)
-> (Argument -> Series m PropertyFailure)
-> Either Argument Argument
-> Series m PropertyFailure
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PropertyFailure -> Series m PropertyFailure
forall a. a -> Series m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PropertyFailure -> Series m PropertyFailure)
-> (Argument -> PropertyFailure)
-> Argument
-> Series m PropertyFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Argument -> PropertyFailure
PropertyFalse (Maybe Argument -> PropertyFailure)
-> (Argument -> Maybe Argument) -> Argument -> PropertyFailure
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Argument -> Maybe Argument
forall a. a -> Maybe a
Just) (Series m PropertyFailure -> Argument -> Series m PropertyFailure
forall a b. a -> b -> a
const Series m PropertyFailure
forall a. Series m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero) Either Argument Argument
r
    in Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
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 = Series m a -> (a -> b) -> Property m
forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
testFunction Series m a
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 = Property m -> Property m
Property m -> Property n
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 = Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
forall a. (Env m -> a) -> ReaderT (Env m) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader ((Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m))
-> (Env m -> PropertySeries m) -> Reader (Env m) (PropertySeries m)
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) <- PropertySeries m -> Series m (Property m, [Argument])
forall (m :: * -> *).
PropertySeries m -> Series m (Property m, [Argument])
searchClosest (PropertySeries m -> Series m (Property m, [Argument]))
-> PropertySeries m -> Series m (Property m, [Argument])
forall a b. (a -> b) -> a -> b
$ Env m -> Property m -> PropertySeries m
forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env (Property m -> PropertySeries m) -> Property m -> PropertySeries m
forall a b. (a -> b) -> a -> b
$ b -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
test (b -> Property m) -> b -> Property m
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
      (Property m, [Argument]) -> Series m (Property m, [Argument])
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property m
p, a -> Argument
forall a. Show a => a -> Argument
show a
x Argument -> [Argument] -> [Argument]
forall a. a -> [a] -> [a]
: [Argument]
args)
  in

  case Env m -> Quantification
forall (m :: * -> *). Env m -> Quantification
quantification Env m
env of
    Quantification
Forall -> Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
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 <- PropertySeries m -> Series m PropertyFailure
forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples (PropertySeries m -> Series m PropertyFailure)
-> PropertySeries m -> Series m PropertyFailure
forall a b. (a -> b) -> a -> b
$ Env m -> Property m -> PropertySeries m
forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env (Property m -> PropertySeries m) -> Property m -> PropertySeries m
forall a b. (a -> b) -> a -> b
$ b -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
test (b -> Property m) -> b -> Property m
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
          let arg :: Argument
arg = a -> Argument
forall a. Show a => a -> Argument
show a
x
          PropertyFailure -> Series m PropertyFailure
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropertyFailure -> Series m PropertyFailure)
-> PropertyFailure -> Series m PropertyFailure
forall a b. (a -> b) -> a -> b
$
            case PropertyFailure
failure of
              CounterExample [Argument]
args PropertyFailure
etc -> [Argument] -> PropertyFailure -> PropertyFailure
CounterExample (Argument
argArgument -> [Argument] -> [Argument]
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 Maybe Argument
forall a. Maybe a
Nothing PropertySuccess -> Series m () -> Series m PropertySuccess
forall a b. a -> Series m b -> Series m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Series m PropertyFailure -> Series m ()
forall a. Series m a -> Series m ()
forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertyFailure
failure
      -- }}}

    Quantification
Exists -> Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
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 <- PropertySeries m -> Series m PropertySuccess
forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples (PropertySeries m -> Series m PropertySuccess)
-> PropertySeries m -> Series m PropertySuccess
forall a b. (a -> b) -> a -> b
$ Env m -> Property m -> PropertySeries m
forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env (Property m -> PropertySeries m) -> Property m -> PropertySeries m
forall a b. (a -> b) -> a -> b
$ b -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
test (b -> Property m) -> b -> Property m
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
          let arg :: Argument
arg = a -> Argument
forall a. Show a => a -> Argument
show a
x

          PropertySuccess -> Series m PropertySuccess
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropertySuccess -> Series m PropertySuccess)
-> PropertySuccess -> Series m PropertySuccess
forall a b. (a -> b) -> a -> b
$
            case PropertySuccess
s of
              Exist [Argument]
args PropertySuccess
etc -> [Argument] -> PropertySuccess -> PropertySuccess
Exist (Argument
argArgument -> [Argument] -> [Argument]
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 PropertyFailure -> Series m () -> Series m PropertyFailure
forall a b. a -> Series m b -> Series m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Series m PropertySuccess -> Series m ()
forall a. Series m a -> Series m ()
forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertySuccess
success
      -- }}}

    Quantification
ExistsUnique -> Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
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 = Int
-> Series m ([Argument], PropertySuccess)
-> Series m [([Argument], PropertySuccess)]
forall (m :: * -> *) a. MonadLogic m => Int -> m a -> m [a]
atMost Int
2 (Series m ([Argument], PropertySuccess)
 -> Series m [([Argument], PropertySuccess)])
-> Series m ([Argument], PropertySuccess)
-> Series m [([Argument], PropertySuccess)]
forall a b. (a -> b) -> a -> b
$ do
          (Property m
prop, [Argument]
args) <- Series m (Property m, [Argument])
closest
          PropertySuccess
ex <- Series m PropertySuccess -> Series m PropertySuccess
forall a. Series m a -> Series m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once (Series m PropertySuccess -> Series m PropertySuccess)
-> Series m PropertySuccess -> Series m PropertySuccess
forall a b. (a -> b) -> a -> b
$ PropertySeries m -> Series m PropertySuccess
forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples (PropertySeries m -> Series m PropertySuccess)
-> PropertySeries m -> Series m PropertySuccess
forall a b. (a -> b) -> a -> b
$ Env m -> Property m -> PropertySeries m
forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env (Property m -> PropertySeries m) -> Property m -> PropertySeries m
forall a b. (a -> b) -> a -> b
$ Property m -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
test Property m
prop
          ([Argument], PropertySuccess)
-> Series m ([Argument], PropertySuccess)
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Argument]
args, PropertySuccess
ex)

        success :: Series m PropertySuccess
success =
          Series m [([Argument], PropertySuccess)]
search Series m [([Argument], PropertySuccess)]
-> ([([Argument], PropertySuccess)] -> Series m PropertySuccess)
-> Series m PropertySuccess
forall a b. Series m a -> (a -> Series m b) -> Series m b
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)] -> PropertySuccess -> Series m PropertySuccess
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropertySuccess -> Series m PropertySuccess)
-> PropertySuccess -> Series m PropertySuccess
forall a b. (a -> b) -> a -> b
$ [Argument] -> PropertySuccess -> PropertySuccess
ExistUnique [Argument]
x PropertySuccess
s
                [([Argument], PropertySuccess)]
_ -> Series m PropertySuccess
forall a. Series m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

        failure :: Series m PropertyFailure
failure =
          Series m [([Argument], PropertySuccess)]
search Series m [([Argument], PropertySuccess)]
-> ([([Argument], PropertySuccess)] -> Series m PropertyFailure)
-> Series m PropertyFailure
forall a b. Series m a -> (a -> Series m b) -> Series m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
            \[([Argument], PropertySuccess)]
examples ->
              case [([Argument], PropertySuccess)]
examples of
                [] -> PropertyFailure -> Series m PropertyFailure
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return PropertyFailure
NotExist
                ([Argument]
x1,PropertySuccess
s1):([Argument]
x2,PropertySuccess
s2):[([Argument], PropertySuccess)]
_ -> PropertyFailure -> Series m PropertyFailure
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropertyFailure -> Series m PropertyFailure)
-> PropertyFailure -> Series m PropertyFailure
forall a b. (a -> b) -> a -> b
$ [Argument]
-> PropertySuccess
-> [Argument]
-> PropertySuccess
-> PropertyFailure
AtLeastTwo [Argument]
x1 PropertySuccess
s1 [Argument]
x2 PropertySuccess
s2
                [([Argument], PropertySuccess)]
_ -> Series m PropertyFailure
forall a. Series m a
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  | Bool
otherwise = do
      Maybe (a, m a)
m' <- m a -> m (Maybe (a, m a))
forall a. m a -> m (Maybe (a, m a))
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 -> [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just (a
x,m a
rest) ->
          (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> m [a] -> m [a]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` Int -> m a -> m [a]
forall (m :: * -> *) a. MonadLogic m => Int -> m a -> m [a]
atMost (Int
nInt -> Int -> Int
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) =
  Property m -> Property m
forall (m :: * -> *). Property m -> Property m
makeAtomic (Property m -> Property m) -> Property m -> Property m
forall a b. (a -> b) -> a -> b
$ Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ (Env m -> Env m)
-> Reader (Env m) (PropertySeries m)
-> Reader (Env m) (PropertySeries m)
forall a.
(Env m -> Env m)
-> ReaderT (Env m) Identity a -> ReaderT (Env m) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env m
env -> Env m
env { 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 = a -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
forAll

-- | Set the universal quantification context.
--
-- @since 1.0
forAll :: Testable m a => a -> Property m
forAll :: forall (m :: * -> *) a. Testable m a => a -> Property m
forAll = Quantification -> Property m -> Property m
forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
Forall (Property m -> Property m) -> (a -> Property m) -> a -> Property m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
test

-- | Set the existential quantification context.
--
-- @since 1.0
exists :: Testable m a => a -> Property m
exists :: forall (m :: * -> *) a. Testable m a => a -> Property m
exists = Quantification -> Property m -> Property m
forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
Exists (Property m -> Property m) -> (a -> Property m) -> a -> Property m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property m
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.0
existsUnique :: Testable m a => a -> Property m
existsUnique :: forall (m :: * -> *) a. Testable m a => a -> Property m
existsUnique = Quantification -> Property m -> Property m
forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
ExistsUnique (Property m -> Property m) -> (a -> Property m) -> a -> Property m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property m
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.0
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 = Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (Reader (Env m) (PropertySeries m) -> Property m)
-> Reader (Env m) (PropertySeries m) -> Property m
forall a b. (a -> b) -> a -> b
$ do
  Env m
env <- ReaderT (Env m) Identity (Env m)
forall r (m :: * -> *). MonadReader r m => m r
ask

  let
    counterExample :: Series m PropertyFailure
counterExample = Series m PropertyFailure -> Series m PropertyFailure
forall a. Series m a -> Series m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once (Series m PropertyFailure -> Series m PropertyFailure)
-> Series m PropertyFailure -> Series m PropertyFailure
forall a b. (a -> b) -> a -> b
$ PropertySeries m -> Series m PropertyFailure
forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples (PropertySeries m -> Series m PropertyFailure)
-> PropertySeries m -> Series m PropertyFailure
forall a b. (a -> b) -> a -> b
$ Env m -> Property m -> PropertySeries m
forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env' (Property m -> PropertySeries m) -> Property m -> PropertySeries m
forall a b. (a -> b) -> a -> b
$ c -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
freshContext c
cond
      -- NB: we do not invoke the test hook in the antecedent
      where env' :: Env m
env' = Env m
env { testHook = const $ return () }

    consequent :: PropertySeries m
consequent = Env m -> Property m -> PropertySeries m
forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env (Property m -> PropertySeries m) -> Property m -> PropertySeries m
forall a b. (a -> b) -> a -> b
$ a -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
freshContext a
prop

    badTestHook :: Series m ()
badTestHook = m () -> Series m ()
forall (m :: * -> *) a. Monad m => m a -> Series m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> Series m ()) -> m () -> Series m ()
forall a b. (a -> b) -> a -> b
$ Env m -> TestQuality -> m ()
forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
BadTest

    success :: Series m PropertySuccess
success =
      Series m PropertyFailure
-> (PropertyFailure -> Series m PropertySuccess)
-> Series m PropertySuccess
-> Series m PropertySuccess
forall a b.
Series m a -> (a -> Series m b) -> Series m b -> Series m b
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte Series m PropertyFailure
counterExample
        -- then
        (\PropertyFailure
ex -> do
          Series m ()
badTestHook
          PropertySuccess -> Series m PropertySuccess
forall a. a -> Series m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropertySuccess -> Series m PropertySuccess)
-> PropertySuccess -> Series m PropertySuccess
forall a b. (a -> b) -> a -> b
$ PropertyFailure -> PropertySuccess
Vacuously PropertyFailure
ex
        )
        -- else
        (PropertySeries m -> Series m PropertySuccess
forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples PropertySeries m
consequent)

    failure :: Series m PropertyFailure
failure =
      Series m PropertyFailure
-> (PropertyFailure -> Series m PropertyFailure)
-> Series m PropertyFailure
-> Series m PropertyFailure
forall a b.
Series m a -> (a -> Series m b) -> Series m b -> Series m b
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte Series m PropertyFailure
counterExample
        -- then
        (Series m PropertyFailure
-> PropertyFailure -> Series m PropertyFailure
forall a b. a -> b -> a
const (Series m PropertyFailure
 -> PropertyFailure -> Series m PropertyFailure)
-> Series m PropertyFailure
-> PropertyFailure
-> Series m PropertyFailure
forall a b. (a -> b) -> a -> b
$ do
          m () -> Series m ()
forall (m :: * -> *) a. Monad m => m a -> Series m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> Series m ()) -> m () -> Series m ()
forall a b. (a -> b) -> a -> b
$ Env m -> TestQuality -> m ()
forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
BadTest
          Series m PropertyFailure
forall a. Series m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
        )
        -- else
        (PropertySeries m -> Series m PropertyFailure
forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples PropertySeries m
consequent)

  PropertySeries m -> Reader (Env m) (PropertySeries m)
forall a. a -> ReaderT (Env m) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropertySeries m -> Reader (Env m) (PropertySeries m))
-> PropertySeries m -> Reader (Env m) (PropertySeries m)
forall a b. (a -> b) -> a -> b
$ Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
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.0
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 = Reader (Env m) (PropertySeries m) -> Property m
forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (PropertySeries m -> PropertySeries m
changeDepthPS (PropertySeries m -> PropertySeries m)
-> Reader (Env m) (PropertySeries m)
-> Reader (Env m) (PropertySeries m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Property m -> Reader (Env m) (PropertySeries m)
forall (m :: * -> *).
Property m -> Reader (Env m) (PropertySeries m)
unProperty (a -> Property m
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) =
      Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries
        ((Int -> Int)
-> Series m PropertySuccess -> Series m PropertySuccess
forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m PropertySuccess
ss)
        ((Int -> Int)
-> Series m PropertyFailure -> Series m PropertyFailure
forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m PropertyFailure
sf)
        ((Property m -> Property m)
-> (Property m, [Argument]) -> (Property m, [Argument])
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Int -> Int) -> Property m -> Property m
forall (m :: * -> *) a.
Testable m a =>
(Int -> Int) -> a -> Property m
changeDepth Int -> Int
modifyDepth) ((Property m, [Argument]) -> (Property m, [Argument]))
-> Series m (Property m, [Argument])
-> Series m (Property m, [Argument])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          (Int -> Int)
-> Series m (Property m, [Argument])
-> Series m (Property m, [Argument])
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.0
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 = Series m a -> (a -> b) -> Property m
forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
over (Series m a -> (a -> b) -> Property m)
-> Series m a -> (a -> b) -> Property m
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Series m a -> Series m a
forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m a
forall (m :: * -> *) a. Serial m a => Series m a
series

-- }}}