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

#ifndef HAVE_COMONAD

module Hedgehog.Classes.Comonad () where

#else

module Hedgehog.Classes.Comonad (comonadLaws) where

import Control.Comonad

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'Comonad' laws:
--
-- [__Extend/Extract Identity__]: @'extend' 'extract' ≡ 'id'@
-- [__Extract/Extend__]: @'extract' '.' 'extend' f ≡ f@
-- [__Extend/Extend__]: @'extend' f '.' 'extend' g ≡ 'extend' (f '.' 'extend' g)@
-- [__Extract Right Identity__]: @f '=>=' 'extract' ≡ f@
-- [__Extract Left Identity__]: @'extract' '=>=' f ≡ f@
-- [__Cokleisli Associativity__]: @(f '=>=' g) '=>=' h ≡ f '=>=' (g '=>=' h)@
-- [__Extract/Duplicate Identity__]: @'extract' '.' 'duplicate' ≡ 'id'@
-- [__Fmap Extract/Duplicate Identity__]: @'fmap' 'extract' '.' 'duplicate' ≡ 'id'@
-- [__Double Duplication__]: @'duplicate' '.' 'duplicate' ≡ 'fmap' 'duplicate' '.' 'duplicate'@
-- [__Extend/Fmap . Duplicate Identity__]: @'extend' f ≡ 'fmap' f '.' 'duplicate'@
-- [__Duplicate/Extend id Identity__]: @'duplicate' ≡ 'extend' 'id'@
-- [__Fmap/Extend Extract__]: @'fmap' f ≡ 'extend' (f '.' 'extract')@
-- [__Fmap/LiftW Isomorphism__]: @'fmap' ≡ 'liftW'@
comonadLaws ::
  ( Comonad f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Laws
comonadLaws :: (forall x. Gen x -> Gen (f x)) -> Laws
comonadLaws forall x. Gen x -> Gen (f x)
gen = String -> [(String, Property)] -> Laws
Laws String
"Comonad"
  [ (String
"Extend/Extract Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
extendExtractIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract/Extend", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
extractExtend forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extend/Extend", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
extendExtend forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract Right Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
extractRightIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract Left Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
extractLeftIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Cokleisli Associativity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
cokleisliAssociativity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract/Duplicate Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
extractDuplicateIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Fmap Extract/Duplicate Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
fmapExtractDuplicateIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Double Duplication", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
doubleDup forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extend/Fmap . Duplicate Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
extendDuplicate forall x. Gen x -> Gen (f x)
gen)
  , (String
"Duplicate/Extend id Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
duplicateExtendId forall x. Gen x -> Gen (f x)
gen)
  , (String
"Fmap/Extend Extract", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
fmapExtendExtract forall x. Gen x -> Gen (f x)
gen)
  , (String
"Fmap/LiftW Isomorphism", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). ComonadProp f
fmapLiftW forall x. Gen x -> Gen (f x)
gen)
  ]

