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

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

{-# OPTIONS_GHC -Wall #-}

module Test.QuickCheck.Classes.Monad
  (
#if HAVE_UNARY_LAWS
    monadLaws
#endif
  ) where

import Control.Applicative
import Test.QuickCheck hiding ((.&.))
import Control.Monad (ap)
#if HAVE_UNARY_LAWS
import Test.QuickCheck.Arbitrary (Arbitrary1(..))
import Data.Functor.Classes (Eq1,Show1)
#endif
import Test.QuickCheck.Property (Property)

import Test.QuickCheck.Classes.Internal

#if HAVE_UNARY_LAWS

-- | Tests the following monadic properties:
--
-- [/Left Identity/]
--   @'return' a '>>=' k ≡ k a@
-- [/Right Identity/]
--   @m '>>=' 'return' ≡ m@
-- [/Associativity/]
--   @m '>>=' (\\x -> k x '>>=' h) ≡ (m '>>=' k) '>>=' h@
-- [/Return/]
--   @'pure' ≡ 'return'@
-- [/Ap/]
--   @('<*>') ≡ 'ap'@
monadLaws ::
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Monad f, Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Monad f, Applicative f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Laws
monadLaws :: proxy f -> Laws
monadLaws proxy f
p = String -> [(String, Property)] -> Laws
Laws String
"Monad"
  [ (String
"Left Identity", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Monad f, Functor 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
monadLeftIdentity proxy f
p)
  , (String
"Right Identity", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Monad 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
monadRightIdentity proxy f
p)
  , (String
"Associativity", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Monad f, Functor 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
monadAssociativity proxy f
p)
  , (String
"Return", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Monad f, Applicative 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
monadReturn proxy f
p)
  , (String
"Ap", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Monad f, Applicative 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
monadAp proxy f
p)
  ]

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

monadRightIdentity :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Monad f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Monad f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadRightIdentity :: proxy f -> Property
monadRightIdentity 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
m :: 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
m f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
forall (m :: * -> *) a. Monad m => a -> m a
return) f Integer
m

monadAssociativity :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Monad f, Functor f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Monad f, Functor f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadAssociativity :: proxy f -> Property
monadAssociativity proxy f
_ = (Apply f Integer -> LinearEquationM f -> LinearEquationM f -> Bool)
-> Property
forall prop. Testable prop => prop -> Property
property ((Apply f Integer
  -> LinearEquationM f -> LinearEquationM f -> Bool)
 -> Property)
-> (Apply f Integer
    -> LinearEquationM f -> LinearEquationM f -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f Integer
m :: f Integer)) (LinearEquationM f
k' :: LinearEquationM f) (LinearEquationM f
h' :: LinearEquationM f) ->
  let k :: Integer -> f Integer
k = LinearEquationM f -> Integer -> f Integer
forall (m :: * -> *).
Monad m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
k'
      h :: Integer -> f Integer
h = LinearEquationM f -> Integer -> f Integer
forall (m :: * -> *).
Monad m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
h'
   in 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
m f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Integer
x -> Integer -> f Integer
k Integer
x f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
h)) ((f Integer
m f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
k) f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
h)

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

monadAp :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Monad f, Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Monad f, Applicative f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
monadAp :: proxy f -> Property
monadAp proxy f
_ = (Apply f QuadraticEquation -> Apply f Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply f QuadraticEquation -> Apply f Integer -> Bool)
 -> Property)
-> (Apply f QuadraticEquation -> Apply f Integer -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f QuadraticEquation
f' :: f QuadraticEquation)) (Apply (f Integer
x :: f Integer)) ->
  let f :: f (Integer -> Integer)
f = (QuadraticEquation -> Integer -> Integer)
-> f QuadraticEquation -> f (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QuadraticEquation -> Integer -> Integer
runQuadraticEquation f QuadraticEquation
f'
   in 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 -> Integer) -> f Integer -> f Integer
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap f (Integer -> Integer)
f f Integer
x) (f (Integer -> Integer)
f f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
x)

#endif