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

module Hedgehog.Classes.MonadZip (monadZipLaws) where

import Control.Arrow (Arrow(..))
import Control.Monad.Zip (MonadZip(mzip))

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'MonadZip' laws:
--
-- [__Naturality__]: @'fmap' (f '***' g) ('mzip' ma mb)@ ≡ @'mzip' ('fmap' f ma) ('fmap' g mb)@
monadZipLaws ::
  ( MonadZip f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Laws
monadZipLaws :: forall (f :: * -> *).
(MonadZip f, forall x. Eq x => Eq (f x),
 forall x. Show x => Show (f x)) =>
(forall x. Gen x -> Gen (f x)) -> Laws
monadZipLaws forall x. Gen x -> Gen (f x)
gen = String -> [(String, Property)] -> Laws
Laws String
"Monad"
  [ (String
"Naturality", forall (f :: * -> *). MonadZipProp f
monadZipNaturality forall x. Gen x -> Gen (f x)
gen)
  ]

type MonadZipProp f =
  ( MonadZip f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Property

monadZipNaturality :: forall f. MonadZipProp f
monadZipNaturality :: forall (f :: * -> *). MonadZipProp f
monadZipNaturality forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  LinearEquation
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen LinearEquation
genLinearEquation
  LinearEquation
g' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen LinearEquation
genLinearEquation
  let f :: Integer -> Integer
f = LinearEquation -> Integer -> Integer
runLinearEquation LinearEquation
f'
      g :: Integer -> Integer
g = LinearEquation -> Integer -> Integer
runLinearEquation LinearEquation
g'
  f Integer
ma <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  f Integer
mb <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  let lhs :: f (Integer, Integer)
lhs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer
f forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Integer -> Integer
g) (forall (m :: * -> *) a b. MonadZip m => m a -> m b -> m (a, b)
mzip f Integer
ma f Integer
mb)
  let rhs :: f (Integer, Integer)
rhs = forall (m :: * -> *) a b. MonadZip m => m a -> m b -> m (a, b)
mzip (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f f Integer
ma) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
g f Integer
mb)
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Naturality", lawContextTcName :: String
lawContextTcName = String
"MonadZip"
        , lawContextLawBody :: String
lawContextLawBody = String
"(fmap (f *** g) (mzip ma mb)" String -> String -> String
`congruency` String
"mzip (fmap f ma) (fmap g mb)"
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f (Integer, Integer)
lhs f (Integer, Integer)
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showF :: String
showF = forall a. Show a => a -> String
show LinearEquation
f'; showG :: String
showG = forall a. Show a => a -> String
show LinearEquation
g'; showMA :: String
showMA = forall a. Show a => a -> String
show f Integer
ma; showMB :: String
showMB = forall a. Show a => a -> String
show f Integer
mb;
            in [String] -> String
lawWhere
              [ String
"fmap (f *** g) (mzip ma mb)" String -> String -> String
`congruency` String
"mzip (fmap f ma) (fmap g mb), where"
              , String
"f = " forall a. [a] -> [a] -> [a]
++ String
showF
              , String
"g = " forall a. [a] -> [a] -> [a]
++ String
showG
              , String
"ma = " forall a. [a] -> [a] -> [a]
++ String
showMA  
              , String
"mb = " forall a. [a] -> [a] -> [a]
++ String
showMB
              ]
        }
  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 f (Integer, Integer)
lhs f (Integer, Integer)
rhs Context
ctx