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

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

{-# OPTIONS_GHC -Wall #-}

module Test.QuickCheck.Classes.Category
  (
#if HAVE_BINARY_LAWS
    categoryLaws
  , commutativeCategoryLaws
#endif
  ) where

import Prelude hiding (id, (.))
import Control.Category (Category(..))
import Test.QuickCheck hiding ((.&.))
#if HAVE_BINARY_LAWS
import Data.Functor.Classes (Eq2,Show2)
#endif
import Test.QuickCheck.Property (Property)

import Test.QuickCheck.Classes.Internal

#if HAVE_BINARY_LAWS

-- | Tests the following 'Category' properties:
--
-- [/Right Identity/]
--   @f '.' 'id' ≡ f@
-- [/Left Identity/]
--   @'id' '.' f ≡ f@
-- [/Associativity/]
--   @f '.' (g '.' h) ≡ (f '.' g) '.' h@
--
-- /Note/: This property test is only available when this package is built with
-- @base-4.9+@ or @transformers-0.5+@.
categoryLaws :: forall proxy c.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Category c, forall a b. (Eq a, Eq b) => Eq (c a b), forall a b. (Show a, Show b) => Show (c a b), forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b))
#else
  (Category c, Eq2 c, Show2 c, Arbitrary2 c)
#endif
  => proxy c -> Laws
categoryLaws :: proxy c -> Laws
categoryLaws proxy c
p = String -> [(String, Property)] -> Laws
Laws String
"Category"
  [ (String
"Right Identity", proxy c -> Property
forall (proxy :: (* -> * -> *) -> *) (c :: * -> * -> *).
(Category c, forall a b. (Eq a, Eq b) => Eq (c a b),
 forall a b. (Show a, Show b) => Show (c a b),
 forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b)) =>
proxy c -> Property
categoryRightIdentity proxy c
p)
  , (String
"Left Identity", proxy c -> Property
forall (proxy :: (* -> * -> *) -> *) (c :: * -> * -> *).
(Category c, forall a b. (Eq a, Eq b) => Eq (c a b),
 forall a b. (Show a, Show b) => Show (c a b),
 forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b)) =>
proxy c -> Property
categoryLeftIdentity proxy c
p)
  , (String
"Associativity", proxy c -> Property
forall (proxy :: (* -> * -> *) -> *) (c :: * -> * -> *).
(Category c, forall a b. (Eq a, Eq b) => Eq (c a b),
 forall a b. (Show a, Show b) => Show (c a b),
 forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b)) =>
proxy c -> Property
categoryAssociativity proxy c
p)
  ]

-- | Test everything from 'categoryLaws' plus the following:
--
-- [/Commutative/]
--   @f '.' g ≡ g '.' f@
--
-- /Note/: This property test is only available when this package is built with
-- @base-4.9+@ or @transformers-0.5+@.
commutativeCategoryLaws :: forall proxy c.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Category c, forall a b. (Eq a, Eq b) => Eq (c a b), forall a b. (Show a, Show b) => Show (c a b), forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b))
#else
  (Category c, Eq2 c, Show2 c, Arbitrary2 c)
#endif
  => proxy c -> Laws
commutativeCategoryLaws :: proxy c -> Laws
commutativeCategoryLaws proxy c
p = String -> [(String, Property)] -> Laws
Laws String
"Commutative Category" ([(String, Property)] -> Laws) -> [(String, Property)] -> Laws
forall a b. (a -> b) -> a -> b
$ Laws -> [(String, Property)]
lawsProperties (proxy c -> Laws
forall (proxy :: (* -> * -> *) -> *) (c :: * -> * -> *).
(Category c, forall a b. (Eq a, Eq b) => Eq (c a b),
 forall a b. (Show a, Show b) => Show (c a b),
 forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b)) =>
proxy c -> Laws
categoryLaws proxy c
p) [(String, Property)]
-> [(String, Property)] -> [(String, Property)]
forall a. [a] -> [a] -> [a]
++
  [ (String
"Commutative", proxy c -> Property
forall (proxy :: (* -> * -> *) -> *) (c :: * -> * -> *).
(Category c, forall a b. (Eq a, Eq b) => Eq (c a b),
 forall a b. (Show a, Show b) => Show (c a b),
 forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b)) =>
proxy c -> Property
categoryCommutativity proxy c
p)
  ]

categoryRightIdentity :: forall proxy c.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Category c, forall a b. (Eq a, Eq b) => Eq (c a b), forall a b. (Show a, Show b) => Show (c a b), forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b))
#else
  (Category c, Eq2 c, Show2 c, Arbitrary2 c)
