    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE QuantifiedConstraints #-}
    {-# LANGUAGE RankNTypes #-}

    module Hedgehog.Classes.Contravariant (contravariantLaws) where

    import Data.Functor.Contravariant (Contravariant(..))

    import Hedgehog
    import Hedgehog.Classes.Common

    -- | Tests the following 'Contravariant' laws:
    --
    -- [__Identity__]: @'contramap' 'id'@ ≡ @'id'@
    -- [__Composition__]: @'contramap' f '.' 'contramap' g@ ≡ @'contramap' (g '.' f)@
    contravariantLaws ::
      ( Contravariant f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Laws
    contravariantLaws :: forall (f :: * -> *).
    (Contravariant f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Laws
    contravariantLaws forall x. Gen x -> Gen (f x)
    gen = String -> [(String, Property)] -> Laws
    Laws String
    "Contravariant"
      [ (String
    "Identity", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Contravariant f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    contravariantIdentity Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      , (String
    "Composition", (forall x. Gen x -> Gen (f x)) -> Property
    forall (f :: * -> *).
    (Contravariant f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    contravariantComposition Gen x -> Gen (f x)
    forall x. Gen x -> Gen (f x)
    gen)
      ]

    contravariantIdentity ::
      ( Contravariant f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    contravariantIdentity :: forall (f :: * -> *).
    (Contravariant f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    contravariantIdentity forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      a <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      let lhs = (Integer -> Integer) -> f Integer -> f Integer
    forall a' a. (a' -> a) -> f a -> f a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap Integer -> Integer
    forall a. a -> a
    id f Integer
    a
      let rhs = f Integer -> f Integer
    forall a. a -> a
    id f Integer
    a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Identity", lawContextLawBody :: String
    lawContextLawBody = String
    "contramap id" String -> String -> String
    `congruency` String
    "id"
            , lawContextTcName :: String
    lawContextTcName = String
    "Contravariant", lawContextTcProp :: String
    lawContextTcProp =
                let showA :: String
    showA = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    a
                in [String] -> String
    lawWhere
                  [ String
    "contramap id x" String -> String -> String
    `congruency` String
    "id x, where"
                  , String
    "x = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                  ]
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            }
      heqCtx1 lhs rhs ctx

    contravariantComposition ::
      ( Contravariant f
      , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
      ) => (forall x. Gen x -> Gen (f x)) -> Property
    contravariantComposition :: forall (f :: * -> *).
    (Contravariant f, forall x. Eq x => Eq (f x),
     forall x. Show x => Show (f x)) =>
    (forall x. Gen x -> Gen (f x)) -> Property
    contravariantComposition forall x. Gen x -> Gen (f x)
    fgen = HasCallStack => PropertyT IO () -> Property
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      a <- Gen (f Integer) -> PropertyT IO (f Integer)
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll (Gen (f Integer) -> PropertyT IO (f Integer))
    -> Gen (f Integer) -> PropertyT IO (f Integer)
    forall a b. (a -> b) -> a -> b
    $ Gen Integer -> Gen (f Integer)
    forall x. Gen x -> Gen (f x)
    fgen Gen Integer
    genSmallInteger
      f' <- forAll genQuadraticEquation
      g' <- forAll genQuadraticEquation
      let f = QuadraticEquation -> Integer -> Integer
    runQuadraticEquation QuadraticEquation
    f'
      let g = QuadraticEquation -> Integer -> Integer
    runQuadraticEquation QuadraticEquation
    g'
      let lhs = (Integer -> Integer) -> f Integer -> f Integer
    forall a' a. (a' -> a) -> f a -> f a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap Integer -> Integer
    f ((Integer -> Integer) -> f Integer -> f Integer
    forall a' a. (a' -> a) -> f a -> f a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap Integer -> Integer
    g f Integer
    a)
      let rhs = (Integer -> Integer) -> f Integer -> f Integer
    forall a' a. (a' -> a) -> f a -> f a'
    forall (f :: * -> *) a' a.
    Contravariant f =>
    (a' -> a) -> f a -> f a'
    contramap (Integer -> Integer
    g (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer
    f) f Integer
    a
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    forall a b. (a -> b) -> a -> b
    $ LawContext
            { lawContextLawName :: String
    lawContextLawName = String
    "Composition", lawContextLawBody :: String
    lawContextLawBody = String
    "contramap f . contramap g" String -> String -> String
    `congruency` String
    "contramap (g . f)"
            , lawContextTcName :: String
    lawContextTcName = String
    "Contravariant", lawContextTcProp :: String
    lawContextTcProp =
                let showF :: String
    showF = QuadraticEquation -> String
    forall a. Show a => a -> String
    show QuadraticEquation
    f'; showG :: String
    showG = QuadraticEquation -> String
    forall a. Show a => a -> String
    show QuadraticEquation
    g'; showA :: String
    showA = f Integer -> String
    forall a. Show a => a -> String
    show f Integer
    a;
                in [String] -> String
    lawWhere
                     [ String
    "contramap f . contramap g $ a" String -> String -> String
    `congruency` String
    "contramap (g . f) a, where"
                     , String
    "f = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showF
                     , String
    "g = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showG
                     , String
    "a = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    showA
                     ]
            , lawContextReduced :: String
    lawContextReduced = f Integer -> f Integer -> String
    forall a. Show a => a -> a -> String
    reduced f Integer
    lhs f Integer
    rhs
            }
      heqCtx1 lhs rhs ctx