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