{-# LANGUAGE ScopedTypeVariables #-}

module Hedgehog.Classes.Semigroup
  ( semigroupLaws
  , commutativeSemigroupLaws
  , exponentialSemigroupLaws
  , idempotentSemigroupLaws
  , rectangularBandSemigroupLaws
  ) where

import Data.Semigroup (Semigroup(..))
import Hedgehog
import Hedgehog.Classes.Common
import Data.List.NonEmpty
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import qualified Data.Foldable as Foldable

-- | Tests the following 'Semigroup' laws:
--
-- [__Associativity__]: @a '<>' (b '<>' c)@ ≡ @(a '<>' b) '<>' c@
-- [__Concatenation__]: @'sconcat'@ ≡ @'Foldable.foldr1' ('<>')@
-- [__Times__]: @'stimes' n a@ ≡ @'foldr1' ('<>') ('replicate' n a)@
semigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
semigroupLaws :: Gen a -> Laws
semigroupLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Semigroup"
  [ (String
"Associativity", Gen a -> Property
forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupAssociative Gen a
gen)
  , (String
"Concatenation", Gen a -> Property
forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupConcatenation Gen a
gen)
  , (String
"Times", Gen a -> Property
forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupTimes Gen a
gen)
  ]

-- | Tests the following 'Semigroup' laws:
--
-- [__Commutativity__]: @a '<>' b@ ≡ @b '<>' a@
commutativeSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
commutativeSemigroupLaws :: Gen a -> Laws
commutativeSemigroupLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Commutative Semigroup"
  [ (String
"Commutative", Gen a -> Property
forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupCommutative Gen a
gen)
  ]

-- | Tests the following 'Semigroup' laws:
--
-- [__Exponentiality__]: @'stimes' n (a '<>' b)@ ≡ @'stimes' n a '<>' 'stimes' n b@
exponentialSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
exponentialSemigroupLaws :: Gen a -> Laws
exponentialSemigroupLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Exponential Semigroup"
  [ (String
"Exponential", Gen a -> Property
forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupExponential Gen a
gen)
  ]

-- | Tests the following 'Semigroup' laws:
--
-- [__Idempotency__]: @a '<>' a@ ≡ @a@
idempotentSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
idempotentSemigroupLaws :: Gen a -> Laws
idempotentSemigroupLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Idempotent Semigroup"
  [ (String
"Idempotent", Gen a -> Property
forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupIdempotent Gen a
gen)
  ]

-- | Tests the following 'Semigroup' laws:
--
-- [__Rectangular Bandedness__]: @a '<>' b '<>' a@ ≡ @a@
rectangularBandSemigroupLaws :: (Eq a, Semigroup a, Show a) => Gen a -> Laws
rectangularBandSemigroupLaws :: Gen a -> Laws
rectangularBandSemigroupLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Rectangular Band Semigroup"
  [ (String
"Rectangular Band", Gen a -> Property
forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupRectangularBand Gen a
gen)
  ]

semigroupAssociative :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupAssociative :: Gen a -> Property
semigroupAssociative Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
c <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> (a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c)
  let rhs :: a
rhs = (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b) a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
c
  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
"Associativity", lawContextTcName :: String
lawContextTcName = String
"Semigroup"
        , lawContextLawBody :: String
lawContextLawBody = String
"a <> (b <> c)" String -> String -> String
`congruency` String
"(a <> b) <> c"
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b; showC :: String
showC = a -> String
forall a. Show a => a -> String
show a
c;
            in [String] -> String
lawWhere
              [ String
"a <> (b <> c)" String -> String -> String
`congruency` String
"(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
              ]
        }
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx

semigroupCommutative :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupCommutative :: Gen a -> Property
semigroupCommutative Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b
  let rhs :: a
rhs = a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a
  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
"Commutativity", lawContextTcName :: String
lawContextTcName = String
"Semigroup"
        , lawContextLawBody :: String
lawContextLawBody = String
"a <> b" String -> String -> String
`congruency` String
"b <> a"
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b;
            in [String] -> String
lawWhere
              [ String
"a <> b" String -> String -> String
`congruency` String
"b <> a, 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
              ]
        }  
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx

semigroupConcatenation :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupConcatenation :: Gen a -> Property
semigroupConcatenation Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen 
  [a]
as <- Gen [a] -> PropertyT IO [a]
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen [a] -> PropertyT IO [a]) -> Gen [a] -> PropertyT IO [a]
forall a b. (a -> b) -> a -> b
$ Gen a -> Gen [a]
forall a. Gen a -> Gen [a]
genSmallList Gen a
gen
  let ne :: NonEmpty a