type ComonadProp f =
  ( Comonad f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Property

extendExtractIdentity :: forall f. ComonadProp f
extendExtractIdentity :: (forall x. Gen x -> Gen (f x)) -> Property
extendExtractIdentity 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
  f Integer
x <- 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 :: f Integer
lhs = (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
forall (w :: * -> *) a. Comonad w => w a -> a
extract f Integer
x
  let rhs :: f Integer
rhs = f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Extend/Extract Identity", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"extend extract" String -> String -> String
`congruency` String
"id"
        , lawContextReduced :: String
lawContextReduced = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"extend extract x" String -> String -> String
`congruency` String
"x, where"
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

extractExtend :: forall f. ComonadProp f
extractExtend :: (forall x. Gen x -> Gen (f x)) -> Property
extractExtend 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
  f Integer
x <- 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
  LinearEquationW f
k <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  let k' :: f Integer -> Integer
k' = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
k
  let lhs :: Integer
lhs = f Integer -> Integer
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f Integer -> Integer)
-> (f Integer -> f Integer) -> f Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
k' (f Integer -> Integer) -> f Integer -> Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: Integer
rhs = f Integer -> Integer
k' f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Extract/Extend", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"extract . extend f" String -> String -> String
`congruency` String
"f"
        , lawContextReduced :: String
lawContextReduced = Integer -> Integer -> String
forall a. Show a => a -> a -> String
reduced Integer
lhs Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"extract . extend f $ x" String -> String -> String
`congruency` String
"f x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
k
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  Integer -> Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Integer
lhs Integer
rhs Context
ctx

extendExtend :: forall f. ComonadProp f
extendExtend :: (forall x. Gen x -> Gen (f x)) -> Property
extendExtend 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
  f Integer
x <- 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
  LinearEquationW f
f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  LinearEquationW f
g' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  let f :: f Integer -> Integer
f = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let g :: f Integer -> Integer
g = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
g'
  let lhs :: f Integer
lhs = (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
f (f Integer -> f Integer)
-> (f Integer -> f Integer) -> f Integer -> f Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
g (f Integer -> f Integer) -> f Integer -> f Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f Integer
rhs = (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (f Integer -> Integer
f (f Integer -> Integer)
-> (f Integer -> f Integer) -> f Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
g) f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Extend/Extend", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"extend f . extend g" String -> String -> String
`congruency` String
"extend (f . extend g)"
        , lawContextReduced :: String
lawContextReduced = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"extend f . extend g $ x" String -> String -> String
`congruency` String
"extend (f . extend g) $ x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"g = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
g'
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

extractRightIdentity :: forall f. ComonadProp f
extractRightIdentity :: (forall x. Gen x -> Gen (f x)) -> Property
extractRightIdentity 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
  f Integer
x <- 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
  LinearEquationW f
f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  let f :: f Integer -> Integer
f = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let lhs :: Integer
lhs = f Integer -> Integer
f (f Integer -> Integer)
-> (f Integer -> Integer) -> f Integer -> Integer
forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f Integer -> Integer) -> f Integer -> Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: Integer
rhs = f Integer -> Integer
f f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Extract Cokleisli Right Identity", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"f =>= extract" String -> String -> String
`congruency` String
"f"
        , lawContextReduced :: String
lawContextReduced = Integer -> Integer -> String
forall a. Show a => a -> a -> String
reduced Integer
lhs Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"f =>= extract $ x" String -> String -> String
`congruency` String
"f x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  Integer -> Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Integer
lhs Integer
rhs Context
ctx

extractLeftIdentity :: forall f. ComonadProp f
extractLeftIdentity :: (forall x. Gen x -> Gen (f x)) -> Property
extractLeftIdentity 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
  f Integer
x <- 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
  LinearEquationW f
f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  let f :: f Integer -> Integer
f = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let lhs :: Integer
lhs = f Integer -> Integer
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f Integer -> Integer)
-> (f Integer -> Integer) -> f Integer -> Integer
forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
f (f Integer -> Integer) -> f Integer -> Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: Integer
rhs = f Integer -> Integer
f f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Extract Cokleisli Left Identity", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"extract =>= f" String -> String -> String
`congruency` String
"f"
        , lawContextReduced :: String
lawContextReduced = Integer -> Integer -> String
forall a. Show a => a -> a -> String
reduced Integer
lhs Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"extract =>= f $ x" String -> String -> String
`congruency` String
"f x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  Integer -> Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Integer
lhs Integer
rhs Context
ctx

cokleisliAssociativity :: forall f. ComonadProp f
cokleisliAssociativity :: (forall x. Gen x -> Gen (f x)) -> Property
cokleisliAssociativity 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
  f Integer
x <- 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
  LinearEquationW f
f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  LinearEquationW f
g' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  LinearEquationW f
h' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  let f :: f Integer -> Integer
f = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let g :: f Integer -> Integer
g = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
g'
  let h :: f Integer -> Integer
h = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
h'
  let lhs :: Integer
lhs = (f Integer -> Integer
f (f Integer -> Integer)
-> (f Integer -> Integer) -> f Integer -> Integer
forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
g) (f Integer -> Integer)
-> (f Integer -> Integer) -> f Integer -> Integer
forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
h (f Integer -> Integer) -> f Integer -> Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: Integer
rhs = f Integer -> Integer
f (f Integer -> Integer)
-> (f Integer -> Integer) -> f Integer -> Integer
forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= (f Integer -> Integer
g (f Integer -> Integer)
-> (f Integer -> Integer) -> f Integer -> Integer
forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
h) (f Integer -> Integer) -> f Integer -> Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Cokleisli Associativity", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"(f =>= g) =>= h" String -> String -> String
`congruency` String
"f =>= (g =>= h)"
        , lawContextReduced :: String
lawContextReduced = Integer -> Integer -> String
forall a. Show a => a -> a -> String
reduced Integer
lhs Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"(f =>= g) =>= h $ x" String -> String -> String
`congruency` String
"f =>= (g =>= h) $ x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"g = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
g'
            , String
"h = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
h'
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  Integer -> Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Integer
lhs Integer
rhs Context
ctx


extractDuplicateIdentity :: forall f. ComonadProp f
extractDuplicateIdentity :: (forall x. Gen x -> Gen (f x)) -> Property
extractDuplicateIdentity 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
  f Integer
x <- 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 :: f Integer
lhs = f (f Integer) -> f Integer
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f (f Integer) -> f Integer)
-> (f Integer -> f (f Integer)) -> f Integer -> f Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Integer -> f (f Integer)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (f Integer -> f Integer) -> f Integer -> f Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f Integer
rhs = f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Extract/Duplicate Identity", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"extract . duplicate" String -> String -> String
`congruency` String
"id"
        , lawContextReduced :: String
