-- 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 ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}

-- 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 Test.SmallCheck.Series
import Test.SmallCheck.SeriesMonad
import Test.SmallCheck.Property.Result
import Control.Arrow (first)
import Control.Monad (liftM, mzero)
import Control.Monad.Logic (MonadLogic, runLogicT, ifte, once, msplit, lnot)
import Control.Monad.Reader (Reader, runReader, lift, ask, local, reader)
import Control.Applicative (pure, (<$>), (<$))
import Data.Typeable (Typeable(..))

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

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

-- | The type of properties over the monad @m@.
newtype Property m = Property { Property m -> Reader (Env m) (PropertySeries m)
unProperty :: Reader (Env m) (PropertySeries m) }
#if NEWTYPEABLE
  deriving Typeable
#endif

data PropertySeries m =
  PropertySeries
    { PropertySeries m -> Series m PropertySuccess
searchExamples        :: Series m PropertySuccess
    , PropertySeries m -> Series m PropertyFailure
searchCounterExamples :: Series m PropertyFailure
    , PropertySeries m -> Series m (Property m, [Argument])
searchClosest         :: Series m (Property m, [Argument])
    }

data Env m =
  Env
    { Env m -> Quantification
quantification :: Quantification
    , Env m -> TestQuality -> m ()
testHook :: TestQuality -> m ()
    }

data Quantification
  = Forall
  | Exists
  | ExistsUnique

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
/= :: TestQuality -> TestQuality -> Bool
$c/= :: TestQuality -> TestQuality -> Bool
== :: TestQuality -> TestQuality -> Bool
$c== :: 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
min :: TestQuality -> TestQuality -> TestQuality
$cmin :: TestQuality -> TestQuality -> TestQuality
max :: TestQuality -> TestQuality -> TestQuality
$cmax :: TestQuality -> TestQuality -> TestQuality
>= :: TestQuality -> TestQuality -> Bool
$c>= :: TestQuality -> TestQuality -> Bool
> :: TestQuality -> TestQuality -> Bool
$c> :: TestQuality -> TestQuality -> Bool
<= :: TestQuality -> TestQuality -> Bool
$c<= :: TestQuality -> TestQuality -> Bool
< :: TestQuality -> TestQuality -> Bool
$c< :: TestQuality -> TestQuality -> Bool
compare :: TestQuality -> TestQuality -> Ordering
$ccompare :: TestQuality -> TestQuality -> Ordering
$cp1Ord :: Eq 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
enumFromThenTo :: TestQuality -> TestQuality -> TestQuality -> [TestQuality]
$cenumFromThenTo :: TestQuality -> TestQuality -> TestQuality -> [TestQuality]
enumFromTo :: TestQuality -> TestQuality -> [TestQuality]
$cenumFromTo :: TestQuality -> TestQuality -> [TestQuality]
enumFromThen :: TestQuality -> TestQuality -> [TestQuality]
$cenumFromThen :: TestQuality -> TestQuality -> [TestQuality]
enumFrom :: TestQuality -> [TestQuality]
$cenumFrom :: TestQuality -> [TestQuality]
fromEnum :: TestQuality -> Int
$cfromEnum :: TestQuality -> Int
toEnum :: Int -> TestQuality
$ctoEnum :: Int -> TestQuality
pred :: TestQuality -> TestQuality
$cpred :: TestQuality -> TestQuality
succ :: TestQuality -> TestQuality
$csucc :: TestQuality -> TestQuality
Enum, Int -> TestQuality -> ShowS
[TestQuality] -> ShowS
TestQuality -> Argument
(Int -> TestQuality -> ShowS)
-> (TestQuality -> Argument)
-> ([TestQuality] -> ShowS)
-> Show TestQuality
forall a.
(Int -> a -> ShowS) -> (a -> Argument) -> ([a] -> ShowS) -> Show a
showList :: [TestQuality] -> ShowS
$cshowList :: [TestQuality] -> ShowS
show :: TestQuality -> Argument
$cshow :: TestQuality -> Argument
showsPrec :: Int -> TestQuality -> ShowS
$cshowsPrec :: Int -> TestQuality -> ShowS
Show)

#if !NEWTYPEABLE
-- Typeable here is not polykinded yet, and also GHC doesn't know how to
-- derive this.
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 :: 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 :: 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 (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 (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 :: 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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure PropertySeries m
prop, []))
  in PropertySeries m
prop

makeAtomic :: Property m -> Property m
makeAtomic :: 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 (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.
over
  :: (Show a, Testable m b)
  => Series m a -> (a -> b) -> Property m
over :: 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.
monadic :: Testable m a => m a -> Property m
monadic :: 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 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 (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'.
class Monad m => Testable m a where
  test :: a -> Property m

instance Monad m => Testable m Bool where
  test :: Bool -> Property m
test Bool
b = 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 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 (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 (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 (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 (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Series m PropertySuccess -> 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 'Bool' instance, but includes an explanation of the result.
--
-- 'Left' and 'Right' correspond to test failure and success
-- respectively.
instance Monad m => Testable m (Either Reason Reason) where
  test :: 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 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 (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 (m :: * -> *) a. MonadPlus m => m a
mzero) (PropertySuccess -> Series m PropertySuccess
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 (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 (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 (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 n
forall a. a -> a
id

testFunction
  :: (Show a, Testable m b)
  => Series m a -> (a -> b) -> Property m
testFunction :: 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 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 (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 (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 (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Series m PropertyFailure -> 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 (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 (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Series m PropertySuccess -> 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 (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 (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 (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 (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 (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 (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 (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 (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 (m :: * -> *) a. MonadPlus m => m a
mzero
      -- }}}

atMost :: MonadLogic m => Int -> m a -> m [a]
atMost :: 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 (m :: * -> *) a. Monad m => a -> m a
return []
  | Bool
otherwise = do
      Maybe (a, m a)
m' <- 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 (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 :: 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 r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env m
env -> Env m
env { quantification :: Quantification
quantification = Quantification
q }) Reader (Env m) (PropertySeries m)
a

freshContext :: Testable m a => a -> Property m
freshContext :: a -> Property m
freshContext = a -> Property m
forall (m :: * -> *) a. Testable m a => a -> Property m
forAll

-- | Set the universal quantification context.
forAll :: Testable m a => a -> Property m
forAll :: 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.
exists :: Testable m a => a -> Property m
exists :: 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.
existsUnique :: Testable m a => a -> Property m
existsUnique :: 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).
infixr 0 ==>
(==>) :: (Testable m c, Testable m a) => c -> a -> Property m
c
cond ==> :: 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 (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 :: TestQuality -> m ()
testHook = m () -> TestQuality -> m ()
forall a b. a -> b -> a
const (m () -> TestQuality -> m ()) -> m () -> TestQuality -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
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 (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 (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 (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 (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 (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 (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 (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.
changeDepth :: Testable m a => (Depth -> Depth) -> a -> Property m
changeDepth :: (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 (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.
changeDepth1 :: (Show a, Serial m a, Testable m b) => (Depth -> Depth) -> (a -> b) -> Property m
changeDepth1 :: (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

-- }}}