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