    {-# 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 :: forall a. (Eq a, Arbitrary a, Show a) => 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 :: forall a. (Show a, Eq a, Arbitrary a) => 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 :: forall a. (Show a, Eq a, Arbitrary a) => 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 :: forall a. (Show a, Eq a, Arbitrary a) => 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 :: forall a. (Show a, Eq a, Arbitrary a) => 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 :: forall a.
    (Eq a, Arbitrary a, CoArbitrary a, Function a, Show a) =>
    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
        )
      ]