{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}

#if HAVE_QUANTIFIED_CONSTRAINTS
{-# LANGUAGE QuantifiedConstraints #-}
#endif

{-# OPTIONS_GHC -Wall #-}

module Test.QuickCheck.Classes.Applicative
  (
#if HAVE_UNARY_LAWS
    applicativeLaws
#endif
  ) where

import Control.Applicative
import Test.QuickCheck hiding ((.&.))
#if HAVE_UNARY_LAWS
import Test.QuickCheck.Arbitrary (Arbitrary1(..))
import Data.Functor.Classes (Eq1,Show1)
#endif
import Test.QuickCheck.Property (Property)

import Test.QuickCheck.Classes.Internal

#if HAVE_UNARY_LAWS

-- | Tests the following applicative properties:
--
-- [/Identity/]
--   @'pure' 'id' '<*>' v ≡ v@
-- [/Composition/]
--   @'pure' ('.') '<*>' u '<*>' v '<*>' w ≡ u '<*>' (v '<*>' w)@
-- [/Homomorphism/]
--   @'pure' f '<*>' 'pure' x ≡ 'pure' (f x)@
-- [/Interchange/]
--   @u '<*>' 'pure' y ≡ 'pure' ('$' y) '<*>' u@
-- [/LiftA2 (1)/]
--   @('<*>') ≡ 'liftA2' 'id'@
applicativeLaws ::
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Applicative f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Laws
applicativeLaws :: proxy f -> Laws
applicativeLaws proxy f
p = String -> [(String, Property)] -> Laws
Laws String
"Applicative"
  [ (String
"Identity", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Applicative f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
applicativeIdentity proxy f
p)
  , (String
"Composition", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Applicative f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
applicativeComposition proxy f
p)
  , (String
"Homomorphism", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Applicative f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a)) =>
proxy f -> Property
applicativeHomomorphism proxy f
p)
  , (String
"Interchange", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Applicative f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
applicativeInterchange proxy f
p)
  , (String
"LiftA2 Part 1", proxy f -> Property
forall (proxy :: (* -> *) -> *) (f :: * -> *).
(Applicative f, forall a. Eq a => Eq (f a),
 forall a. Show a => Show (f a),
 forall a. Arbitrary a => Arbitrary (f a)) =>
proxy f -> Property
applicativeLiftA2_1 proxy f
p)
    -- todo: liftA2 part 2, we need an equation of two variables for this
  ]

applicativeIdentity :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Applicative f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
applicativeIdentity :: proxy f -> Property
applicativeIdentity proxy f
_ = (Apply f Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply f Integer -> Bool) -> Property)
-> (Apply f Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f Integer
a :: f Integer)) -> f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 ((Integer -> Integer) -> f (Integer -> Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer -> Integer
forall a. a -> a
id f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
a) f Integer
a

applicativeComposition :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Applicative f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
applicativeComposition :: proxy f -> Property
applicativeComposition proxy f
_ = (Apply f QuadraticEquation
 -> Apply f QuadraticEquation -> Apply f Integer -> Bool)
-> Property
forall prop. Testable prop => prop -> Property
property ((Apply f QuadraticEquation
  -> Apply f QuadraticEquation -> Apply f Integer -> Bool)
 -> Property)
-> (Apply f QuadraticEquation
    -> Apply f QuadraticEquation -> Apply f Integer -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f QuadraticEquation
u' :: f QuadraticEquation)) (Apply (f QuadraticEquation
v' :: f QuadraticEquation)) (Apply (f Integer
w :: f Integer)) ->
  let u :: f (Integer -> Integer)
