{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
module Hedgehog.Classes.MonadIO (monadIOLaws) where
import Control.Monad.IO.Class (MonadIO(..))
import Hedgehog
import Hedgehog.Classes.Common
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 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 x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). MonadIOProp f
monadIOReturn forall x. Gen x -> Gen (f x)
gen)
, (String
"Lift", (forall x. Gen x -> Gen (f x)) -> Property
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 x. Gen x -> Gen (f x)) -> Property
monadIOReturn forall x. Gen x -> Gen (f x)
_fgen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
Integer
x <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Integer
genSmallInteger
let lhs :: f Integer
lhs = IO Integer -> f Integer
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x)
let rhs :: f Integer
rhs = Integer -> f Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x :: f Integer
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
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 = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = Integer -> String
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
]
}
f Integer -> f Integer -> Context -> PropertyT IO ()
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 x. Gen x -> Gen (f x)) -> Property
monadIOLift forall x. Gen x -> Gen (f x)
_fgen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
IO Integer
m <- (IO Integer -> String)
-> Gen (IO Integer) -> PropertyT IO (IO Integer)
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith IO Integer -> String
forall a. Show a => IO a -> String
showIO (Gen (IO Integer) -> PropertyT IO (IO Integer))
-> Gen (IO Integer) -> PropertyT IO (IO Integer)
forall a b. (a -> b) -> a -> b
$ Gen Integer -> Gen (IO Integer)
forall a. Gen a -> Gen (IO a)
genIO Gen Integer
genSmallInteger
LinearEquation
f' <- Gen LinearEquation -> PropertyT IO LinearEquation
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen LinearEquation
genLinearEquation
let f :: Integer -> IO Integer
f = Integer -> IO Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> IO Integer)
-> (Integer -> Integer) -> Integer -> IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LinearEquation -> Integer -> Integer
runLinearEquation LinearEquation
f'
let lhs :: f Integer
lhs = IO Integer -> f Integer
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Integer
m IO Integer -> (Integer -> IO Integer) -> IO Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> IO Integer
f) :: f Integer
let rhs :: f Integer
rhs = IO Integer -> f Integer
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO Integer
m f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (IO Integer -> f Integer
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Integer -> f Integer)
-> (Integer -> IO Integer) -> Integer -> f Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> IO Integer
f) :: f Integer
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
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 = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showM :: String
showM = IO Integer -> String
forall a. Show a => IO a -> String
showIO IO Integer
m
showF :: String
showF = LinearEquation -> String
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showF
, String
"m = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showM
]
}
f Integer -> f Integer -> Context -> PropertyT IO ()
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