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

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

import Data.GenValidity

import Test.QuickCheck

import Test.Syd.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 -> a -> Bool) -- ^ A relation
    -> (a -> a -> Bool) -- ^ An equivalence relation
    -> a
    -> a -- ^ Two elements
    -> Bool
antisymmetricOnElemsWithEquality :: (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 :: (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 :: (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> antisymmetryOnValid ((>) :: Double -> Double -> Bool)
-- prop> antisymmetryOnValid ((>=) :: Double -> Double -> Bool)
-- prop> antisymmetryOnValid ((<=) :: Double -> Double -> Bool)
-- prop> antisymmetryOnValid ((<) :: Double -> Double -> Bool)
-- prop> antisymmetryOnValid (Data.List.isPrefixOf :: [Double] -> [Double] -> Bool)
-- prop> antisymmetryOnValid (Data.List.isSuffixOf :: [Double] -> [Double] -> Bool)
-- prop> antisymmetryOnValid (Data.List.isInfixOf :: [Double] -> [Double] -> Bool)
antisymmetryOnValid ::
       (Show a, Eq a, GenValid a) => (a -> a -> Bool) -> Property
antisymmetryOnValid :: (a -> a -> Bool) -> Property
antisymmetryOnValid 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> 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, GenUnchecked a) => (a -> a -> Bool) -> Property
antisymmetry :: (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. GenUnchecked a => Gen a
genUnchecked a -> [a]
forall a. GenUnchecked a => a -> [a]
shrinkUnchecked

-- |
--
-- 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 :: (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