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

module Hedgehog.Classes.MonadIO (monadIOLaws) where

import Control.Monad.IO.Class (MonadIO(..))

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'MonadIO' laws:
--
-- [__Return__]: @'liftIO' '.' 'return'@ ≡ @'return'@
-- [__Lift__]: @'liftIO' (m '>>=' f)@ ≡ @'liftIO' m '>>=' ('liftIO' '.' f)@
monadIOLaws ::
  ( MonadIO f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Laws
monadIOLaws :: forall (f :: * -> *).
(MonadIO f, forall x. Eq x => Eq (f x),
 forall x. Show x => Show (f x)) =>
(forall x. Gen x -> Gen (f x)) -> Laws
monadIOLaws forall x. Gen x -> Gen (f x)
gen = String -> [(String, Property)] -> Laws
Laws String
"MonadIO"
  [ (String
"Return", forall (f :: * -> *). MonadIOProp f
monadIOReturn forall x. Gen x -> Gen (f x)
gen)
  , (String
"Lift", forall (f :: * -> *). MonadIOProp f
monadIOLift forall x. Gen x -> Gen (f x)
gen)
  ]

type MonadIOProp f =
  ( MonadIO f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Property

monadIOReturn :: forall f. MonadIOProp f
monadIOReturn :: forall (f :: * -> *). MonadIOProp f
monadIOReturn forall x. Gen x -> Gen (f x)
_fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  Integer
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Integer
genSmallInteger
  let lhs :: f Integer
lhs = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x)
  let rhs :: f Integer
rhs = forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x :: f Integer
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Return", lawContextTcName :: String
lawContextTcName = String
"MonadIO"
        , lawContextLawBody :: String
lawContextLawBody = String
"liftIO . return" String -> String -> String
`congruency` String
"return"
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = forall a. Show a => a -> String
show Integer
x
            in [String] -> String
lawWhere
              [ String
"liftIO . return $ x" String -> String -> String
`congruency` String
"return x, where"
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        }
  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
lhs f Integer
rhs Context
ctx

monadIOLift :: forall f. MonadIOProp f
monadIOLift :: forall (f :: * -> *). MonadIOProp f
monadIOLift forall x. Gen x -> Gen (f x)
_fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  IO Integer
m <- forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith forall a. Show a => IO a -> String
showIO forall a b. (a -> b) -> a -> b
$ forall a. Gen a -> Gen (IO a)
genIO Gen Integer
genSmallInteger
  LinearEquation
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen LinearEquation
genLinearEquation
  let f :: Integer -> IO Integer
f = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. LinearEquation -> Integer -> Integer
runLinearEquation LinearEquation
f'
  let lhs :: f Integer
lhs = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Integer
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> IO Integer
f) :: f Integer
  let rhs :: f Integer
rhs = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO Integer
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> IO Integer
f) :: f Integer
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Lift", lawContextTcName :: String
lawContextTcName = String
"MonadIO"
        , lawContextLawBody :: String
lawContextLawBody = String
"liftIO (m >>= f)" String -> String -> String
`congruency` String
"liftIO m >>= (liftIO . f)"
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showM :: String
showM = forall a. Show a => IO a -> String
showIO IO Integer
m
                showF :: String
showF = forall a. Show a => a -> String
show LinearEquation
f'
            in [String] -> String
lawWhere
              [ String
"liftIO (m >>= f)" String -> String -> String
`congruency` String
"liftIO m >>= (liftIO . f), where"
              , String
"f = " forall a. [a] -> [a] -> [a]
++ String
showF
              , String
"m = " forall a. [a] -> [a] -> [a]
++ String
showM
              ]
        }
  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
lhs f Integer
rhs Context
ctx