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

#if !NEWTYPEABLE
-- Typeable here is not polykinded yet, and also GHC doesn't know how to
-- derive this.
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) = 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 -> 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)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just PropertyFailure
x) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)) forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a. Int -> Series m a -> LogicT m a
runSeries Int
depth forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples forall a b. (a -> b) -> a -> b
$
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r a. Reader r a -> r -> a
runReader (forall (m :: * -> *).
Quantification -> (TestQuality -> m ()) -> Env m
Env Quantification
Forall TestQuality -> m ()
hook) forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *).
Property m -> Reader (Env m) (PropertySeries m)
unProperty Property m
prop

atomicProperty :: Series m PropertySuccess -> Series m PropertyFailure -> PropertySeries m
atomicProperty :: forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
s Series m PropertyFailure
f =
  let prop :: PropertySeries m
prop = forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
s Series m PropertyFailure
f (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
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) =
  forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Reader (Env m) (PropertySeries m)
prop forall a b. (a -> b) -> a -> b
$ \PropertySeries m
ps ->
    forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty (forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples PropertySeries m
ps) (forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples PropertySeries m
ps)

-- | @'over' s $ \\x -> p x@ makes @x@ range over the 'Series' @s@ (by
-- default, all variables range over the 'series' for their types).
--
-- Note that, unlike the quantification operators, this affects only the
-- variable following the operator and not subsequent variables.
--
-- 'over' does not affect the quantification context.
--
-- @since 1.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 = 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 =
  forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Env m
env ->

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

    forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty
      (forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Series m (PropertySeries m)
pair)
      (forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Series m (PropertySeries m)
pair)

-- }}}

-------------------------------
-- Testable class and instances
-------------------------------
-- {{{

-- | Class of tests that can be run in a monad. For pure tests, it is
-- recommended to keep their types polymorphic in @m@ rather than
-- specialising it to 'Data.Functor.Identity'.
--
-- @since 1.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 = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Env m
env ->
    let
      success :: Series m PropertySuccess
success = do
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
        if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe Argument -> PropertySuccess
PropertyTrue forall a. Maybe a
Nothing else forall (m :: * -> *) a. MonadPlus m => m a
mzero
      failure :: Series m PropertyFailure
failure = Maybe Argument -> PropertyFailure
PropertyFalse forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertySuccess
success
    in 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 = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Env m
env ->
    let
      success :: Series m PropertySuccess
success = do
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
        forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadPlus m => m a
mzero) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Argument -> PropertySuccess
PropertyTrue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) Either Argument Argument
r
      failure :: Series m PropertyFailure
failure = do
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Env m -> TestQuality -> m ()
testHook Env m
env TestQuality
GoodTest
        forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Argument -> PropertyFailure
PropertyFalse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) (forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadPlus m => m a
mzero) Either Argument Argument
r
    in 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 = forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
testFunction forall (m :: * -> *) a. Serial m a => Series m a
series

instance (Monad m, m ~ n) => Testable n (Property m) where
  test :: Property m -> Property n
test = 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 = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader 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) <- forall (m :: * -> *).
PropertySeries m -> Series m (Property m, [Argument])
searchClosest forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
test forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
      forall (m :: * -> *) a. Monad m => a -> m a
return (Property m
p, forall a. Show a => a -> Argument
show a
x forall a. a -> [a] -> [a]
: [Argument]
args)
  in

  case forall (m :: * -> *). Env m -> Quantification
quantification Env m
env of
    Quantification
Forall -> forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
success Series m PropertyFailure
failure Series m (Property m, [Argument])
closest
      -- {{{
      where
        failure :: Series m PropertyFailure
failure = do
          a
x <- Series m a
s
          PropertyFailure
failure <- forall (m :: * -> *). PropertySeries m -> Series m PropertyFailure
searchCounterExamples forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
test forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
          let arg :: Argument
arg = forall a. Show a => a -> Argument
show a
x
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
            case PropertyFailure
failure of
              CounterExample [Argument]
args PropertyFailure
etc -> [Argument] -> PropertyFailure -> PropertyFailure
CounterExample (Argument
argforall a. a -> [a] -> [a]
:[Argument]
args) PropertyFailure
etc
              PropertyFailure
_ -> [Argument] -> PropertyFailure -> PropertyFailure
CounterExample [Argument
arg] PropertyFailure
failure

        success :: Series m PropertySuccess
success = Maybe Argument -> PropertySuccess
PropertyTrue forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertyFailure
failure
      -- }}}

    Quantification
Exists -> forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries Series m PropertySuccess
success Series m PropertyFailure
failure Series m (Property m, [Argument])
closest
      -- {{{
      where
        success :: Series m PropertySuccess
success = do
          a
x <- Series m a
s
          PropertySuccess
s <- forall (m :: * -> *). PropertySeries m -> Series m PropertySuccess
searchExamples forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Env t -> Property t -> PropertySeries t
unProp Env m
env forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Testable m a => a -> Property m
test forall a b. (a -> b) -> a -> b
$ a -> b
f a
x
          let arg :: Argument
arg = forall a. Show a => a -> Argument
show a
x

          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
            case PropertySuccess
s of
              Exist [Argument]
args PropertySuccess
etc -> [Argument] -> PropertySuccess -> PropertySuccess
Exist (Argument
argforall a. a -> [a] -> [a]
:[Argument]
args) PropertySuccess
etc
              PropertySuccess
_ -> [Argument] -> PropertySuccess -> PropertySuccess
Exist [Argument
arg] PropertySuccess
s

        failure :: Series m PropertyFailure
failure = PropertyFailure
NotExist forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot Series m PropertySuccess
success
      -- }}}

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

        success :: Series m PropertySuccess
success =
          Series m [([Argument], PropertySuccess)]
search forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
            \[([Argument], PropertySuccess)]
examples ->
              case [([Argument], PropertySuccess)]
examples of
                [([Argument]
x,PropertySuccess
s)] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Argument] -> PropertySuccess -> PropertySuccess
ExistUnique [Argument]
x PropertySuccess
s
                [([Argument], PropertySuccess)]
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero

        failure :: Series m PropertyFailure
failure =
          Series m [([Argument], PropertySuccess)]
search forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
            \[([Argument], PropertySuccess)]
examples ->
              case [([Argument], PropertySuccess)]
examples of
                [] -> forall (m :: * -> *) a. Monad m => a -> m a
return PropertyFailure
NotExist
                ([Argument]
x1,PropertySuccess
s1):([Argument]
x2,PropertySuccess
s2):[([Argument], PropertySuccess)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Argument]
-> PropertySuccess
-> [Argument]
-> PropertySuccess
-> PropertyFailure
AtLeastTwo [Argument]
x1 PropertySuccess
s1 [Argument]
x2 PropertySuccess
s2
                [([Argument], PropertySuccess)]
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
      -- }}}

atMost :: 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 forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
  | Bool
otherwise = do
      Maybe (a, m a)
m' <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just (a
x,m a
rest) ->
          (a
xforall a. a -> [a] -> [a]
:) forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` forall (m :: * -> *) a. MonadLogic m => Int -> m a -> m [a]
atMost (Int
nforall a. Num a => a -> a -> a
-Int
1) m a
rest

-- }}}

------------------------------
-- Test constructors
------------------------------
-- {{{

quantify :: Quantification -> Property m -> Property m
quantify :: forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
q (Property Reader (Env m) (PropertySeries m)
a) =
  forall (m :: * -> *). Property m -> Property m
makeAtomic forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\Env m
env -> Env m
env { quantification :: Quantification
quantification = Quantification
q }) Reader (Env m) (PropertySeries m)
a

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

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

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

-- | Set the uniqueness quantification context.
--
-- Bear in mind that \( \exists! x, y\colon p\, x \, y \)
-- is not the same as \( \exists! x \colon \exists! y \colon p \, x \, y \).
--
-- For example, \( \exists! x \colon \exists! y \colon |x| = |y| \)
-- is true (it holds only when \(x=y=0\)),
-- but \( \exists! x, y \colon |x| = |y| \) is false
-- (there are many such pairs).
--
-- As is customary in mathematics,
-- @'existsUnique' $ \\x y -> p x y@ is equivalent to
-- @'existsUnique' $ \\(x, y) -> p x y@ and not to
-- @'existsUnique' $ \\x -> 'existsUnique' $ \\y -> p x y@
-- (the latter, of course, may be explicitly written when desired).
--
-- That is, all the variables affected by the same uniqueness context are
-- quantified simultaneously as a tuple.
--
-- @since 1.0
existsUnique :: Testable m a => a -> Property m
existsUnique :: forall (m :: * -> *) a. Testable m a => a -> Property m
existsUnique = forall (m :: * -> *). Quantification -> Property m -> Property m
quantify Quantification
ExistsUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Testable m a => a -> Property m
test

-- | The '==>' operator can be used to express a restricting condition
-- under which a property should hold. It corresponds to implication in the
-- classical logic.
--
-- Note that '==>' resets the quantification context for its operands to
-- the default (universal).
--
-- @since 1.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 = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property forall a b. (a -> b) -> a -> b
$ do
  Env m
env <- forall r (m :: * -> *). MonadReader r m => m r
ask

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

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

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

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

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

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure -> PropertySeries m
atomicProperty Series m PropertySuccess
success Series m PropertyFailure
failure

-- | Run property with a modified depth. Affects all quantified variables
-- in the property.
--
-- @since 1.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 = forall (m :: * -> *).
Reader (Env m) (PropertySeries m) -> Property m
Property (PropertySeries m -> PropertySeries m
changeDepthPS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
Property m -> Reader (Env m) (PropertySeries m)
unProperty (forall (m :: * -> *) a. Testable m a => a -> Property m
test a
a))
  where
    changeDepthPS :: PropertySeries m -> PropertySeries m
changeDepthPS (PropertySeries Series m PropertySuccess
ss Series m PropertyFailure
sf Series m (Property m, [Argument])
sc) =
      forall (m :: * -> *).
Series m PropertySuccess
-> Series m PropertyFailure
-> Series m (Property m, [Argument])
-> PropertySeries m
PropertySeries
        (forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m PropertySuccess
ss)
        (forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m PropertyFailure
sf)
        (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (m :: * -> *) a.
Testable m a =>
(Int -> Int) -> a -> Property m
changeDepth Int -> Int
modifyDepth) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth Series m (Property m, [Argument])
sc)

-- | Quantify the function's argument over its 'series', but adjust the
-- depth. This doesn't affect any subsequent variables.
--
-- @since 1.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 = forall a (m :: * -> *) b.
(Show a, Testable m b) =>
Series m a -> (a -> b) -> Property m
over forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Int -> Int) -> Series m a -> Series m a
localDepth Int -> Int
modifyDepth forall (m :: * -> *) a. Serial m a => Series m a
series

-- }}}