{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Test.Syd.Validity.Operations.Identity
    ( leftIdentityOnElemWithEquality
    , leftIdentityOnGenWithEquality
    , leftIdentityOnGen
    , leftIdentityOnValid
    , leftIdentity
    , leftIdentityOnArbitrary
    , rightIdentityOnElemWithEquality
    , rightIdentityOnGenWithEquality
    , rightIdentityOnGen
    , rightIdentityOnValid
    , rightIdentity
    , rightIdentityOnArbitrary
    , identityOnGen
    , identityOnValid
    , identity
    , identityOnArbitrary
    ) where

import Data.GenValidity

import Test.QuickCheck

-- |
--
-- \[
--   LeftIdentity(\star, \doteq, b)
--   \quad\equiv\quad
--   \forall a: (b \star a) \doteq a
-- \]
leftIdentityOnElemWithEquality ::
       (b -> a -> a) -- ^ A binary operation
    -> (a -> a -> Bool) -- ^ An equality
    -> b -- ^ A candidate left-identity
    -> a -- ^ An element
    -> Bool
leftIdentityOnElemWithEquality :: (b -> a -> a) -> (a -> a -> Bool) -> b -> a -> Bool
leftIdentityOnElemWithEquality b -> a -> a
op a -> a -> Bool
eq b
b a
a = (b
b b -> a -> a
`op` a
a) a -> a -> Bool
`eq` a
a

leftIdentityOnGenWithEquality ::
       Show a
    => (b -> a -> a) -- ^ A binary operation
    -> (a -> a -> Bool) -- ^ An equality
    -> b -- ^ A candidate left-identity
    -> Gen a
    -> (a -> [a])
    -> Property
leftIdentityOnGenWithEquality :: (b -> a -> a)
-> (a -> a -> Bool) -> b -> Gen a -> (a -> [a]) -> Property
leftIdentityOnGenWithEquality b -> a -> a
op a -> a -> Bool
eq b
b Gen a
gen a -> [a]
s =
    Gen a -> (a -> [a]) -> (a -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink Gen a
gen a -> [a]
s ((a -> Bool) -> Property) -> (a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ (b -> a -> a) -> (a -> a -> Bool) -> b -> a -> Bool
forall b a. (b -> a -> a) -> (a -> a -> Bool) -> b -> a -> Bool
leftIdentityOnElemWithEquality b -> a -> a
op a -> a -> Bool
eq b
b

leftIdentityOnGen ::
       (Show a, Eq a)
    => (b -> a -> a) -- ^ A binary operation
    -> b -- ^ A candidate left-identity
    -> Gen a
    -> (a -> [a])
    -> Property
leftIdentityOnGen :: (b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
leftIdentityOnGen b -> a -> a
op = (b -> a -> a)
-> (a -> a -> Bool) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
Show a =>
(b -> a -> a)
-> (a -> a -> Bool) -> b -> Gen a -> (a -> [a]) -> Property
leftIdentityOnGenWithEquality b -> a -> a
op a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- |
--
-- prop> leftIdentityOnValid (flip ((^) :: Rational -> Int -> Rational)) 1
leftIdentityOnValid ::
       (Show a, Eq a, GenValid a) => (b -> a -> a) -> b -> Property
leftIdentityOnValid :: (b -> a -> a) -> b -> Property
leftIdentityOnValid b -> a -> a
op b
b = (b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
leftIdentityOnGen b -> a -> a
op b
b Gen a
forall a. GenValid a => Gen a
genValid a -> [a]
forall a. GenValid a => a -> [a]
shrinkValid

-- |
--
-- prop> leftIdentity (flip ((^) :: Int -> Int -> Int)) 1
leftIdentity :: (Show a, Eq a, GenUnchecked a) => (b -> a -> a) -> b -> Property
leftIdentity :: (b -> a -> a) -> b -> Property
leftIdentity b -> a -> a
op b
b = (b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
leftIdentityOnGen b -> a -> a
op b
b Gen a
forall a. GenUnchecked a => Gen a
genUnchecked a -> [a]
forall a. GenUnchecked a => a -> [a]
shrinkUnchecked

-- |
--
-- prop> leftIdentityOnArbitrary (flip ((^) :: Int -> Int -> Int)) 1
leftIdentityOnArbitrary ::
       (Show a, Eq a, Arbitrary a) => (b -> a -> a) -> b -> Property
leftIdentityOnArbitrary :: (b -> a -> a) -> b -> Property
leftIdentityOnArbitrary b -> a -> a
op b
b = (b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
leftIdentityOnGen b -> a -> a
op b
b Gen a
forall a. Arbitrary a => Gen a
arbitrary a -> [a]
forall a. Arbitrary a => a -> [a]
shrink

-- |
--
-- \[
--   RightIdentity(\star, \doteq, b)
--   \quad\equiv\quad
--   \forall a: (a \star b) \doteq a
-- \]
rightIdentityOnElemWithEquality ::
       (a -> b -> a) -- ^ A binary operation
    -> (a -> a -> Bool) -- ^ An equality
    -> b -- ^ A candidate right-identity
    -> a -- ^ An element
    -> Bool
rightIdentityOnElemWithEquality :: (a -> b -> a) -> (a -> a -> Bool) -> b -> a -> Bool
rightIdentityOnElemWithEquality a -> b -> a
op a -> a -> Bool
eq b
b a
a = (a
a a -> b -> a
`op` b
b) a -> a -> Bool
`eq` a
a

rightIdentityOnGenWithEquality ::
       Show a
    => (a -> b -> a) -- ^ A binary operation
    -> (a -> a -> Bool) -- ^ An equality
    -> b -- ^ A candidate right-identity
    -> Gen a
    -> (a -> [a])
    -> Property
rightIdentityOnGenWithEquality :: (a -> b -> a)
-> (a -> a -> Bool) -> b -> Gen a -> (a -> [a]) -> Property
rightIdentityOnGenWithEquality a -> b -> a
op a -> a -> Bool
eq b
b Gen a
gen a -> [a]
s =
    Gen a -> (a -> [a]) -> (a -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink Gen a
gen a -> [a]
s ((a -> Bool) -> Property) -> (a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ (a -> b -> a) -> (a -> a -> Bool) -> b -> a -> Bool
forall a b. (a -> b -> a) -> (a -> a -> Bool) -> b -> a -> Bool
rightIdentityOnElemWithEquality a -> b -> a
op a -> a -> Bool
eq b
b

rightIdentityOnGen ::
       (Show a, Eq a)
    => (a -> b -> a) -- ^ A binary operation
    -> b -- ^ A candidate right-identity
    -> Gen a
    -> (a -> [a])
    -> Property
rightIdentityOnGen :: (a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
rightIdentityOnGen a -> b -> a
op = (a -> b -> a)
-> (a -> a -> Bool) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
Show a =>
(a -> b -> a)
-> (a -> a -> Bool) -> b -> Gen a -> (a -> [a]) -> Property
rightIdentityOnGenWithEquality a -> b -> a
op a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- |
--
-- prop> rightIdentityOnValid ((^) :: Rational -> Int -> Rational) 1
rightIdentityOnValid ::
       (Show a, Eq a, GenValid a) => (a -> b -> a) -> b -> Property
rightIdentityOnValid :: (a -> b -> a) -> b -> Property
rightIdentityOnValid a -> b -> a
op b
b = (a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
rightIdentityOnGen a -> b -> a
op b
b Gen a
forall a. GenValid a => Gen a
genValid a -> [a]
forall a. GenValid a => a -> [a]
shrinkValid

-- |
--
-- prop> rightIdentity ((^) :: Int -> Int -> Int) 1
rightIdentity ::
       (Show a, Eq a, GenUnchecked a) => (a -> b -> a) -> b -> Property
rightIdentity :: (a -> b -> a) -> b -> Property
rightIdentity a -> b -> a
op b
b = (a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
rightIdentityOnGen a -> b -> a
op b
b Gen a
forall a. GenUnchecked a => Gen a
genUnchecked a -> [a]
forall a. GenUnchecked a => a -> [a]
shrinkUnchecked

-- |
--
-- prop> rightIdentityOnArbitrary ((^) :: Int -> Int -> Int) 1
rightIdentityOnArbitrary ::
       (Show a, Eq a, Arbitrary a) => (a -> b -> a) -> b -> Property
rightIdentityOnArbitrary :: (a -> b -> a) -> b -> Property
rightIdentityOnArbitrary a -> b -> a
op b
b = (a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
rightIdentityOnGen a -> b -> a
op b
b Gen a
forall a. Arbitrary a => Gen a
arbitrary a -> [a]
forall a. Arbitrary a => a -> [a]
shrink

-- |
--
-- \[
--   Identity(\star, \doteq, b)
--   \quad\equiv\quad
--   LeftIdentity(\star, \doteq, b) \wedge RightIdentity(\star, \doteq, b)
-- \]
identityOnGen ::
       (Show a, Eq a) => (a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
identityOnGen :: (a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
identityOnGen a -> a -> a
op a
e Gen a
gen a -> [a]
s =
    (a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(b -> a -> a) -> b -> Gen a -> (a -> [a]) -> Property
leftIdentityOnGen a -> a -> a
op a
e Gen a
gen a -> [a]
s Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
forall a b.
(Show a, Eq a) =>
(a -> b -> a) -> b -> Gen a -> (a -> [a]) -> Property
rightIdentityOnGen a -> a -> a
op a
e Gen a
gen a -> [a]
s

-- |
--
-- prop> identityOnValid ((*) :: Rational -> Rational -> Rational) 1
-- prop> identityOnValid ((+) :: Rational -> Rational -> Rational) 0
identityOnValid :: (Show a, Eq a, GenValid a) => (a -> a -> a) -> a -> Property
identityOnValid :: (a -> a -> a) -> a -> Property
identityOnValid a -> a -> a
op a
a = (a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
forall a.
(Show a, Eq a) =>
(a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
identityOnGen a -> a -> a
op a
a Gen a
forall a. GenValid a => Gen a
genValid a -> [a]
forall a. GenValid a => a -> [a]
shrinkValid

-- |
--
-- prop> identity ((*) :: Int -> Int -> Int) 1
-- prop> identity ((+) :: Int -> Int -> Int) 0
identity :: (Show a, Eq a, GenUnchecked a) => (a -> a -> a) -> a -> Property
identity :: (a -> a -> a) -> a -> Property
identity a -> a -> a
op a
e = (a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
forall a.
(Show a, Eq a) =>
(a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
identityOnGen a -> a -> a
op a
e Gen a
forall a. GenUnchecked a => Gen a
genUnchecked a -> [a]
forall a. GenUnchecked a => a -> [a]
shrinkUnchecked

-- |
--
-- prop> identityOnArbitrary ((*) :: Int -> Int -> Int) 1
-- prop> identityOnArbitrary ((+) :: Int -> Int -> Int) 0
identityOnArbitrary ::
       (Show a, Eq a, Arbitrary a) => (a -> a -> a) -> a -> Property
identityOnArbitrary :: (a -> a -> a) -> a -> Property
identityOnArbitrary a -> a -> a
op a
a = (a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
forall a.
(Show a, Eq a) =>
(a -> a -> a) -> a -> Gen a -> (a -> [a]) -> Property
identityOnGen a -> a -> a
op a
a Gen a
forall a. Arbitrary a => Gen a
arbitrary a -> [a]
forall a. Arbitrary a => a -> [a]
shrink