lawContextReduced = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"extract . duplicate $ x" String -> String -> String
`congruency` String
"x, where"
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

fmapExtractDuplicateIdentity :: forall f. ComonadProp f
fmapExtractDuplicateIdentity :: (forall x. Gen x -> Gen (f x)) -> Property
fmapExtractDuplicateIdentity 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
  f Integer
x <- 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 :: f Integer
lhs = (f Integer -> Integer) -> f (f Integer) -> f Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f Integer -> Integer
forall (w :: * -> *) a. Comonad w => w a -> a
extract (f (f Integer) -> f Integer)
-> (f Integer -> f (f Integer)) -> f Integer -> f Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Integer -> f (f Integer)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (f Integer -> f Integer) -> f Integer -> f Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f Integer
rhs = f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Fmap Extract/Duplicate Identity", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"fmap extract . duplicate" String -> String -> String
`congruency` String
"id"
        , lawContextReduced :: String
lawContextReduced = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"fmap extract . duplicate $ x" String -> String -> String
`congruency` String
"x, where"
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

doubleDup :: forall f. ComonadProp f
doubleDup :: (forall x. Gen x -> Gen (f x)) -> Property
doubleDup 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
  f Integer
x <- 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 :: f (f (f Integer))
lhs = f (f Integer) -> f (f (f Integer))
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (f (f Integer) -> f (f (f Integer)))
-> (f Integer -> f (f Integer)) -> f Integer -> f (f (f Integer))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Integer -> f (f Integer)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (f Integer -> f (f (f Integer))) -> f Integer -> f (f (f Integer))
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f (f (f Integer))
rhs = (f Integer -> f (f Integer)) -> f (f Integer) -> f (f (f Integer))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f Integer -> f (f Integer)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (f (f Integer) -> f (f (f Integer)))
-> (f Integer -> f (f Integer)) -> f Integer -> f (f (f Integer))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Integer -> f (f Integer)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (f Integer -> f (f (f Integer))) -> f Integer -> f (f (f Integer))
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Double Duplicate", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"duplicate . duplicate" String -> String -> String
`congruency` String
"fmap duplicate . duplicate"
        , lawContextReduced :: String
lawContextReduced = f (f (f Integer)) -> f (f (f Integer)) -> String
forall a. Show a => a -> a -> String
reduced f (f (f Integer))
lhs f (f (f Integer))
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"duplicate . duplicate $ x" String -> String -> String
`congruency` String
"fmap duplicate . duplicate $ x, where"
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f (f (f Integer))
-> f (f (f Integer)) -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f (f (f Integer))
lhs f (f (f Integer))
rhs Context
ctx

extendDuplicate :: forall f. ComonadProp f
extendDuplicate :: (forall x. Gen x -> Gen (f x)) -> Property
extendDuplicate 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
  f Integer
x <- 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
  LinearEquationW f
f' <- Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f))
-> Gen (LinearEquationW f) -> PropertyT IO (LinearEquationW f)
forall a b. (a -> b) -> a -> b
$ (forall x. Gen x -> Gen (f x)) -> Gen (LinearEquationW f)
forall (w :: * -> *).
Comonad w =>
(forall x. Gen x -> Gen (w x)) -> Gen (LinearEquationW w)
genLinearEquationW forall x. Gen x -> Gen (f x)
fgen
  let f :: f Integer -> Integer
