{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}

#if HAVE_QUANTIFIED_CONSTRAINTS
{-# LANGUAGE QuantifiedConstraints #-}
#endif

{-# OPTIONS_GHC -Wall #-}

module Test.QuickCheck.Classes.MonadPlus
  (
#if HAVE_UNARY_LAWS
    monadPlusLaws
#endif
  ) where

import Test.QuickCheck hiding ((.&.))
import Test.QuickCheck.Property (Property)
import Test.QuickCheck.Classes.Internal
import Control.Monad (MonadPlus(mzero,mplus))

#if HAVE_UNARY_LAWS
import Test.QuickCheck.Arbitrary (Arbitrary1(..))
import Data.Functor.Classes (Eq1,Show1)
#endif

#if HAVE_UNARY_LAWS

-- | Tests the following monad plus properties:
--
-- [/Left Identity/]
--   @'mplus' 'mzero' x ≡ x@
-- [/Right Identity/]
--   @'mplus' x 'mzero' ≡ x@
-- [/Associativity/]
--   @'mplus' a ('mplus' b c) ≡ 'mplus' ('mplus' a b) c)@ 
-- [/Left Zero/]
--   @'mzero' '>>=' f ≡ 'mzero'@
-- [/Right Zero/]
--   @m '>>' 'mzero' ≡ 'mzero'@
monadPlusLaws ::
#if HAVE_QUANTIFIED_CONSTRAINTS
  (MonadPlus f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (MonadPlus f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Laws
monadPlusLaws :: proxy f -> Laws
monadPlusLaws proxy f
p = String -> [(String, Property)] -> Laws
Laws String
"MonadPlus"
  [ (String
"Left Identity", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(MonadPlus f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
monadPlusLeftIdentity proxy f
p)
  , (String
"Right Identity", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(MonadPlus f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
monadPlusRightIdentity proxy f
p)
  , (String
"Associativity", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(MonadPlus f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
monadPlusAssociativity proxy f
p)
  , (String
"Left Zero", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(MonadPlus f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
monadPlusLeftZero proxy f
p)
  , (String
"Right Zero", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(MonadPlus f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
monadPlusRightZero proxy f
p)
  ]

monadPlusLeftIdentity :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (MonadPlus f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (MonadPlus f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadPlusLeftIdentity :: proxy f -> Property
monadPlusLeftIdentity proxy f
_ = (Apply f Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply f Integer -> Bool) -> Property)
-> (Apply f Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f Integer
a :: f Integer)) -> f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (f Integer -> f Integer -> f Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
forall (m :: * -> *) a. MonadPlus m => m a
mzero f Integer
a) f Integer
a

monadPlusRightIdentity :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (MonadPlus f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (MonadPlus f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadPlusRightIdentity :: proxy f -> Property
monadPlusRightIdentity proxy f
_ = (Apply f Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply f Integer -> Bool) -> Property)
-> (Apply f Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f Integer
a :: f Integer)) -> f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (f Integer -> f Integer -> f Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
a f Integer
forall (m :: * -> *) a. MonadPlus m => m a
mzero) f Integer
a

monadPlusAssociativity :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (MonadPlus f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (MonadPlus f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadPlusAssociativity :: proxy f -> Property
monadPlusAssociativity proxy f
_ = (Apply f Integer -> Apply f Integer -> Apply f Integer -> Bool)
-> Property
forall prop. Testable prop => prop -> Property
property ((Apply f Integer -> Apply f Integer -> Apply f Integer -> Bool)
 -> Property)
-> (Apply f Integer -> Apply f Integer -> Apply f Integer -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f Integer
a :: f Integer)) (Apply (f Integer
b :: f Integer)) (Apply (f Integer
c :: f Integer)) -> f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (f Integer -> f Integer -> f Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
a (f Integer -> f Integer -> f Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
b f Integer
c)) (f Integer -> f Integer -> f Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (f Integer -> f Integer -> f Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
a f Integer
b) f Integer
c)

monadPlusLeftZero :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (MonadPlus f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (MonadPlus f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadPlusLeftZero :: proxy f -> Property
monadPlusLeftZero proxy f
_ = (LinearEquationM f -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((LinearEquationM f -> Bool) -> Property)
-> (LinearEquationM f -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(LinearEquationM f
k' :: LinearEquationM f) -> f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (f Integer
forall (m :: * -> *) a. MonadPlus m => m a
mzero f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LinearEquationM f -> Integer -> f Integer
forall (m :: * -> *).
Monad m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
k') f Integer
forall (m :: * -> *) a. MonadPlus m => m a
mzero

monadPlusRightZero :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (MonadPlus f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (MonadPlus f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadPlusRightZero :: proxy f -> Property
monadPlusRightZero proxy f
_ = (Apply f Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply f Integer -> Bool) -> Property)
-> (Apply f Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f Integer
a :: f Integer)) -> f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (f Integer
a f Integer -> f Integer -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (f Integer
forall (m :: * -> *) a. MonadPlus m => m a
mzero :: f Integer)) f Integer
forall (m :: * -> *) a. MonadPlus m => m a
mzero

#endif