{-# 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
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)
]
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