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

module Hedgehog.Classes.MonadPlus (monadPlusLaws) where

import Control.Monad (MonadPlus(..))

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'MonadPlus' laws:
--
-- [__Left Identity__]: @'mplus' 'mzero'@ ≡ @'id'@
-- [__Right Identity__]: @'flip' 'mplus' 'mzero'@ ≡ @'id'@
-- [__Associativity__]: @'mplus' a ('mplus' b c)@ ≡ @'mplus' ('mplus' a b) c@
-- [__Left Zero__]: @'mzero' '>>=' f@ ≡ @'mzero'@
-- [__Right Zero__]: @v '>>' 'mzero'@ ≡ @'mzero'@
monadPlusLaws ::
  ( MonadPlus f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Laws
monadPlusLaws :: forall (f :: * -> *).
(MonadPlus f, forall x. Eq x => Eq (f x),
 forall x. Show x => Show (f x)) =>
(forall x. Gen x -> Gen (f x)) -> Laws
monadPlusLaws forall x. Gen x -> Gen (f x)
gen = String -> [(String, Property)] -> Laws
Laws String
"MonadPlus"
  [ (String
"Left Identity", forall (f :: * -> *). MonadPlusProp f
monadPlusLeftIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Right Identity", forall (f :: * -> *). MonadPlusProp f
monadPlusRightIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Associativity", forall (f :: * -> *). MonadPlusProp f
monadPlusAssociativity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Left Zero", forall (f :: * -> *). MonadPlusProp f
monadPlusLeftZero forall x. Gen x -> Gen (f x)
gen)
  , (String
"Right Zero", forall (f :: * -> *). MonadPlusProp f
monadPlusRightZero forall x. Gen x -> Gen (f x)
gen)
  ]

type MonadPlusProp f =
  ( MonadPlus f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Property

monadPlusLeftIdentity :: forall f. MonadPlusProp f
monadPlusLeftIdentity :: forall (f :: * -> *). MonadPlusProp f
monadPlusLeftIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f 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. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  let lhs :: f Integer
lhs = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus forall (m :: * -> *) a. MonadPlus m => m a
mzero f Integer
x
  let rhs :: f Integer
rhs = f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Left Identity", lawContextTcName :: String
lawContextTcName = String
"MonadPlus"
        , lawContextLawBody :: String
lawContextLawBody = String
"mplus mzero" String -> String -> String
`congruency` String
"id"
        , 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 f Integer
x; showMZero :: String
showMZero = forall a. Show a => a -> String
show (forall (m :: * -> *) a. MonadPlus m => m a
mzero :: f Integer);
            in [String] -> String
lawWhere
              [ String
"mplus mzero x" String -> String -> String
`congruency` String
"id x, where"
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              , String
"mzero = " forall a. [a] -> [a] -> [a]
++ String
showMZero
              ]
        }
  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

monadPlusRightIdentity :: forall f. MonadPlusProp f
monadPlusRightIdentity :: forall (f :: * -> *). MonadPlusProp f
monadPlusRightIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f 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. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  let lhs :: f Integer
lhs = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
x forall (m :: * -> *) a. MonadPlus m => m a
mzero
  let rhs :: f Integer
rhs = f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Right Identity", lawContextTcName :: String
lawContextTcName = String
"MonadPlus"
        , lawContextLawBody :: String
lawContextLawBody = String
"flip mplus mzero" String -> String -> String
`congruency` String
"id"
        , 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 f Integer
x; showMZero :: String
showMZero = forall a. Show a => a -> String
show (forall (m :: * -> *) a. MonadPlus m => m a
mzero :: f Integer);
            in [String] -> String
lawWhere
              [ String
"mplus x mzero" String -> String -> String
`congruency` String
"id x, where"
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              , String
"mzero = " forall a. [a] -> [a] -> [a]
++ String
showMZero
              ]
        }
  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

