    {-# 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 :: forall a. (Eq a, Show a) => 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 :: forall a. (Eq a, Show a) => 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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      c <- forAll gen
      let 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 = a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    c
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ 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 == 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 :: forall a. (Eq a, Show a) => 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 <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      b <- forAll gen
      let lhs = a
    a a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    b; rhs = a
    b a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ 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
            }
      heqCtx lhs rhs ctx

    eqReflexive :: forall a. (Eq a, Show a) => Gen a -> Property
    eqReflexive :: forall a. (Eq a, Show a) => 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 <- 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
    a
      let rhs = a
    a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ 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
            }
      heqCtx lhs rhs ctx

    eqNegation :: forall a. (Eq a, Show a) => Gen a -> Property
    eqNegation :: forall a. (Eq a, Show a) => 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
      x <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      y <- forAll gen
      let lhs = a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    /= a
    y
      let rhs = Bool -> Bool
    not (a
    x a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y)
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ 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
                  ]
            }
      heqCtx lhs rhs ctx