ne = a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
as
  let lhs :: a
lhs = NonEmpty a -> a
forall a. Semigroup a => NonEmpty a -> a
sconcat NonEmpty a
ne
  let rhs :: a
rhs = (a -> a -> a) -> NonEmpty a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Foldable.foldr1 a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) NonEmpty a
ne
  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
"Concatenation", lawContextTcName :: String
lawContextTcName = String
"Semigroup"
        , lawContextLawBody :: String
lawContextLawBody = String
"sconcat" String -> String -> String
`congruency` String
"foldr1 (<>)"
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showNE :: String
showNE = NonEmpty a -> String
forall a. Show a => a -> String
show NonEmpty a
ne;
            in [String] -> String
lawWhere
              [ String
"sconcat ne" String -> String -> String
`congruency` String
"foldr1 (<>) ne, where"
              , String
"ne = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showNE
              ]
        }
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx  

semigroupTimes :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupTimes :: Gen a -> Property
semigroupTimes Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  Int
n <- Gen Int -> PropertyT IO Int
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Range Int -> Gen Int
forall (m :: * -> *). MonadGen m => Range Int -> m Int
Gen.int (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
2 Int
5))
  let lhs :: a
lhs = Int -> a -> a
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes Int
n a
a
  let rhs :: a
rhs = (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Foldable.foldr1 a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) (Int -> a -> [a]
forall a. Int -> a -> [a]
replicate Int
n a
a)
  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
"Times", lawContextTcName :: String
lawContextTcName = String
"Semigroup"
        , lawContextLawBody :: String
lawContextLawBody = String
"stimes n a" String -> String -> String
`congruency` String
"foldr1 (<>) (replicate n a)"
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showN :: String
showN = Int -> String
forall a. Show a => a -> String
show Int
n; showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a;
            in [String] -> String
lawWhere
              [ String
"stimes n a" String -> String -> String
`congruency` String
"foldr1 (<>) (replicate n a), where"
              , String
"a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
              , String
"n = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showN
              ]
        }  
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx

semigroupExponential :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupExponential :: Gen a -> Property
semigroupExponential Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  Int
n <- Gen Int -> PropertyT IO Int
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Range Int -> Gen Int
forall (m :: * -> *). MonadGen m => Range Int -> m Int
Gen.int (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
2 Int
5))
  let lhs :: a
lhs = Int -> a -> a
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes Int
n (a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b)
  let rhs :: a
rhs = Int -> a -> a
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes Int
n a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Int -> a -> a
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes Int
n a
b
  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
"Exponential", lawContextTcName :: String
lawContextTcName = String
"Semigroup"
        , lawContextLawBody :: String
lawContextLawBody = String
"stimes n (a <> b)" String -> String -> String
`congruency` String
"stimes n a <> stimes n b"
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showN :: String
showN = Int -> String
forall a. Show a => a -> String
show Int
n; showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b;
            in [String] -> String
lawWhere
              [ String
"stimes n (a <> b)" String -> String -> String
`congruency` String
"stimes n a <> stimes n b, 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
"n = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showN
              ]
        }  
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx

semigroupIdempotent :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupIdempotent :: Gen a -> Property
semigroupIdempotent Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a
  let rhs :: a
rhs = a
a
  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
"Idempotency", lawContextTcName :: String
lawContextTcName = String
"Semigroup"
        , lawContextLawBody :: String
lawContextLawBody = String
"a <> a" String -> String -> String
`congruency` String
"a"
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a;
            in [String] -> String
lawWhere
              [ String
"a <> a" String -> String -> String
`congruency` String
"a, where"
              , String
"a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
              ]
        }
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx

semigroupRectangularBand :: forall a. (Eq a, Semigroup a, Show a) => Gen a -> Property
semigroupRectangularBand :: Gen a -> Property
semigroupRectangularBand Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = a
a a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
b a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a
  let rhs :: a
rhs = a
a
  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
"Rectangular Band", lawContextTcName :: String
lawContextTcName = String
"Semigroup"
        , lawContextLawBody :: String
lawContextLawBody = String
"a <> b <> a" String -> String -> String
`congruency` String
"a"
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b;
            in [String] -> String
lawWhere
              [ String
"a <> b <> a" String -> String -> String
`congruency` String
"a, 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
              ]
        }  
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx