{-# 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 (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)
gen)
  , (String
"Composition", 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)
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
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  let lhs :: f Integer
lhs = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall a. a -> a
id f Integer
a
  let rhs :: f Integer
rhs = forall a. a -> a
id f Integer
a
  let ctx :: Context
ctx = LawContext -> Context
contextualise 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 = 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 = " forall a. [a] -> [a] -> [a]
++ String
showA
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }
  forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
 forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 f Integer
lhs f Integer
rhs Context
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
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  QuadraticEquation
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen QuadraticEquation
genQuadraticEquation
  QuadraticEquation
g' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen QuadraticEquation
genQuadraticEquation
  let f :: Integer -> Integer
f = QuadraticEquation -> Integer -> Integer
runQuadraticEquation QuadraticEquation
f'
  let g :: Integer -> Integer
g = QuadraticEquation -> Integer -> Integer
runQuadraticEquation QuadraticEquation
g'
  let lhs :: f Integer
lhs = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap Integer -> Integer
f (forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap Integer -> Integer
g f Integer
a)
  let rhs :: f Integer
rhs = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (Integer -> Integer
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
f) f Integer
a
  let ctx :: Context
ctx = LawContext -> Context
contextualise 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 = forall a. Show a => a -> String
show QuadraticEquation
f'; showG :: String
showG = forall a. Show a => a -> String
show QuadraticEquation
g'; showA :: String
showA = 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 = " forall a. [a] -> [a] -> [a]
++ String
showF
                 , String
"g = " forall a. [a] -> [a] -> [a]
++ String
showG
                 , String
"a = " forall a. [a] -> [a] -> [a]
++ String
showA
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }
  forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
 forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 f Integer
lhs f Integer
rhs Context
ctx