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

    module Test.Validity.Relations.Antisymmetry
      ( antisymmetricOnElemsWithEquality,
        antisymmetryOnGensWithEquality,
        antisymmetryOnGens,
        antisymmetry,
        antisymmetryOnArbitrary,
      )
    where

    import Data.GenValidity
    import Test.QuickCheck
    import Test.Validity.Property.Utils

    -- |
    --
    -- \[
    --   Antisymmetric(\prec, \doteq)
    --   \quad\equiv\quad
    --   \forall a, b: ((a \prec b) \wedge (b \prec a)) \Rightarrow (a \doteq b)
    -- \]
    antisymmetricOnElemsWithEquality ::
      -- | A relation
      (a -> a -> Bool) ->
      -- | An equivalence relation
      (a -> a -> Bool) ->
      a ->
      -- | Two elements
      a ->
      Bool
    antisymmetricOnElemsWithEquality :: forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> a -> a -> Bool
    antisymmetricOnElemsWithEquality a -> a -> Bool
    func a -> a -> Bool
    eq a
    a a
    b =
      (a -> a -> Bool
    func a
    a a
    b Bool -> Bool -> Bool
    && a -> a -> Bool
    func a
    b a
    a) Bool -> Bool -> Bool
    ===> (a
    a a -> a -> Bool
    `eq` a
    b)

    antisymmetryOnGensWithEquality ::
      Show a =>
      (a -> a -> Bool) ->
      Gen (a, a) ->
      (a -> a -> Bool) ->
      (a -> [a]) ->
      Property
    antisymmetryOnGensWithEquality :: forall a.
    Show a =>
    (a -> a -> Bool)
    -> Gen (a, a) -> (a -> a -> Bool) -> (a -> [a]) -> Property
    antisymmetryOnGensWithEquality a -> a -> Bool
    func Gen (a, a)
    gen a -> a -> Bool
    eq a -> [a]
    s =
      Gen (a, a) -> ((a, a) -> [(a, a)]) -> ((a, a) -> Bool) -> Property
    forall a prop.
    (Show a, Testable prop) =>
    Gen a -> (a -> [a]) -> (a -> prop) -> Property
    forAllShrink Gen (a, a)
    gen ((a -> [a]) -> (a, a) -> [(a, a)]
    forall a. (a -> [a]) -> (a, a) -> [(a, a)]
    shrinkT2 a -> [a]
    s) (((a, a) -> Bool) -> Property) -> ((a, a) -> Bool) -> Property
    forall a b. (a -> b) -> a -> b
    $
        (a -> a -> Bool) -> (a, a) -> Bool
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((a -> a -> Bool) -> (a, a) -> Bool)
    -> (a -> a -> Bool) -> (a, a) -> Bool
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> Bool) -> (a -> a -> Bool) -> a -> a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> a -> a -> Bool
    antisymmetricOnElemsWithEquality a -> a -> Bool
    func a -> a -> Bool
    eq

    antisymmetryOnGens ::
      (Show a, Eq a) =>
      (a -> a -> Bool) ->
      Gen (a, a) ->
      (a -> [a]) ->
      Property
    antisymmetryOnGens :: forall a.
    (Show a, Eq a) =>
    (a -> a -> Bool) -> Gen (a, a) -> (a -> [a]) -> Property
    antisymmetryOnGens a -> a -> Bool
    func Gen (a, a)
    gen = (a -> a -> Bool)
    -> Gen (a, a) -> (a -> a -> Bool) -> (a -> [a]) -> Property
    forall a.
    Show a =>
    (a -> a -> Bool)
    -> Gen (a, a) -> (a -> a -> Bool) -> (a -> [a]) -> Property
    antisymmetryOnGensWithEquality a -> a -> Bool
    func Gen (a, a)
    gen a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    (==)

    -- |
    --
    -- prop> antisymmetry ((>) :: Int -> Int -> Bool)
    -- prop> antisymmetry ((>=) :: Int -> Int -> Bool)
    -- prop> antisymmetry ((<=) :: Int -> Int -> Bool)
    -- prop> antisymmetry ((<) :: Int -> Int -> Bool)
    -- prop> antisymmetry (Data.List.isPrefixOf :: [Int] -> [Int] -> Bool)
    -- prop> antisymmetry (Data.List.isSuffixOf :: [Int] -> [Int] -> Bool)
    -- prop> antisymmetry (Data.List.isInfixOf :: [Int] -> [Int] -> Bool)
    -- prop> antisymmetry ((\x y -> even x && odd y) :: Int -> Int -> Bool)
    antisymmetry :: (Show a, Eq a, GenValid a) => (a -> a -> Bool) -> Property
    antisymmetry :: forall a.
    (Show a, Eq a, GenValid a) =>
    (a -> a -> Bool) -> Property
    antisymmetry a -> a -> Bool
    func = (a -> a -> Bool) -> Gen (a, a) -> (a -> [a]) -> Property
    forall a.
    (Show a, Eq a) =>
    (a -> a -> Bool) -> Gen (a, a) -> (a -> [a]) -> Property
    antisymmetryOnGens a -> a -> Bool
    func Gen (a, a)
    forall a. GenValid a => Gen a
    genValid a -> [a]
    forall a. GenValid a => a -> [a]
    shrinkValid

    -- |
    --
    -- prop> antisymmetryOnArbitrary ((>) :: Int -> Int -> Bool)
    -- prop> antisymmetryOnArbitrary ((>=) :: Int -> Int -> Bool)
    -- prop> antisymmetryOnArbitrary ((<=) :: Int -> Int -> Bool)
    -- prop> antisymmetryOnArbitrary ((<) :: Int -> Int -> Bool)
    -- prop> antisymmetryOnArbitrary (Data.List.isPrefixOf :: [Int] -> [Int] -> Bool)
    -- prop> antisymmetryOnArbitrary (Data.List.isSuffixOf :: [Int] -> [Int] -> Bool)
    -- prop> antisymmetryOnArbitrary (Data.List.isInfixOf :: [Int] -> [Int] -> Bool)
    -- prop> antisymmetryOnArbitrary ((\x y -> even x && odd y) :: Int -> Int -> Bool)
    antisymmetryOnArbitrary ::
      (Show a, Eq a, Arbitrary a) => (a -> a -> Bool) -> Property
    antisymmetryOnArbitrary :: forall a.
    (Show a, Eq a, Arbitrary a) =>
    (a -> a -> Bool) -> Property
    antisymmetryOnArbitrary a -> a -> Bool
    func = (a -> a -> Bool) -> Gen (a, a) -> (a -> [a]) -> Property
    forall a.
    (Show a, Eq a) =>
    (a -> a -> Bool) -> Gen (a, a) -> (a -> [a]) -> Property
    antisymmetryOnGens a -> a -> Bool
    func Gen (a, a)
    forall a. Arbitrary a => Gen a
    arbitrary a -> [a]
    forall a. Arbitrary a => a -> [a]
    shrink