    -- 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
          x <- Series m a
    s
          (p, args) <- searchClosest $ unProp env $ test $ f x
          return (p, show x : 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
              x <- Series m a
    s
              failure <- searchCounterExamples $ unProp env $ test $ f x
              let arg = a -> Argument
    forall a. Show a => a -> Argument
    show a
    x
              return $
                case 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
              x <- Series m a
    s
              s <- searchExamples $ unProp env $ test $ f x
              let arg = a -> Argument
    forall a. Show a => a -> Argument
    show a
    x

              return $
                case 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
              (prop, args) <- Series m (Property m, [Argument])
    closest
              ex <- once $ searchExamples $ unProp env $ test prop
              return (args, 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
          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 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 <- ReaderT (Env m) Identity (Env m)
    forall r (m :: * -> *). MonadReader r m => m r
    ask

      let
        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 = 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 = 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 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
    -> (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)

      return $ atomicProperty success 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

    -- }}}