{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall #-}

module Test.QuickCheck.Classes.Eq
  ( eqLaws
  , substitutiveEqLaws
  ) where

import Data.Proxy (Proxy)
import Test.QuickCheck hiding ((.&.))
import Test.QuickCheck.Property (Property)
import Test.QuickCheck.Function

import Test.QuickCheck.Classes.Internal (Laws(..))

-- | Tests the following properties:
--
-- [/Transitive/]
--   @a '==' b ∧ b '==' c ⇒ a '==' c@
-- [/Symmetric/]
--   @a '==' b ⇒ b '==' a@
-- [/Reflexive/]
--   @a '==' a@
-- [/Negation/]
--   @x '/=' y '==' 'not' (x '==' y)@
--
-- Some of these properties involve implication. In the case that
-- the left hand side of the implication arrow does not hold, we
-- do not retry. Consequently, these properties only end up being
-- useful when the data type has a small number of inhabitants.
eqLaws :: (Eq a, Arbitrary a, Show a) => Proxy a -> Laws
eqLaws :: Proxy a -> Laws
eqLaws Proxy a
p = String -> [(String, Property)] -> Laws
Laws String
"Eq"
  [ (String
"Transitive", Proxy a -> Property
forall a. (Show a, Eq a, Arbitrary a) => Proxy a -> Property
eqTransitive Proxy a
p)
  , (String
"Symmetric", Proxy a -> Property
forall a. (Show a, Eq a, Arbitrary a) => Proxy a -> Property
eqSymmetric Proxy a
p)
  , (String
"Reflexive", Proxy a -> Property
forall a. (Show a, Eq a, Arbitrary a) => Proxy a -> Property
eqReflexive Proxy a
p)
  ]

eqTransitive :: forall a. (Show a, Eq a, Arbitrary a) => Proxy a -> Property
eqTransitive :: Proxy a -> Property
eqTransitive Proxy a
_ = (a -> a -> a -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> a -> Bool) -> Property)
-> (a -> a -> a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
a :: a) a
b a
c -> case a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b of
  Bool
True -> case a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c of
    Bool
True -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c
    Bool
False -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
c
  Bool
False -> case a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c of
    Bool
True -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
c
    Bool
False -> Bool
True

eqSymmetric :: forall a. (Show a, Eq a, Arbitrary a) => Proxy a -> Property
eqSymmetric :: Proxy a -> Property
eqSymmetric Proxy a
_ = (a -> a -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> Bool) -> Property) -> (a -> a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
a :: a) a
b -> case a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b of
  Bool
True -> a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
  Bool
False -> a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
a

eqReflexive :: forall a. (Show a, Eq a, Arbitrary a) => Proxy a -> Property
eqReflexive :: Proxy a -> Property
eqReflexive Proxy a
_ = (a -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> Bool) -> Property) -> (a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
a :: a) -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a

eqNegation :: forall a. (Show a, Eq a, Arbitrary a) => Proxy a -> Property
eqNegation :: Proxy a -> Property
eqNegation Proxy a
_ = (a -> a -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> Bool) -> Property) -> (a -> a -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
x :: a) a
y -> (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Bool
not (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y)

-- | Tests the following properties:
--
-- [/Substitutive/]
--   @x '==' y ⇒ f x '==' f y@
--
-- /Note/: This does not test `eqLaws`.
-- If you want to use this, You should use it in addition to `eqLaws`.
substitutiveEqLaws :: forall a. (Eq a, Arbitrary a, CoArbitrary a, Function a, Show a) => Proxy a -> Laws
substitutiveEqLaws :: Proxy a -> Laws
substitutiveEqLaws Proxy a
_ = String -> [(String, Property)] -> Laws
Laws String
"Eq"
  [ (String
"Substitutivity"
    , (a -> a -> Fun a Integer -> Property) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> Fun a Integer -> Property) -> Property)
-> (a -> a -> Fun a Integer -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(a
x :: a) a
y (Fun a Integer
f :: Fun a Integer) ->
        a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Fun a Integer -> a -> Integer
forall a b. Fun a b -> a -> b
applyFun Fun a Integer
f a
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Fun a Integer -> a -> Integer
forall a b. Fun a b -> a -> b
applyFun Fun a Integer
f a
y
    )
  ]