monadPlusAssociativity :: forall f. MonadPlusProp f
monadPlusAssociativity :: forall (f :: * -> *). MonadPlusProp f
monadPlusAssociativity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
a <- 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
b <- 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
c <- 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
lhs = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
a (forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
b f Integer
c)
  let rhs :: f Integer
rhs = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus f Integer
a f Integer
b) f Integer
c
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Associativity", lawContextTcName :: String
lawContextTcName = String
"MonadPlus"
        , lawContextLawBody :: String
lawContextLawBody = String
"mplus a (mplus b c)" String -> String -> String
`congruency` String
"mplus (mplus a b) c"
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showA :: String
showA = forall a. Show a => a -> String
show f Integer
a; showB :: String
showB = forall a. Show a => a -> String
show f Integer
b; showC :: String
showC = forall a. Show a => a -> String
show f Integer
c;
            in [String] -> String
lawWhere
              [ String
"mplus a (mplus b c)" String -> String -> String
`congruency` String
"mplus (mplus a b) c, where"
              , String
"a = " forall a. [a] -> [a] -> [a]
++ String
showA
              , String
"b = " forall a. [a] -> [a] -> [a]
++ String
showB
              , String
"c = " forall a. [a] -> [a] -> [a]
++ String
showC
              ]
        }
  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

monadPlusLeftZero :: forall f. MonadPlusProp f
monadPlusLeftZero :: forall (f :: * -> *). MonadPlusProp f
monadPlusLeftZero forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  LinearEquationM f
k' :: LinearEquationM f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
genLinearEquationM
  let lhs :: f Integer
lhs = forall (m :: * -> *) a. MonadPlus m => m a
mzero forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
Functor m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
k'
  let rhs :: f a
rhs = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Left Zero", lawContextTcName :: String
lawContextTcName = String
"MonadPlus"
        , lawContextLawBody :: String
lawContextLawBody = String
"mzero >>= f" String -> String -> String
`congruency` String
"mzero"
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs forall {a}. f a
rhs
        , lawContextTcProp :: String
lawContextTcProp  =
            let showF :: String
showF = forall a. Show a => a -> String
show LinearEquationM f
k'; showMZero :: String
showMZero = forall a. Show a => a -> String
show (forall (m :: * -> *) a. MonadPlus m => m a
mzero :: f Integer);
            in [String] -> String
lawWhere
              [ String
"mzero >>= f" String -> String -> String
`congruency` String
"mzero, where"
              , String
"f = " forall a. [a] -> [a] -> [a]
++ String
showF
              , String
"mzero = " forall a. [a] -> [a] -> [a]
++ String
showMZero
              ]
        }
  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 forall {a}. f a
rhs Context
ctx

monadPlusRightZero :: forall f. MonadPlusProp f
monadPlusRightZero :: forall (f :: * -> *). MonadPlusProp f
monadPlusRightZero forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
v <- 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
lhs = f Integer
v forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (forall (m :: * -> *) a. MonadPlus m => m a
mzero :: f Integer)
  let rhs :: f a
rhs = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Right Zero", lawContextTcName :: String
lawContextTcName = String
"MonadPlus"
        , lawContextLawBody :: String
lawContextLawBody = String
"v >> mzero" String -> String -> String
`congruency` String
"mzero"
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs forall {a}. f a
rhs
        , lawContextTcProp :: String
lawContextTcProp  =
            let showV :: String
showV = forall a. Show a => a -> String
show f Integer
v; showMZero :: String
showMZero = forall a. Show a => a -> String
show (forall (m :: * -> *) a. MonadPlus m => m a
mzero :: f Integer);
            in [String] -> String
lawWhere
              [ String
"v >> mzero" String -> String -> String
`congruency` String
"mzero, where"
              , String
"v = " forall a. [a] -> [a] -> [a]
++ String
showV
              , String
"mzero = " forall a. [a] -> [a] -> [a]
++ String
showMZero
              ]
        }
  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 forall {a}. f a
rhs Context
ctx