#endif
  => proxy c -> Property
categoryRightIdentity :: proxy c -> Property
categoryRightIdentity proxy c
_ = (Apply2 c Integer Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply2 c Integer Integer -> Bool) -> Property)
-> (Apply2 c Integer Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Apply2 (c Integer Integer
x :: c Integer Integer)) -> c Integer Integer -> c Integer Integer -> Bool
forall b (f :: * -> * -> *) a.
(forall a1. (Eq a1, Eq b) => Eq (f a1 b), Eq a, Eq b) =>
f a b -> f a b -> Bool
eq2 (c Integer Integer
x c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c Integer Integer
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) c Integer Integer
x

categoryLeftIdentity :: forall proxy c.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Category c, forall a b. (Eq a, Eq b) => Eq (c a b), forall a b. (Show a, Show b) => Show (c a b), forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b))
#else
  (Category c, Eq2 c, Show2 c, Arbitrary2 c)
#endif
  => proxy c -> Property
categoryLeftIdentity :: proxy c -> Property
categoryLeftIdentity proxy c
_ = (Apply2 c Integer Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply2 c Integer Integer -> Bool) -> Property)
-> (Apply2 c Integer Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Apply2 (c Integer Integer
x :: c Integer Integer)) -> c Integer Integer -> c Integer Integer -> Bool
forall b (f :: * -> * -> *) a.
(forall a1. (Eq a1, Eq b) => Eq (f a1 b), Eq a, Eq b) =>
f a b -> f a b -> Bool
eq2 (c Integer Integer
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c Integer Integer
x) c Integer Integer
x

categoryAssociativity :: forall proxy c.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Category c, forall a b. (Eq a, Eq b) => Eq (c a b), forall a b. (Show a, Show b) => Show (c a b), forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b))
#else
  (Category c, Eq2 c, Show2 c, Arbitrary2 c)
#endif
  => proxy c -> Property
categoryAssociativity :: proxy c -> Property
categoryAssociativity proxy c
_ = (Apply2 c Integer Integer
 -> Apply2 c Integer Integer -> Apply2 c Integer Integer -> Bool)
-> Property
forall prop. Testable prop => prop -> Property
property ((Apply2 c Integer Integer
  -> Apply2 c Integer Integer -> Apply2 c Integer Integer -> Bool)
 -> Property)
-> (Apply2 c Integer Integer
    -> Apply2 c Integer Integer -> Apply2 c Integer Integer -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(Apply2 (c Integer Integer
f :: c Integer Integer)) (Apply2 (c Integer Integer
g :: c Integer Integer)) (Apply2 (c Integer Integer
h :: c Integer Integer)) -> c Integer Integer -> c Integer Integer -> Bool
forall b (f :: * -> * -> *) a.
(forall a1. (Eq a1, Eq b) => Eq (f a1 b), Eq a, Eq b) =>
f a b -> f a b -> Bool
eq2 (c Integer Integer
f c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (c Integer Integer
g c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c Integer Integer
h)) ((c Integer Integer
f c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c Integer Integer
g) c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c Integer Integer
h)

categoryCommutativity :: forall proxy c.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Category c, forall a b. (Eq a, Eq b) => Eq (c a b), forall a b. (Show a, Show b) => Show (c a b), forall a b. (Arbitrary a, Arbitrary b) => Arbitrary (c a b))
#else
  (Category c, Eq2 c, Show2 c, Arbitrary2 c)
#endif
  => proxy c -> Property
categoryCommutativity :: proxy c -> Property
categoryCommutativity proxy c
_ = (Apply2 c Integer Integer -> Apply2 c Integer Integer -> Bool)
-> Property
forall prop. Testable prop => prop -> Property
property ((Apply2 c Integer Integer -> Apply2 c Integer Integer -> Bool)
 -> Property)
-> (Apply2 c Integer Integer -> Apply2 c Integer Integer -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(Apply2 (c Integer Integer
f :: c Integer Integer)) (Apply2 (c Integer Integer
g :: c Integer Integer)) -> c Integer Integer -> c Integer Integer -> Bool
forall b (f :: * -> * -> *) a.
(forall a1. (Eq a1, Eq b) => Eq (f a1 b), Eq a, Eq b) =>
f a b -> f a b -> Bool
eq2 (c Integer Integer
f c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c Integer Integer
g) (c Integer Integer
g c Integer Integer -> c Integer Integer -> c Integer Integer
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c Integer Integer
f)

#endif