    {-# 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 x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadPlusProp f
    monadPlusLeftIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Right Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadPlusProp f
    monadPlusRightIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Associativity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadPlusProp f
    monadPlusAssociativity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Left Zero", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadPlusProp f
    monadPlusLeftZero Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Right Zero", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *). MonadPlusProp f
    monadPlusRightZero Gen x -> Gen (f x)
    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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs = f Integer -> f Integer -> f Integer
    forall a. f a -> f a -> f a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus f Integer
    forall a. f a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero f Integer
    x
      let rhs = f Integer
    x
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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 = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x; showMZero :: String
    showMZero = f Integer -> String
    forall a. Show a => a -> String
    show (f Integer
    forall a. f a
    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 = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  , String
    "mzero = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showMZero
                  ]
            }
      heqCtx1 lhs rhs ctx

    monadPlusRightIdentity :: forall f. MonadPlusProp f
    monadPlusRightIdentity :: forall (f :: * -> *). MonadPlusProp f
    monadPlusRightIdentity 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
      x <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs = f Integer -> f Integer -> f Integer
    forall a. f a -> f a -> f a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus f Integer
    x f Integer
    forall a. f a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      let rhs = f Integer
    x
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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 = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    x; showMZero :: String
    showMZero = f Integer -> String
    forall a. Show a => a -> String
    show (f Integer
    forall a. f a
    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 = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showX
                  , String
    "mzero = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showMZero
                  ]
            }
      heqCtx1 lhs rhs ctx

    monadPlusAssociativity :: forall f. MonadPlusProp f
    monadPlusAssociativity :: forall (f :: * -> *). MonadPlusProp f
    monadPlusAssociativity 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
      a <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      b <- forAll $ fgen genSmallInteger
      c <- forAll $ fgen genSmallInteger
      let lhs = f Integer -> f Integer -> f Integer
    forall a. f a -> f a -> f a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus f Integer
    a (f Integer -> f Integer -> f Integer
    forall a. f a -> f a -> f a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus f Integer
    b f Integer
    c)
      let rhs = f Integer -> f Integer -> f Integer
    forall a. f a -> f a -> f a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus (f Integer -> f Integer -> f Integer
    forall a. f a -> f a -> f a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus f Integer
    a f Integer
    b) f Integer
    c
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            , lawContextTcProp :: String
    lawContextTcProp =
                let showA :: String
    showA = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    a; showB :: String
    showB = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    b; showC :: String
    showC = f Integer -> String
    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 = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                  , String
    "b = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showB
                  , String
    "c = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showC
                  ]
            }
      heqCtx1 lhs rhs ctx

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

    monadPlusRightZero :: forall f. MonadPlusProp f
    monadPlusRightZero :: forall (f :: * -> *). MonadPlusProp f
    monadPlusRightZero 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
      v <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs = f Integer
    v f Integer -> f Integer -> f Integer
    forall a b. f a -> f b -> f b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (f Integer
    forall a. f a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero :: f Integer)
      let rhs = f a
    forall a. f a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    forall a. f a
    rhs
            , lawContextTcProp :: String
    lawContextTcProp  =
                let showV :: String
    showV = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    v; showMZero :: String
    showMZero = f Integer -> String
    forall a. Show a => a -> String
    show (f Integer
    forall a. f a
    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 = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showV
                  , String
    "mzero = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showMZero
                  ]
            }
      heqCtx1 lhs rhs ctx