{-# LANGUAGE CPP #-}
#ifndef NO_SAFE_HASKELL
#if !defined(NO_ST_MONAD) && !(MIN_VERSION_base(4,8,0))
{-# LANGUAGE Trustworthy #-}
#else
{-# LANGUAGE Safe #-}
#endif
#endif
#ifndef NO_ST_MONAD
{-# LANGUAGE Rank2Types #-}
#endif
{-|
Module   : Test.QuickCheck.Monadic

Allows testing of monadic values. Will generally follow this form:

@
prop_monadic a b = 'monadicIO' $ do
  a\' \<- 'run' (f a)
  b\' \<- 'run' (f b)
  -- ...
  'assert' someBoolean
@

Example using the @FACTOR(1)@ command-line utility:

@
import System.Process
import Test.QuickCheck
import Test.QuickCheck.Monadic

-- $ factor 16
-- 16: 2 2 2 2
factor :: Integer -> IO [Integer]
factor n = parse \`fmap\` 'System.Process.readProcess' \"factor\" [show n] \"\" where

  parse :: String -> [Integer]
  parse = map read . tail . words

prop_factor :: Positive Integer -> Property
prop_factor ('Test.QuickCheck.Modifiers.Positive' n) = 'monadicIO' $ do
  factors \<- 'run' (factor n)

  'assert' (product factors == n)
@

>>> quickCheck prop_factor
+++ OK, passed 100 tests.

See the paper \"<http://www.cse.chalmers.se/~rjmh/Papers/QuickCheckST.ps Testing Monadic Code with QuickCheck>\".
-}
module Test.QuickCheck.Monadic (
  -- * Property monad
    PropertyM(..)

  -- * Monadic specification combinators
  , run
  , assert
  , assertWith
  , pre
  , wp
  , pick
  , forAllM
  , monitor
  , stop

  -- * Run functions
  , monadic
  , monadic'
  , monadicIO
#ifndef NO_ST_MONAD
  , monadicST
  , runSTGen
#endif
  ) where

--------------------------------------------------------------------------
-- imports

import Test.QuickCheck.Gen
import Test.QuickCheck.Gen.Unsafe
import Test.QuickCheck.Property

import Control.Monad(liftM, liftM2)

import Control.Monad.ST
import Control.Applicative

#ifndef NO_TRANSFORMERS
import Control.Monad.IO.Class
import Control.Monad.Trans.Class
#endif

#ifndef NO_MONADFAIL
import qualified Control.Monad.Fail as Fail
#endif

--------------------------------------------------------------------------
-- type PropertyM

-- | The property monad is really a monad transformer that can contain
-- monadic computations in the monad @m@ it is parameterized by:
--
--   * @m@ - the @m@-computations that may be performed within @PropertyM@
--
-- Elements of @PropertyM m a@ may mix property operations and @m@-computations.
newtype PropertyM m a =
  MkPropertyM { forall (m :: * -> *) a.
PropertyM m a -> (a -> Gen (m Property)) -> Gen (m Property)
unPropertyM :: (a -> Gen (m Property)) -> Gen (m Property) }

bind :: PropertyM m a -> (a -> PropertyM m b) -> PropertyM m b
MkPropertyM (a -> Gen (m Property)) -> Gen (m Property)
m bind :: forall (m :: * -> *) a b.
PropertyM m a -> (a -> PropertyM m b) -> PropertyM m b
`bind` a -> PropertyM m b
f = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (\b -> Gen (m Property)
k -> (a -> Gen (m Property)) -> Gen (m Property)
m (\a
a -> forall (m :: * -> *) a.
PropertyM m a -> (a -> Gen (m Property)) -> Gen (m Property)
unPropertyM (a -> PropertyM m b
f a
a) b -> Gen (m Property)
k))

fail_ :: Monad m => String -> PropertyM m a
fail_ :: forall (m :: * -> *) a. Monad m => String -> PropertyM m a
fail_ String
s = forall prop (m :: * -> *) a.
(Testable prop, Monad m) =>
prop -> PropertyM m a
stop (Result
failed { reason :: String
reason = String
s })

instance Functor (PropertyM m) where
  fmap :: forall a b. (a -> b) -> PropertyM m a -> PropertyM m b
fmap a -> b
f (MkPropertyM (a -> Gen (m Property)) -> Gen (m Property)
m) = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (\b -> Gen (m Property)
k -> (a -> Gen (m Property)) -> Gen (m Property)
m (b -> Gen (m Property)
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f))

instance Applicative (PropertyM m) where
  pure :: forall a. a -> PropertyM m a
pure a
x = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (\a -> Gen (m Property)
k -> a -> Gen (m Property)
k a
x)
  PropertyM m (a -> b)
mf <*> :: forall a b. PropertyM m (a -> b) -> PropertyM m a -> PropertyM m b
<*> PropertyM m a
mx =
    PropertyM m (a -> b)
mf forall (m :: * -> *) a b.
PropertyM m a -> (a -> PropertyM m b) -> PropertyM m b
`bind` \a -> b
f -> PropertyM m a
mx forall (m :: * -> *) a b.
PropertyM m a -> (a -> PropertyM m b) -> PropertyM m b
`bind` \a
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b
f a
x)

instance Monad m => Monad (PropertyM m) where
  return :: forall a. a -> PropertyM m a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  >>= :: forall a b. PropertyM m a -> (a -> PropertyM m b) -> PropertyM m b
(>>=) = forall (m :: * -> *) a b.
PropertyM m a -> (a -> PropertyM m b) -> PropertyM m b
bind
#if !MIN_VERSION_base(4,13,0)
  fail = fail_
#endif

#ifndef NO_MONADFAIL
instance Monad m => Fail.MonadFail (PropertyM m) where
  fail :: forall a. String -> PropertyM m a
fail = forall (m :: * -> *) a. Monad m => String -> PropertyM m a
fail_
#endif

#ifndef NO_TRANSFORMERS
instance MonadTrans PropertyM where
  lift :: forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
lift = forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run

instance MonadIO m => MonadIO (PropertyM m) where
  liftIO :: forall a. IO a -> PropertyM m a
liftIO = forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
#endif

stop :: (Testable prop, Monad m) => prop -> PropertyM m a
stop :: forall prop (m :: * -> *) a.
(Testable prop, Monad m) =>
prop -> PropertyM m a
stop prop
p = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (\a -> Gen (m Property)
_k -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall (m :: * -> *) a. Monad m => a -> m a
return (forall prop. Testable prop => prop -> Property
property prop
p)))

-- should think about strictness/exceptions here
-- assert :: Testable prop => prop -> PropertyM m ()
-- | Allows embedding non-monadic properties into monadic ones.
assert :: Monad m => Bool -> PropertyM m ()
assert :: forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
True  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
assert Bool
False = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Assertion failed"

-- | Like 'assert' but allows caller to specify an explicit message to show on failure.
--
-- __Example:__
--
-- @
-- do
--   assertWith True  "My first predicate."
--   assertWith False "My other predicate."
--   ...
-- @
--
-- @
-- Assertion failed (after 2 tests):
--     Passed: My first predicate
--     Failed: My other predicate
-- @
assertWith :: Monad m => Bool -> String -> PropertyM m ()
assertWith :: forall (m :: * -> *). Monad m => Bool -> String -> PropertyM m ()
assertWith Bool
condition String
msg = do
    let prefix :: String
prefix = if Bool
condition then String
"Passed: " else String
"Failed: "
    forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample forall a b. (a -> b) -> a -> b
$ String
prefix forall a. [a] -> [a] -> [a]
++ String
msg
    forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
condition

-- should think about strictness/exceptions here
-- | Tests preconditions. Unlike 'assert' this does not cause the
-- property to fail, rather it discards them just like using the
-- implication combinator 'Test.QuickCheck.Property.==>'.
--
-- This allows representing the <https://en.wikipedia.org/wiki/Hoare_logic Hoare triple>
--
-- > {p} x ← e{q}
--
-- as
--
-- @
-- pre p
-- x \<- run e
-- assert q
-- @
--
pre :: Monad m => Bool -> PropertyM m ()
pre :: forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
pre Bool
True  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
pre Bool
False = forall prop (m :: * -> *) a.
(Testable prop, Monad m) =>
prop -> PropertyM m a
stop Result
rejected

-- should be called lift?
-- | The lifting operation of the property monad. Allows embedding
-- monadic\/'IO'-actions in properties:
--
-- @
-- log :: Int -> IO ()
--
-- prop_foo n = monadicIO $ do
--   run (log n)
--   -- ...
-- @
run :: Monad m => m a -> PropertyM m a
run :: forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run m a
m = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (m a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => m (Gen a) -> Gen (m a)
promote)

-- | Quantification in a monadic property, fits better with
-- /do-notation/ than 'forAllM'.
-- __Note__: values generated by 'pick' do not shrink.
pick :: (Monad m, Show a) => Gen a -> PropertyM m a
pick :: forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick Gen a
gen = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM forall a b. (a -> b) -> a -> b
$ \a -> Gen (m Property)
k ->
  do a
a <- Gen a
gen
     m Property
mp <- a -> Gen (m Property)
k a
a
     forall (m :: * -> *) a. Monad m => a -> m a
return (do Property
p <- m Property
mp
                forall (m :: * -> *) a. Monad m => a -> m a
return (forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall (m :: * -> *) a. Monad m => a -> m a
return a
a) (forall a b. a -> b -> a
const Property
p)))

-- | The <https://en.wikipedia.org/wiki/Predicate_transformer_semantics#Weakest_preconditions weakest precondition>
--
-- > wp(x ← e, p)
--
-- can be expressed as in code as @wp e (\\x -> p)@.
wp :: Monad m => m a -> (a -> PropertyM m b) -> PropertyM m b
wp :: forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> PropertyM m b) -> PropertyM m b
wp m a
m a -> PropertyM m b
k = forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run m a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> PropertyM m b
k

-- | Quantification in monadic properties to 'pick', with a notation similar to
-- 'forAll'. __Note__: values generated by 'forAllM' do not shrink.

forAllM :: (Monad m, Show a) => Gen a -> (a -> PropertyM m b) -> PropertyM m b
forAllM :: forall (m :: * -> *) a b.
(Monad m, Show a) =>
Gen a -> (a -> PropertyM m b) -> PropertyM m b
forAllM Gen a
gen a -> PropertyM m b
k = forall (m :: * -> *) a. (Monad m, Show a) => Gen a -> PropertyM m a
pick Gen a
gen forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> PropertyM m b
k

-- | Allows making observations about the test data:
--
-- @
-- monitor ('collect' e)
-- @
--
-- collects the distribution of value of @e@.
--
-- @
-- monitor ('counterexample' "Failure!")
-- @
--
-- Adds @"Failure!"@ to the counterexamples.
monitor :: Monad m => (Property -> Property) -> PropertyM m ()
monitor :: forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor Property -> Property
f = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (\() -> Gen (m Property)
k -> (Property -> Property
f forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (() -> Gen (m Property)
k ()))

-- run functions

monadic :: (Testable a, Monad m) => (m Property -> Property) -> PropertyM m a -> Property
monadic :: forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic m Property -> Property
runner PropertyM m a
m = forall prop. Testable prop => prop -> Property
property (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m Property -> Property
runner (forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
monadic' PropertyM m a
m))

monadic' :: (Testable a, Monad m) => PropertyM m a -> Gen (m Property)
monadic' :: forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
monadic' (MkPropertyM (a -> Gen (m Property)) -> Gen (m Property)
m) = (a -> Gen (m Property)) -> Gen (m Property)
m (\a
prop -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall (m :: * -> *) a. Monad m => a -> m a
return (forall prop. Testable prop => prop -> Property
property a
prop)))

-- | Runs the property monad for 'IO'-computations.
--
-- @
-- prop_cat msg = monadicIO $ do
--   (exitCode, stdout, _) \<- run ('System.Process.readProcessWithExitCode' "cat" [] msg)
--
--   pre ('System.Exit.ExitSuccess' == exitCode)
--
--   assert (stdout == msg)
-- @
--
-- >>> quickCheck prop_cat
-- +++ OK, passed 100 tests.
--
monadicIO :: Testable a => PropertyM IO a -> Property
monadicIO :: forall a. Testable a => PropertyM IO a -> Property
monadicIO = forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic forall prop. Testable prop => IO prop -> Property
ioProperty

#ifndef NO_ST_MONAD
-- | Runs the property monad for 'ST'-computations.
--
-- @
-- -- Your mutable sorting algorithm here
-- sortST :: Ord a => [a] -> 'Control.Monad.ST.ST' s (MVector s a)
-- sortST = 'Data.Vector.thaw' . 'Data.Vector.fromList' . 'Data.List.sort'
--
-- prop_sortST xs = monadicST $ do
--   sorted  \<- run ('Data.Vector.freeze' =<< sortST xs)
--   assert ('Data.Vector.toList' sorted == sort xs)
-- @
--
-- >>> quickCheck prop_sortST
-- +++ OK, passed 100 tests.
--
monadicST :: Testable a => (forall s. PropertyM (ST s) a) -> Property
monadicST :: forall a. Testable a => (forall s. PropertyM (ST s) a) -> Property
monadicST forall s. PropertyM (ST s) a
m = forall prop. Testable prop => prop -> Property
property (forall a. (forall s. Gen (ST s a)) -> Gen a
runSTGen (forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
monadic' forall s. PropertyM (ST s) a
m))

runSTGen :: (forall s. Gen (ST s a)) -> Gen a
runSTGen :: forall a. (forall s. Gen (ST s a)) -> Gen a
runSTGen forall s. Gen (ST s a)
f = do
  Capture forall a. Gen a -> a
eval <- Gen Capture
capture
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. (forall s. ST s a) -> a
runST (forall a. Gen a -> a
eval forall s. Gen (ST s a)
f))
#endif

--------------------------------------------------------------------------
-- the end.