{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}

module Hedgehog.Classes.Category (categoryLaws, commutativeCategoryLaws) where

import Hedgehog
import Hedgehog.Classes.Common

import Control.Category(Category(..))
import Prelude hiding (id, (.))

-- | Tests the following 'Category' laws:
--
-- [__Left Identity__]: @'id' '.' f@ ≡ @f@
-- [__Right Identity__]: @f '.' 'id'@ ≡ @f@
-- [__Associativity__]: @f '.' (g '.' h)@ ≡ @(f '.' g) '.' h@
categoryLaws :: forall f.
  ( Category f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
categoryLaws :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
categoryLaws forall x y. Gen x -> Gen y -> Gen (f x y)
gen = String -> [(String, Property)] -> Laws
Laws String
"Category"
  [ (String
"Left Identity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryLeftIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Right Identity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryRightIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Associativity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryAssociativity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  ]

-- | Tests the following 'Category' laws:
--
-- [__Commutativity__]: @f '.' g@ ≡ @g '.' f@
commutativeCategoryLaws :: forall f.
  ( Category f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
commutativeCategoryLaws :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
commutativeCategoryLaws forall x y. Gen x -> Gen y -> Gen (f x y)
gen = String -> [(String, Property)] -> Laws
Laws String
"Commutative Category"
  [ (String
"Commutativity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryCommutativity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  ]

categoryRightIdentity :: forall f.
  ( Category f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryRightIdentity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryRightIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer Integer
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  (f Integer Integer
x forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f Integer Integer
x

categoryLeftIdentity :: forall f.
  ( Category f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryLeftIdentity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryLeftIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer Integer
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  (forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
x) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f Integer Integer
x

categoryAssociativity :: forall f.
  ( Category f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryAssociativity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryAssociativity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  f Integer Integer
g <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger 
  f Integer Integer
h <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger 
  (f Integer Integer
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f Integer Integer
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
h)) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` ((f Integer Integer
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
g) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
h)

categoryCommutativity :: forall f.
  ( Category f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryCommutativity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryCommutativity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  f Integer Integer
g <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  (f Integer Integer
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
g) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` (f Integer Integer
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
f)