-- 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 MultiParamTypeClasses, FlexibleInstances, TypeFamilies,
             ScopedTypeVariables, DeriveDataTypeable #-}

-- CPP is for Typeable1 vs Typeable
{-# LANGUAGE CPP #-}

-- 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
{-# LANGUAGE Trustworthy #-}
#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.Monad
import Control.Monad.Logic
import Control.Monad.Reader
import Control.Applicative
import Data.Typeable

------------------------------
-- 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
        (mkTyCon3 "smallcheck" "Test.SmallCheck.Property" "Property")
        [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 '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 ∃! (x, y): p x y is not the same as ∃! x: ∃! y: p x y.
--
-- For example, ∃! x: ∃! y: |x| = |y| is true (it holds only when x=0), but ∃! (x,y): |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
prop, [Argument]
args) -> ((Int -> Int) -> Property m -> Property m
forall (m :: * -> *) a.
Testable m a =>
(Int -> Int) -> a -> Property m
changeDepth Int -> Int
modifyDepth Property m
prop, [Argument]
args)) ((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

-- }}}