{- HLINT ignore "Use camelCase" -}
{- HLINT ignore "Redundant bracket" -}

-- |
-- Copyright: © 2022–2023 Jonathan Knowles
-- License: Apache-2.0
--
-- This module provides 'Laws' definitions for classes exported by
-- "Data.Group".
--
module Test.QuickCheck.Classes.Group
    (
    -- * Group
      groupLaws

    -- * Abelian
    , abelianLaws
    )
    where

import Prelude

import Data.Function
    ( (&) )
import Data.Group
    ( Abelian, Group (..) )
import Data.Proxy
    ( Proxy (..) )
import Internal
    ( cover, makeLaw0, makeLaw1, makeLaw2, makeProperty, report )
import Test.QuickCheck
    ( Arbitrary (..)
    , NonNegative (..)
    , NonPositive (..)
    , Property
    , forAllShrink
    )
import Test.QuickCheck.Classes
    ( Laws (..) )

--------------------------------------------------------------------------------
-- Group
--------------------------------------------------------------------------------

-- | 'Laws' for instances of 'Group'.
--
-- Includes the following laws:
--
-- __/Inversion/__
--
-- @
-- 'invert' 'mempty' '==' 'mempty'
-- @
--
-- @
-- 'invert' ('invert' a) '==' a
-- @
--
-- @
-- \      \ a '<>' 'invert' a '==' 'mempty'
-- 'invert' a '<>' \      \ a '==' 'mempty'
-- @
--
-- __/Subtraction/__
--
-- @
-- a '~~' 'mempty' '==' a
-- @
--
-- @
-- a '~~' a '==' 'mempty'
-- @
--
-- @
-- a '~~' b '==' a '<>' 'invert' b
-- @
--
-- __/Exponentiation/__
--
-- @
-- 'pow' a 0 '==' 'mempty'
-- @
--
-- @
-- n '>=' 0 ==> 'pow' a n '==' \      \  'mconcat' ('replicate'  \   \ n  a)
-- n '<=' 0 ==> 'pow' a n '==' 'invert' ('mconcat' ('replicate' ('abs' n) a))
-- @
--
-- == Superclass laws
--
-- Note that the following superclass laws are __not__ included:
--
-- * 'Test.QuickCheck.Classes.monoidLaws'
--
groupLaws
    :: forall a. (Arbitrary a, Show a, Eq a, Group a)
    => Proxy a
    -> Laws
groupLaws :: forall a. (Arbitrary a, Show a, Eq a, Group a) => Proxy a -> Laws
groupLaws Proxy a
_ = String -> [(String, Property)] -> Laws
Laws String
"Group"
    [ forall {k} (a :: k).
String -> (Proxy a -> Property) -> (String, Property)
makeLaw0 @a
        String
"groupLaw_invert_mempty"
        (forall a. (Eq a, Show a, Group a) => Proxy a -> Property
groupLaw_invert_mempty)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_invert_invert"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_invert)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_invert_mappend_1"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_mappend_1)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_invert_mappend_2"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_mappend_2)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_subtract_mempty"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_subtract_mempty)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_subtract_self"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_subtract_self)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"groupLaw_subtract_other"
        (forall a. (Eq a, Show a, Group a) => a -> a -> Property
groupLaw_subtract_other)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_pow_zero"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_zero)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_pow_nonNegative"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_nonNegative)
    , forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> t) -> (String, Property)
makeLaw1 @a
        String
"groupLaw_pow_nonPositive"
        (forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_nonPositive)
    ]

groupLaw_invert_mempty
    :: forall a. (Eq a, Show a, Group a) => Proxy a -> Property
