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

module Hedgehog.Classes.Arrow (arrowLaws) where

import Hedgehog
import Hedgehog.Classes.Common

import Control.Arrow(Arrow(..), (>>>))
import Control.Category(Category(..))
import Prelude hiding (id, (.))
import qualified Prelude

-- | Tests the following 'Arrow' laws:
--
-- [__Arr Identity__]: @'arr' 'id'@ ≡ @'id'@
-- [__Arr Composition__]: @'arr' (f '>>>' g)@ ≡ @'arr' f '>>>' 'arr' g@
-- [__Arr-First inverse__]: @'first' ('arr' f)@ ≡ @'arr' ('first' f)@
-- [__First Composition__]: @'first' (f '>>>' g)@ ≡ @'first' f '>>>' 'first' g@
-- [__Arrow Law 5__]: @'first' f '>>>' 'arr' 'fst'@ ≡ @'arr' 'fst' '>>>' f@
-- [__Arrow Law 6__]: @'first' f '>>>' 'arr' ('id' '***' g)@ ≡ @'arr' ('id' '***' g) '>>>' 'first' f@
-- [__Arrow Law 7__]: @'first' ('first' f) '>>>' 'arr' assoc@ ≡ @'arr' assoc '>>>' 'first' f, where assoc ((a,b),c) = (a,(b,c))@
arrowLaws :: forall f.
  ( Arrow f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
arrowLaws :: forall (f :: * -> * -> *).
(Arrow f, forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
arrowLaws forall x y. Gen x -> Gen y -> Gen (f x y)
gen = String -> [(String, Property)] -> Laws
Laws String
"Arrow"
  [ (String
"Arr Identity", forall (f :: * -> * -> *). ArrowProp f
arrowLaw1 forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Arr Composition", forall (f :: * -> * -> *). ArrowProp f
arrowLaw2 forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Arr . First == First . Arr", forall (f :: * -> * -> *). ArrowProp f
arrowLaw3 forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"First Composition", forall (f :: * -> * -> *). ArrowProp f
arrowLaw4 forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Arrow Law 5", forall (f :: * -> * -> *). ArrowProp f
arrowLaw5 forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Arrow Law 6", forall (f :: * -> * -> *). ArrowProp f
arrowLaw6 forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  , (String
"Arrow Law 7", forall (f :: * -> * -> *). ArrowProp f
arrowLaw7 forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
  ]

type ArrowProp f =
  ( Arrow f
  , forall x y. (Eq x, Eq y) => Eq (f x y)
  , forall x y. (Show x, Show y) => Show (f x y)
  ) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property

arrowLaw1 :: forall f. ArrowProp f
arrowLaw1 :: forall (f :: * -> * -> *). ArrowProp f
arrowLaw1 forall x y. Gen x -> Gen y -> Gen (f x y)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a. a -> a
Prelude.id forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` (forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id :: f Integer Integer)

arrowLaw2 :: forall f. ArrowProp f
arrowLaw2 :: forall (f :: * -> * -> *). ArrowProp f
arrowLaw2 forall x y. Gen x -> Gen y -> Gen (f x y)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  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'
      g :: Integer -> Integer
g = QuadraticEquation -> Integer -> Integer
runQuadraticEquation QuadraticEquation
g'
  (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (Integer -> Integer
f forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Integer -> Integer
g) :: f Integer Integer) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Integer -> Integer
f forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Integer -> Integer
g) 

arrowLaw3 :: forall f. ArrowProp f
arrowLaw3 :: forall (f :: * -> * -> *). ArrowProp f
arrowLaw3 forall x y. Gen x -> Gen y -> Gen (f x y)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  QuadraticEquation
f' <- 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 x :: f (Integer, Integer) (Integer, Integer)
x = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr Integer -> Integer
f) :: f (Integer, Integer) (Integer, Integer)
  let y :: f (Integer, Integer) (Integer, Integer)
y = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Integer -> Integer
f) :: f (Integer, Integer) (Integer, Integer) 
  f (Integer, Integer) (Integer, Integer)
x forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f (Integer, Integer) (Integer, Integer)
y

arrowLaw4 :: forall f. ArrowProp f
arrowLaw4 :: forall (f :: * -> * -> *). ArrowProp f
arrowLaw4 forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  f Integer Integer
g <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  let x :: f (Integer, Integer) (Integer, Integer)
x = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (f Integer Integer
f forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> f Integer Integer
g) :: f (Integer, Integer) (Integer, Integer)
  let y :: f (Integer, Integer) (Integer, Integer)
y = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f Integer Integer
f forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f Integer Integer
g :: f (Integer, Integer) (Integer, Integer)
  f (Integer, Integer) (Integer, Integer)
x forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f (Integer, Integer) (Integer, Integer)
y 

arrowLaw5 :: forall f. ArrowProp f
arrowLaw5 :: forall (f :: * -> * -> *). ArrowProp f
arrowLaw5 forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  let x :: f (Integer, Integer) Integer
x = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f Integer Integer
f forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> a
fst :: f (Integer, Integer) Integer
  let y :: f (Integer, Integer) Integer
y = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> a
fst forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> f Integer Integer
f :: f (Integer, Integer) Integer
  f (Integer, Integer) Integer
x forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f (Integer, Integer) Integer
y 

arrowLaw6 :: forall f. ArrowProp f
arrowLaw6 :: forall (f :: * -> * -> *). ArrowProp f
arrowLaw6 forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  QuadraticEquation
g' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen QuadraticEquation
genQuadraticEquation
  let g :: Integer -> Integer
g = QuadraticEquation -> Integer -> Integer
runQuadraticEquation QuadraticEquation
g'
  let x :: f (Integer, Integer) (Integer, Integer)
x = ((forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f Integer Integer
f) forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall a. a -> a
Prelude.id forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Integer -> Integer
g))) :: f (Integer, Integer) (Integer, Integer) 
  let y :: f (Integer, Integer) (Integer, Integer)
y = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Integer -> Integer
g) forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f Integer Integer
f :: f (Integer, Integer) (Integer, Integer) 
  f (Integer, Integer) (Integer, Integer)
x forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f (Integer, Integer) (Integer, Integer)
y

arrowLaw7 :: forall f. ArrowProp f
arrowLaw7 :: forall (f :: * -> * -> *). ArrowProp f
arrowLaw7 forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  let assoc :: ((a, a), b) -> (a, (a, b))
assoc ((a
a,a
b),b
c) = (a
a,(a
b,b
c))
  f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
  let x :: f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
x = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f Integer Integer
f) forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall {a} {a} {b}. ((a, a), b) -> (a, (a, b))
assoc :: f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
  let y :: f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
y = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall {a} {a} {b}. ((a, a), b) -> (a, (a, b))
assoc forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f Integer Integer
f :: f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
  f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
x forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
 forall x y. (Eq x, Eq y) => Eq (f x y),
 forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f ((Integer, Integer), Integer) (Integer, (Integer, Integer))
y