{-# 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 x y. Gen x -> Gen y -> Gen (f x y)) -> Property
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 Gen x -> Gen y -> Gen (f x y)
forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Right Identity", (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
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 Gen x -> Gen y -> Gen (f x y)
forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Associativity", (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
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 Gen x -> Gen y -> Gen (f x y)
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 x y. Gen x -> Gen y -> Gen (f x y)) -> Property
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 Gen x -> Gen y -> Gen (f x y)
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
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  x <- Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f Integer Integer) -> PropertyT IO (f Integer Integer))
-> Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall a b. (a -> b) -> a -> b
$ Gen Integer -> Gen Integer -> Gen (f Integer Integer)
forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  (x . id) `heq2` 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
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  x <- Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f Integer Integer) -> PropertyT IO (f Integer Integer))
-> Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall a b. (a -> b) -> a -> b
$ Gen Integer -> Gen Integer -> Gen (f Integer Integer)
forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  (id . x) `heq2` 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
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  f <- Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f Integer Integer) -> PropertyT IO (f Integer Integer))
-> Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall a b. (a -> b) -> a -> b
$ Gen Integer -> Gen Integer -> Gen (f Integer Integer)
forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  g <- forAll $ fgen genSmallInteger genSmallInteger 
  h <- forAll $ fgen genSmallInteger genSmallInteger 
  (f . (g . h)) `heq2` ((f . g) . 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
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  f <- Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f Integer Integer) -> PropertyT IO (f Integer Integer))
-> Gen (f Integer Integer) -> PropertyT IO (f Integer Integer)
forall a b. (a -> b) -> a -> b
$ Gen Integer -> Gen Integer -> Gen (f Integer Integer)
forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  g <- forAll $ fgen genSmallInteger genSmallInteger
  (f . g) `heq2` (g . f)