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

module Hedgehog.Classes.Bitraversable (bitraversableLaws) where

import Hedgehog
import Hedgehog.Classes.Common

import Data.Bitraversable (Bitraversable(..))
import Data.Functor.Compose (Compose(..))
import Data.Functor.Identity (Identity(..))

import qualified Data.Set as S
import qualified Control.Monad.Trans.Writer.Lazy as WL

-- | Tests the following 'Bitraversable' laws:
--
-- [__Naturality__]: @'bitraverse' (t '.' f) (t '.' g)@ ≡ @t '.' 'bitraverse' f g, for every applicative transformation t@
-- [__Identity__]: @'bitraverse' 'Identity' 'Identity'@ ≡ @'Identity'@
-- [__Composition__]: @'Compose' '.' 'fmap' ('bitraverse' g1 g2) '.' 'bitraverse' f1 f2@ ≡ @'bitraverse' ('Compose' '.' 'fmap' g1 '.' f1) ('Compose' '.' 'fmap' g2 '.' f2)@
bitraversableLaws :: forall f.
  ( Bitraversable 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
bitraversableLaws :: forall (f :: * -> * -> *).
(Bitraversable 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
bitraversableLaws forall x y. Gen x -> Gen y -> Gen (f x y)
gen = String -> [(String, Property)] -> Laws
Laws String
"Bitraversable"
  [ (String
"Naturality", forall (f :: * -> * -> *). BitraversableProp f
bitraversableNaturality forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Identity", forall (f :: * -> * -> *). BitraversableProp f
bitraversableIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Composition", forall (f :: * -> * -> *). BitraversableProp f
bitraversableComposition forall x y. Gen x -> Gen y -> Gen (f x y)
gen) 
  ]

type BitraversableProp f =
  ( Bitraversable 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

bitraversableNaturality :: forall f. BitraversableProp f
bitraversableNaturality :: forall (f :: * -> * -> *). BitraversableProp f
bitraversableNaturality 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 t :: Compose Triple (Writer (Set Integer)) a
-> Compose (Writer (Set Integer)) Triple a
t = forall a.
Compose Triple (Writer (Set Integer)) a
-> Compose (Writer (Set Integer)) Triple a
apTrans; f :: Integer -> Compose Triple (Writer (Set Integer)) Integer
f = Integer -> Compose Triple (Writer (Set Integer)) Integer
func4; g :: Integer -> Compose Triple (Writer (Set Integer)) Integer
g = Integer -> Compose Triple (Writer (Set Integer)) Integer
func4
  let lhs :: Compose (Writer (Set Integer)) Triple (f Integer Integer)
lhs = forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse (forall a.
Compose Triple (Writer (Set Integer)) a
-> Compose (Writer (Set Integer)) Triple a
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Compose Triple (Writer (Set Integer)) Integer
f) (forall a.
Compose Triple (Writer (Set Integer)) a
-> Compose (Writer (Set Integer)) Triple a
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Compose Triple (Writer (Set Integer)) Integer
g) f Integer Integer
x
  let rhs :: Compose (Writer (Set Integer)) Triple (f Integer Integer)
rhs = forall a.
Compose Triple (Writer (Set Integer)) a
-> Compose (Writer (Set Integer)) Triple a
t (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse Integer -> Compose Triple (Writer (Set Integer)) Integer
f Integer -> Compose Triple (Writer (Set Integer)) Integer
g f Integer Integer
x)
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Naturality", lawContextLawBody :: String
lawContextLawBody = String
"bitraverse (t . f) (t . g)" String -> String -> String
`congruency` String
"t . bitraverse f g, for every applicative transformation t"
        , lawContextTcName :: String
lawContextTcName = String
"Bitraversable", lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = forall a. Show a => a -> String
show f Integer Integer
x;
            in [String] -> String
lawWhere
                 [ String
"bitraverse (t . f) (t . g) $ x" String -> String -> String
`congruency` String
"t . bitraverse f g $ x, for every applicative transformation t, where"
                 , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Compose (Writer (Set Integer)) Triple (f Integer Integer)
lhs Compose (Writer (Set Integer)) Triple (f Integer Integer)
rhs 
        }
  forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
 forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 Compose (Writer (Set Integer)) Triple (f Integer Integer)
lhs Compose (Writer (Set Integer)) Triple (f Integer Integer)
rhs Context
ctx  

bitraversableIdentity :: forall f. BitraversableProp f
bitraversableIdentity :: forall (f :: * -> * -> *). BitraversableProp f
bitraversableIdentity 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 :: Identity (f Integer Integer)
lhs = forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall a. a -> Identity a
Identity forall a. a -> Identity a
Identity f Integer Integer
x
  let rhs :: Identity (f Integer Integer)
rhs = forall a. a -> Identity a
Identity 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
"bitraverse Identity Identity" String -> String -> String
`congruency` String
"Identity"
        , lawContextTcName :: String
lawContextTcName = String
"Bitraversable", lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = forall a. Show a => a -> String
show f Integer Integer
x;
            in [String] -> String
lawWhere
                 [ String
"bitraverse Identity Identity x" String -> String -> String
`congruency` String
"Identity x, where"
                 , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Identity (f Integer Integer)
lhs Identity (f Integer Integer)
rhs 
        }
  forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
 forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 Identity (f Integer Integer)
lhs Identity (f Integer Integer)
rhs Context
ctx  
  
bitraversableComposition :: forall f. BitraversableProp f
bitraversableComposition :: forall (f :: * -> * -> *). BitraversableProp f
bitraversableComposition 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 f1 :: Integer -> Triple Integer
f1 = Integer -> Triple Integer
func6; f2 :: Integer -> Triple Integer
f2 = Integer -> Triple Integer
func5; g1 :: Integer -> Compose Triple (Writer (Set Integer)) Integer
g1 = Integer -> Compose Triple (Writer (Set Integer)) Integer
func4; g2 :: Integer -> Compose Triple (Writer (Set Integer)) Integer
g2 = Integer -> Compose Triple (Writer (Set Integer)) Integer
func4
  let lhs :: Compose Triple (Compose Triple (WL.Writer (S.Set Integer))) (f Integer Integer)
      lhs :: Compose
  Triple (Compose Triple (Writer (Set Integer))) (f Integer Integer)
lhs = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse Integer -> Compose Triple (Writer (Set Integer)) Integer
g1 Integer -> Compose Triple (Writer (Set Integer)) Integer
g2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse Integer -> Triple Integer
f1 Integer -> Triple Integer
f2 forall a b. (a -> b) -> a -> b
$ f Integer Integer
x
      
  let rhs :: Compose Triple (Compose Triple (WL.Writer (S.Set Integer))) (f Integer Integer)
      rhs :: Compose
  Triple (Compose Triple (Writer (Set Integer))) (f Integer Integer)
rhs = forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Compose Triple (Writer (Set Integer)) Integer
g1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Triple Integer
f1) (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Compose Triple (Writer (Set Integer)) Integer
g2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Triple Integer
f2) f Integer Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Composition", lawContextLawBody :: String
lawContextLawBody = String
"Compose . fmap (bitraverse g1 g2) . bitraverse f1 f2" String -> String -> String
`congruency` String
"bitraverse (Compose . fmap g1 . f1) (Compose . fmap g2 . f2)"
        , lawContextTcName :: String
lawContextTcName = String
"Bitraversable", lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = forall a. Show a => a -> String
show f Integer Integer
x;  
            in [String] -> String
lawWhere
                 [ String
"Compose . fmap (bitraverse g1 g2) . bitraverse f1 f2 $ x" String -> String -> String
`congruency` String
"bitraverse (Compose . fmap g1 . f1) (Compose . fmap g2 . f2) $ x, where"
                 , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Compose
  Triple (Compose Triple (Writer (Set Integer))) (f Integer Integer)
lhs Compose
  Triple (Compose Triple (Writer (Set Integer))) (f Integer Integer)
rhs 
        }
  forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
 forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 Compose
  Triple (Compose Triple (Writer (Set Integer))) (f Integer Integer)
lhs Compose
  Triple (Compose Triple (Writer (Set Integer))) (f Integer Integer)
rhs Context
ctx