u = (QuadraticEquation -> Integer -> Integer)
-> f QuadraticEquation -> f (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QuadraticEquation -> Integer -> Integer
runQuadraticEquation f QuadraticEquation
u'
      v :: f (Integer -> Integer)
v = (QuadraticEquation -> Integer -> Integer)
-> f QuadraticEquation -> f (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QuadraticEquation -> Integer -> Integer
runQuadraticEquation f QuadraticEquation
v'
   in f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (((Integer -> Integer)
 -> (Integer -> Integer) -> Integer -> Integer)
-> f ((Integer -> Integer)
      -> (Integer -> Integer) -> Integer -> Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) f ((Integer -> Integer)
   -> (Integer -> Integer) -> Integer -> Integer)
-> f (Integer -> Integer)
-> f ((Integer -> Integer) -> Integer -> Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Integer -> Integer)
u f ((Integer -> Integer) -> Integer -> Integer)
-> f (Integer -> Integer) -> f (Integer -> Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Integer -> Integer)
v f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
w) (f (Integer -> Integer)
u f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (f (Integer -> Integer)
v f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
w))

applicativeHomomorphism :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a))
#else
  (Applicative f, Eq1 f, Show1 f)
#endif
  => proxy f -> Property
applicativeHomomorphism :: proxy f -> Property
applicativeHomomorphism proxy f
_ = (QuadraticEquation -> Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((QuadraticEquation -> Integer -> Bool) -> Property)
-> (QuadraticEquation -> Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(QuadraticEquation
e :: QuadraticEquation) (Integer
a :: Integer) ->
  let f :: Integer -> Integer
f = QuadraticEquation -> Integer -> Integer
runQuadraticEquation QuadraticEquation
e
   in f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 ((Integer -> Integer) -> f (Integer -> Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer -> Integer
f f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> f Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
a) (Integer -> f Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer
f Integer
a) :: f Integer)

applicativeInterchange :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Applicative f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
applicativeInterchange :: proxy f -> Property
applicativeInterchange proxy f
_ = (Apply f QuadraticEquation -> Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply f QuadraticEquation -> Integer -> Bool) -> Property)
-> (Apply f QuadraticEquation -> Integer -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f QuadraticEquation
u' :: f QuadraticEquation)) (Integer
y :: Integer) ->
  let u :: f (Integer -> Integer)
u = (QuadraticEquation -> Integer -> Integer)
-> f QuadraticEquation -> f (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QuadraticEquation -> Integer -> Integer
runQuadraticEquation f QuadraticEquation
u'
   in f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (f (Integer -> Integer)
u f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> f Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
y) (((Integer -> Integer) -> Integer)
-> f ((Integer -> Integer) -> Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
y) f ((Integer -> Integer) -> Integer)
-> f (Integer -> Integer) -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Integer -> Integer)
u)

applicativeLiftA2_1 :: forall proxy f.
#if HAVE_QUANTIFIED_CONSTRAINTS
  (Applicative f, forall a. Eq a => Eq (f a), forall a. Show a => Show (f a), forall a. Arbitrary a => Arbitrary (f a))
#else
  (Applicative f, Eq1 f, Show1 f, Arbitrary1 f)
#endif
  => proxy f -> Property
applicativeLiftA2_1 :: proxy f -> Property
applicativeLiftA2_1 proxy f
_ = (Apply f QuadraticEquation -> Apply f Integer -> Bool) -> Property
forall prop. Testable prop => prop -> Property
property ((Apply f QuadraticEquation -> Apply f Integer -> Bool)
 -> Property)
-> (Apply f QuadraticEquation -> Apply f Integer -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(Apply (f QuadraticEquation
f' :: f QuadraticEquation)) (Apply (f Integer
x :: f Integer)) ->
  let f :: f (Integer -> Integer)
f = (QuadraticEquation -> Integer -> Integer)
-> f QuadraticEquation -> f (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QuadraticEquation -> Integer -> Integer
runQuadraticEquation f QuadraticEquation
f'
   in f Integer -> f Integer -> Bool
forall (f :: * -> *) a.
(forall x. Eq x => Eq (f x), Eq a) =>
f a -> f a -> Bool
eq1 (((Integer -> Integer) -> Integer -> Integer)
-> f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (Integer -> Integer) -> Integer -> Integer
forall a. a -> a
id f (Integer -> Integer)
f f Integer
x) (f (Integer -> Integer)
f f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
x)

#endif