{-# LANGUAGE ScopedTypeVariables #-}

module Hedgehog.Classes.Eq (eqLaws) where

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'Eq' laws:
--
-- [__Reflexivity__]: @x '==' x@ ≡ @'True'@
-- [__Symmetry__]: @x '==' y@ ≡ @y '==' x@
-- [__Transitivity__]: @x '==' y '&&' y '==' z@ ≡ @x '==' z@
-- [__Negation__]: @x '/=' y@ ≡ @'not' (x '==' y)@
eqLaws :: (Eq a, Show a) => Gen a -> Laws
eqLaws :: Gen a -> Laws
eqLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Eq"
  [ (String
"Transitive", Gen a -> Property
forall a. (Eq a, Show a) => Gen a -> Property
eqTransitive Gen a
gen)
  , (String
"Symmetric", Gen a -> Property
forall a. (Eq a, Show a) => Gen a -> Property
eqSymmetric Gen a
gen)  
  , (String
"Reflexive", Gen a -> Property
forall a. (Eq a, Show a) => Gen a -> Property
eqReflexive Gen a
gen) 
  , (String
"Negation", Gen a -> Property
forall a. (Eq a, Show a) => Gen a -> Property
eqNegation Gen a
gen) 
  ]

eqTransitive :: forall a. (Eq a, Show a) => Gen a -> Property
eqTransitive :: Gen a -> Property
eqTransitive Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
c <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: Bool
lhs = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b Bool -> Bool -> Bool
&& a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c; rhs :: Bool
rhs = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Transitivity", lawContextLawBody :: String
lawContextLawBody = String
"a == b ∧ b == c" String -> String -> String
`congruency` String
"a == c"
        , lawContextTcName :: String
lawContextTcName = String
"Eq", lawContextTcProp :: String
lawContextTcProp =
            let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b; showC :: String
showC = a -> String
forall a. Show a => a -> String
show a
c;
            in [String] -> String
lawWhere
              [ String
"a == b ∧ b == c" String -> String -> String
`congruency` String
"a == c, where"
              , String
"a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
              , String
"b = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showB
              , String
"c = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showC
              ]
        , lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
        }
  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 -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
a a
c Context
ctx; Bool
False -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
hneqCtx a
a a
c Context
ctx }
    Bool
False -> case a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c of { Bool
True -> a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
hneqCtx a
a a
c Context
ctx; Bool
False -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => m ()
success }

eqSymmetric :: forall a. (Eq a, Show a) => Gen a -> Property
eqSymmetric :: Gen a -> Property
eqSymmetric Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
b <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: Bool
lhs = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b; rhs :: Bool
rhs = a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Symmetry", lawContextLawBody :: String
lawContextLawBody = String
"a == b" String -> String -> String
`congruency` String
"b == a"
        , lawContextTcName :: String
lawContextTcName = String
"Eq", lawContextTcProp :: String
lawContextTcProp =
            let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a; showB :: String
showB = a -> String
forall a. Show a => a -> String
show a
b;
            in [String] -> String
lawWhere
              [ String
"a == b" String -> String -> String
`congruency` String
"b == a, where"
              , String
"a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
              , String
"b = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showB
              ]
        , lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
        }
  Bool -> Bool -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Bool
lhs Bool
rhs Context
ctx

eqReflexive :: forall a. (Eq a, Show a) => Gen a -> Property
eqReflexive :: Gen a -> Property
eqReflexive Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
a <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = a
a
  let rhs :: a
rhs = a
a
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Reflexivity", lawContextLawBody :: String
lawContextLawBody = String
"a" String -> String -> String
`congruency` String
"a"
        , lawContextTcName :: String
lawContextTcName = String
"Eq"
        , lawContextTcProp :: String
lawContextTcProp = let showA :: String
showA = a -> String
forall a. Show a => a -> String
show a
a in [String] -> String
lawWhere [ String
"a" String -> String -> String
`congruency` String
"a, where", String
"a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA ]
        , lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
a a
a
        }
  a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx

eqNegation :: forall a. (Eq a, Show a) => Gen a -> Property
eqNegation :: Gen a -> Property
eqNegation Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  a
x <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  a
y <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: Bool
lhs = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y
  let rhs :: Bool
rhs = Bool -> Bool
not (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y)
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Negation", lawContextLawBody :: String
lawContextLawBody = String
"x /= y" String -> String -> String
`congruency` String
"not (x == y)"
        , lawContextTcName :: String
lawContextTcName = String
"Eq"
        , lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = a -> String
forall a. Show a => a -> String
show a
x; showY :: String
showY = a -> String
forall a. Show a => a -> String
show a
y;
            in [String] -> String
lawWhere
              [ String
"x /= y" String -> String -> String
`congruency` String
"not (x == y), where"
              , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
              , String
"y = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showY
              ]
        }
  Bool -> Bool -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Bool
lhs Bool
rhs Context
ctx