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

module Hedgehog.Classes.Bifunctor (bifunctorLaws) where

import Hedgehog
import Hedgehog.Classes.Common

import Data.Bifunctor (Bifunctor(..))

-- | Tests the following 'Bifunctor' laws:
--
-- [__Identity__]: @'bimap' 'id' 'id'@ ≡ @'id'@
-- [__First Identity__]: @'first' 'id'@ ≡ @'id'@
-- [__Second Identity__]: @'second' 'id'@ ≡ @'id'@
-- [__Composition__]: @'bimap' 'id' 'id'@ ≡ @'first' 'id' '.' 'second' 'id'@
bifunctorLaws :: forall f.
  ( Bifunctor 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
bifunctorLaws :: forall (f :: * -> * -> *).
(Bifunctor 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
bifunctorLaws forall x y. Gen x -> Gen y -> Gen (f x y)
gen = String -> [(String, Property)] -> Laws
Laws String
"Bifunctor"
  [ (String
"Identity", forall (f :: * -> * -> *). BifunctorProp f
bifunctorIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"First Identity", forall (f :: * -> * -> *). BifunctorProp f
bifunctorFirstIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Second Identity", forall (f :: * -> * -> *). BifunctorProp f
bifunctorSecondIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Composition", forall (f :: * -> * -> *). BifunctorProp f
bifunctorComposition forall x y. Gen x -> Gen y -> Gen (f x y)
gen) 
  ]

type BifunctorProp f =
  ( Bifunctor 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

bifunctorIdentity :: forall f. BifunctorProp f
bifunctorIdentity :: forall (f :: * -> * -> *). BifunctorProp f
bifunctorIdentity 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
  let lhs :: f Integer Integer
lhs = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a. a -> a
id forall a. a -> a
id f Integer Integer
x
  let rhs :: f Integer Integer
rhs = f Integer Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Identity", lawContextLawBody :: String
lawContextLawBody = String
"bimap id id" String -> String -> String
`congruency` String
"id"
        , lawContextTcName :: String
lawContextTcName = String
"Bifunctor", lawContextTcProp :: String
lawContextTcProp =
             let showX :: String
showX = forall a. Show a => a -> String
show f Integer Integer
x;
             in [String] -> String
lawWhere
                 [ String
"bimap id id x" String -> String -> String
`congruency` String
"x, where"
                 , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer Integer
lhs f Integer Integer
rhs 
        } 
  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 -> Context -> m ()
heqCtx2 f Integer Integer
lhs f Integer Integer
rhs Context
ctx 

bifunctorFirstIdentity :: forall f. BifunctorProp f
bifunctorFirstIdentity :: forall (f :: * -> * -> *). BifunctorProp f
bifunctorFirstIdentity 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
  let lhs :: f Integer Integer
lhs = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. a -> a
id f Integer Integer
x
  let rhs :: f Integer Integer
rhs = f Integer Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"First Identity", lawContextLawBody :: String
lawContextLawBody = String
"first id" String -> String -> String
`congruency` String
"id"
        , lawContextTcName :: String
lawContextTcName = String
"Bifunctor", lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = forall a. Show a => a -> String
show f Integer Integer
x;
            in [String] -> String
lawWhere
              [ String
"first id x" String -> String -> String
`congruency` String
"x, where"
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer Integer
lhs f Integer Integer
rhs 
        }
  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 -> Context -> m ()
heqCtx2 f Integer Integer
lhs f Integer Integer
rhs Context
ctx

bifunctorSecondIdentity :: forall f. BifunctorProp f
bifunctorSecondIdentity :: forall (f :: * -> * -> *). BifunctorProp f
bifunctorSecondIdentity 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
  let lhs :: f Integer Integer
lhs = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. a -> a
id f Integer Integer
x
  let rhs :: f Integer Integer
rhs = f Integer Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Second Identity", lawContextLawBody :: String
lawContextLawBody = String
"second id" String -> String -> String
`congruency` String
"id"
        , lawContextTcName :: String
lawContextTcName = String
"Bifunctor", lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = forall a. Show a => a -> String
show f Integer Integer
x;
            in [String] -> String
lawWhere
              [ String
"second id x" String -> String -> String
`congruency` String
"x, where"
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer Integer
lhs f Integer Integer
rhs 
        }
  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 -> Context -> m ()
heqCtx2 f Integer Integer
lhs f Integer Integer
rhs Context
ctx

bifunctorComposition :: forall f. BifunctorProp f
bifunctorComposition :: forall (f :: * -> * -> *). BifunctorProp f
bifunctorComposition 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
z <- 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
  let lhs :: f Integer Integer
lhs = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall a. a -> a
id forall a. a -> a
id f Integer Integer
z
  let rhs :: f Integer Integer
rhs = (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. a -> a
id) f Integer Integer
z
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Composition", lawContextLawBody :: String
lawContextLawBody = String
"bimap id id" String -> String -> String
`congruency` String
"first id . second id"
        , lawContextTcName :: String
lawContextTcName = String
"Bifunctor", lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = forall a. Show a => a -> String
show f Integer Integer
z;
            in [String] -> String
lawWhere
              [ String
"bimap id id x" String -> String -> String
`congruency` String
"first id . second id $ x, where"
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer Integer
lhs f Integer Integer
rhs 
        }       
  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 -> Context -> m ()
heqCtx2 f Integer Integer
lhs f Integer Integer
rhs Context
ctx