groupLaw_invert_mempty :: forall a. (Eq a, Show a, Group a) => Proxy a -> Property
groupLaw_invert_mempty Proxy a
_ =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"invert (mempty @a) == (mempty @a)"
        (forall m. Group m => m -> m
invert (forall a. Monoid a => a
mempty @a) forall a. Eq a => a -> a -> Bool
== (forall a. Monoid a => a
mempty @a))
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mempty @a"
        (forall a. Monoid a => a
mempty @a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert (mempty @a)"
        (forall m. Group m => m -> m
invert (forall a. Monoid a => a
mempty @a))

groupLaw_invert_invert
    :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_invert :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_invert a
a =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"invert (invert a) == a"
        (forall m. Group m => m -> m
invert (forall m. Group m => m -> m
invert a
a) forall a. Eq a => a -> a -> Bool
== a
a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert a"
        (forall m. Group m => m -> m
invert a
a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert (invert a)"
        (forall m. Group m => m -> m
invert (forall m. Group m => m -> m
invert a
a))

groupLaw_invert_mappend_1
    :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_mappend_1 :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_mappend_1 a
a =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"a <> invert a == mempty"
        (a
a forall a. Semigroup a => a -> a -> a
<> forall m. Group m => m -> m
invert a
a forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mempty @a"
        (forall a. Monoid a => a
mempty @a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert a"
        (forall m. Group m => m -> m
invert a
a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> invert a"
        (a
a forall a. Semigroup a => a -> a -> a
<> forall m. Group m => m -> m
invert a
a)

groupLaw_invert_mappend_2
    :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_mappend_2 :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_invert_mappend_2 a
a =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"invert a <> a == mempty"
        (forall m. Group m => m -> m
invert a
a forall a. Semigroup a => a -> a -> a
<> a
a forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mempty @a"
        (forall a. Monoid a => a
mempty @a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert a"
        (forall m. Group m => m -> m
invert a
a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert a <> a"
        (forall m. Group m => m -> m
invert a
a forall a. Semigroup a => a -> a -> a
<> a
a)

groupLaw_subtract_mempty
    :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_subtract_mempty :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_subtract_mempty a
a =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"a ~~ mempty == a"
        (a
a forall m. Group m => m -> m -> m
~~ forall a. Monoid a => a
mempty forall a. Eq a => a -> a -> Bool
== a
a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mempty @a"
        (forall a. Monoid a => a
mempty @a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a ~~ mempty"
        (a
a forall m. Group m => m -> m -> m
~~ forall a. Monoid a => a
mempty)

groupLaw_subtract_self
    :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_subtract_self :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_subtract_self a
a =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"a ~~ a == mempty"
        (a
a forall m. Group m => m -> m -> m
~~ a
a forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty @a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mempty @a"
        (forall a. Monoid a => a
mempty @a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a ~~ a"
        (a
a forall m. Group m => m -> m -> m
~~ a
a)

groupLaw_subtract_other
    :: (Eq a, Show a, Group a) => a -> a -> Property
groupLaw_subtract_other :: forall a. (Eq a, Show a, Group a) => a -> a -> Property
groupLaw_subtract_other a
a a
b =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"a ~~ b == a <> invert b"
        (a
a forall m. Group m => m -> m -> m
~~ a
b forall a. Eq a => a -> a -> Bool
== a
a forall a. Semigroup a => a -> a -> a
<> forall m. Group m => m -> m
invert a
b)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a ~~ b"
        (a
a forall m. Group m => m -> m -> m
~~ a
b)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert b"
        (forall m. Group m => m -> m
invert a
b)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> invert b"
        (a
a forall a. Semigroup a => a -> a -> a
<> forall m. Group m => m -> m
invert a
b)

groupLaw_pow_zero
    :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_zero :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_zero a
a =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"pow a 0 == mempty"
        (forall m x. (Group m, Integral x) => m -> x -> m
pow a
a Integer
0 forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"pow a 0"
        (forall m x. (Group m, Integral x) => m -> x -> m
pow a
a Integer
0)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mempty @a"
        (forall a. Monoid a => a
mempty @a)

groupLaw_pow_nonNegative
    :: (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_nonNegative :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_nonNegative a
a =
    forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink (forall a. Arbitrary a => Gen a
arbitrary @(NonNegative Int)) forall a. Arbitrary a => a -> [a]
shrink forall a b. (a -> b) -> a -> b
$ \(NonNegative Int
n) ->
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"pow a n == mconcat (replicate n a)"
        (forall m x. (Group m, Integral x) => m -> x -> m
pow a
a Int
n forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => [a] -> a
mconcat (forall a. Int -> a -> [a]
replicate Int
n a
a))
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"pow a n"
        (forall m x. (Group m, Integral x) => m -> x -> m
pow a
a Int
n)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mconcat (replicate n a)"
        (forall a. Monoid a => [a] -> a
mconcat (forall a. Int -> a -> [a]
replicate Int
n a
a))
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == 0"
        (Int
n forall a. Eq a => a -> a -> Bool
== Int
0)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == 1"
        (Int
n forall a. Eq a => a -> a -> Bool
== Int
1)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == 2"
        (Int
n forall a. Eq a => a -> a -> Bool
== Int
2)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == 3"
        (Int
n forall a. Eq a => a -> a -> Bool
== Int
3)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n >= 4"
        (Int
n forall a. Ord a => a -> a -> Bool
>= Int
4)

groupLaw_pow_nonPositive
    :: (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_nonPositive :: forall a. (Eq a, Show a, Group a) => a -> Property
groupLaw_pow_nonPositive a
a =
    forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink (forall a. Arbitrary a => Gen a
arbitrary @(NonPositive Int)) forall a. Arbitrary a => a -> [a]
shrink forall a b. (a -> b) -> a -> b
$ \(NonPositive Int
n) ->
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"pow a n == invert (mconcat (replicate (abs n) a))"
        (forall m x. (Group m, Integral x) => m -> x -> m
pow a
a Int
n forall a. Eq a => a -> a -> Bool
== forall m. Group m => m -> m
invert (forall a. Monoid a => [a] -> a
mconcat (forall a. Int -> a -> [a]
replicate (forall a. Num a => a -> a
abs Int
n) a
a)))
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"pow a n"
        (forall m x. (Group m, Integral x) => m -> x -> m
pow a
a Int
n)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"mconcat (replicate (abs n) a)"
        (forall a. Monoid a => [a] -> a
mconcat (forall a. Int -> a -> [a]
replicate (forall a. Num a => a -> a
abs Int
n) a
a))
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"invert (mconcat (replicate (abs n) a))"
        (forall m. Group m => m -> m
invert (forall a. Monoid a => [a] -> a
mconcat (forall a. Int -> a -> [a]
replicate (forall a. Num a => a -> a
abs Int
n) a
a)))
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == -0"
        (Int
n forall a. Eq a => a -> a -> Bool
== -Int
0)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == -1"
        (Int
n forall a. Eq a => a -> a -> Bool
== -Int
1)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == -2"
        (Int
n forall a. Eq a => a -> a -> Bool
== -Int
2)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n == -3"
        (Int
n forall a. Eq a => a -> a -> Bool
== -Int
3)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"n <= -4"
        (Int
n forall a. Ord a => a -> a -> Bool
<= -Int
4)

--------------------------------------------------------------------------------
-- Abelian
--------------------------------------------------------------------------------

-- | 'Laws' for instances of 'Abelian'.
--
-- Includes the following law:
--
-- __/Commutativity/__
--
-- @
-- a '<>' b '==' b '<>' a
-- @
--
-- == Superclass laws
--
-- Note that the following superclass laws are __not__ included:
--
-- * 'Test.QuickCheck.Classes.Group.groupLaws'
--
abelianLaws
    :: forall a. (Arbitrary a, Show a, Eq a, Abelian a)
    => Proxy a
    -> Laws
abelianLaws :: forall a. (Arbitrary a, Show a, Eq a, Abelian a) => Proxy a -> Laws
abelianLaws Proxy a
_ = String -> [(String, Property)] -> Laws
Laws String
"Abelian"
    [ forall a t.
(Arbitrary a, Show a, Eq a, Semigroup a, Testable t) =>
String -> (a -> a -> t) -> (String, Property)
makeLaw2 @a
        String
"abelianLaw_commutative"
        (forall a. (Eq a, Show a, Abelian a) => a -> a -> Property
abelianLaw_commutative)
    ]

abelianLaw_commutative
    :: (Eq a, Show a, Abelian a) => a -> a -> Property
abelianLaw_commutative :: forall a. (Eq a, Show a, Abelian a) => a -> a -> Property
abelianLaw_commutative a
a a
b =
    forall t. Testable t => String -> t -> Property
makeProperty
        String
"a <> b == b <> a"
        (a
a forall a. Semigroup a => a -> a -> a
<> a
b forall a. Eq a => a -> a -> Bool
== a
b forall a. Semigroup a => a -> a -> a
<> a
a)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"a <> b"
        (a
a forall a. Semigroup a => a -> a -> a
<> a
b)
    forall a b. a -> (a -> b) -> b
& forall a prop.
(Show a, Testable prop) =>
String -> a -> prop -> Property
report
        String
"b <> a"
        (a
b forall a. Semigroup a => a -> a -> a
<> a
a)
    forall a b. a -> (a -> b) -> b
& forall t. Testable t => String -> Bool -> t -> Property
cover
        String
"(a /= b) && (a <> b /= a) && (b <> a /= b)"
        ((a
a forall a. Eq a => a -> a -> Bool
/= a
b) Bool -> Bool -> Bool
&& (a
a forall a. Semigroup a => a -> a -> a
<> a
b forall a. Eq a => a -> a -> Bool
/= a
a) Bool -> Bool -> Bool
&& (a
b forall a. Semigroup a => a -> a -> a
<> a
a forall a. Eq a => a -> a -> Bool
/= a
b))