f = LinearEquationW f -> f Integer -> Integer
forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let lhs :: f Integer
lhs = (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
f (f Integer -> f Integer) -> f Integer -> f Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f Integer
rhs = (f Integer -> Integer) -> f (f Integer) -> f Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f Integer -> Integer
f (f (f Integer) -> f Integer)
-> (f Integer -> f (f Integer)) -> f Integer -> f Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Integer -> f (f Integer)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (f Integer -> f Integer) -> f Integer -> f Integer
forall a b. (a -> b) -> a -> b
$ f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Extend/Fmap Duplicate", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"extend f" String -> String -> String
`congruency` String
"fmap f . duplicate"
        , lawContextReduced :: String
lawContextReduced = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"extend f x" String -> String -> String
`congruency` String
"fmap f . duplicate $ x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquationW f -> String
forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

duplicateExtendId :: forall f. ComonadProp f
duplicateExtendId :: (forall x. Gen x -> Gen (f x)) -> Property
duplicateExtendId 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
  f Integer
x <- 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 :: f (f Integer)
lhs = f Integer -> f (f Integer)
forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate f Integer
x
  let rhs :: f (f Integer)
rhs = (f Integer -> f Integer) -> f Integer -> f (f Integer)
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> f Integer
forall a. a -> a
id f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Duplicate/Extend Id", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"duplicate" String -> String -> String
`congruency` String
"extend id"
        , lawContextReduced :: String
lawContextReduced = f (f Integer) -> f (f Integer) -> String
forall a. Show a => a -> a -> String
reduced f (f Integer)
lhs f (f Integer)
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"duplicate x" String -> String -> String
`congruency` String
"extend id x, where"
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f (f Integer) -> f (f Integer) -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f (f Integer)
lhs f (f Integer)
rhs Context
ctx

fmapExtendExtract :: forall f. ComonadProp f
fmapExtendExtract :: (forall x. Gen x -> Gen (f x)) -> Property
fmapExtendExtract 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
  f Integer
x :: f Integer <- 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
  LinearEquation
f' <- Gen LinearEquation -> PropertyT IO LinearEquation
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen LinearEquation
genLinearEquation
  let f :: Integer -> Integer
f = LinearEquation -> Integer -> Integer
runLinearEquation LinearEquation
f'
  let lhs :: f Integer
lhs = (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f f Integer
x
  let rhs :: f Integer
rhs = (f Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (Integer -> Integer
f (Integer -> Integer)
-> (f Integer -> Integer) -> f Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Integer -> Integer
forall (w :: * -> *) a. Comonad w => w a -> a
extract) f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Fmap/Extend Extract", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"fmap f" String -> String -> String
`congruency` String
"extend (f . extract)"
        , lawContextReduced :: String
lawContextReduced = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"fmap f x" String -> String -> String
`congruency` String
"extend (f . extract) x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquation -> String
forall a. Show a => a -> String
show LinearEquation
f'
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

fmapLiftW :: forall f. ComonadProp f
fmapLiftW :: (forall x. Gen x -> Gen (f x)) -> Property
fmapLiftW 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
  f Integer
x <- 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
  LinearEquation
f' <- Gen LinearEquation -> PropertyT IO LinearEquation
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen LinearEquation
genLinearEquation
  let f :: Integer -> Integer
f = LinearEquation -> Integer -> Integer
runLinearEquation LinearEquation
f'
  let lhs :: f Integer
lhs = (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f f Integer
x
  let rhs :: f Integer
rhs = (Integer -> Integer) -> f Integer -> f Integer
forall (w :: * -> *) a b. Comonad w => (a -> b) -> w a -> w b
liftW Integer -> Integer
f f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Fmap/LiftW", lawContextTcName :: String
lawContextTcName = String
"Comonad"
        , lawContextLawBody :: String
lawContextLawBody = String
"fmap" String -> String -> String
`congruency` String
"liftW"
        , lawContextReduced :: String
lawContextReduced = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp = [String] -> String
lawWhere
            [ String
"fmap f x" String -> String -> String
`congruency` String
"liftW f x, where"
            , String
"f = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LinearEquation -> String
forall a. Show a => a -> String
show LinearEquation
f'
            , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ f Integer -> String
forall a. Show a => a -> String
show f Integer
x
            ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

#endif