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

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.
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.
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'.
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 = 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 '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 = 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.
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.
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.
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).
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.
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.
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

-- }}}