{-# 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 (f :: * -> *).
(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)
gen = String -> [(String, Property)] -> Laws
Laws String
"Comonad"
  [ (String
"Extend/Extract Identity", forall (f :: * -> *). ComonadProp f
extendExtractIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract/Extend", forall (f :: * -> *). ComonadProp f
extractExtend forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extend/Extend", forall (f :: * -> *). ComonadProp f
extendExtend forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract Right Identity", forall (f :: * -> *). ComonadProp f
extractRightIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract Left Identity", forall (f :: * -> *). ComonadProp f
extractLeftIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Cokleisli Associativity", forall (f :: * -> *). ComonadProp f
cokleisliAssociativity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extract/Duplicate Identity", forall (f :: * -> *). ComonadProp f
extractDuplicateIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Fmap Extract/Duplicate Identity", forall (f :: * -> *). ComonadProp f
fmapExtractDuplicateIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Double Duplication", forall (f :: * -> *). ComonadProp f
doubleDup forall x. Gen x -> Gen (f x)
gen)
  , (String
"Extend/Fmap . Duplicate Identity", forall (f :: * -> *). ComonadProp f
extendDuplicate forall x. Gen x -> Gen (f x)
gen)
  , (String
"Duplicate/Extend id Identity", forall (f :: * -> *). ComonadProp f
duplicateExtendId forall x. Gen x -> Gen (f x)
gen)
  , (String
"Fmap/Extend Extract", forall (f :: * -> *). ComonadProp f
fmapExtendExtract forall x. Gen x -> Gen (f x)
gen)
  , (String
"Fmap/LiftW Isomorphism", 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 (f :: * -> *). ComonadProp f
extendExtractIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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 (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
extractExtend forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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
  LinearEquationW f
k <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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' = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
k
  let lhs :: Integer
lhs = forall (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
k' 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
k
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
extendExtend forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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
  LinearEquationW f
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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 = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let g :: f Integer -> Integer
g = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
g'
  let lhs :: f Integer
lhs = forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
g forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f Integer
rhs = forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (f Integer -> Integer
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"g = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
g'
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
extractRightIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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
  LinearEquationW f
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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 = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let lhs :: Integer
lhs = f Integer -> Integer
f forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= forall (w :: * -> *) a. Comonad w => w a -> a
extract 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
extractLeftIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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
  LinearEquationW f
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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 = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let lhs :: Integer
lhs = forall (w :: * -> *) a. Comonad w => w a -> a
extract forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
f 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
cokleisliAssociativity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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
  LinearEquationW f
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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 = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let g :: f Integer -> Integer
g = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
g'
  let h :: f Integer -> Integer
h = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
h'
  let lhs :: Integer
lhs = (f Integer -> Integer
f forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
g) forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
h forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: Integer
rhs = f Integer -> Integer
f forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= (f Integer -> Integer
g forall (w :: * -> *) a b c.
Comonad w =>
(w a -> b) -> (w b -> c) -> w a -> c
=>= f Integer -> Integer
h) forall a b. (a -> b) -> a -> b
$ f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"g = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
g'
            , String
"h = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
h'
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
extractDuplicateIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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 (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
fmapExtractDuplicateIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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 b. Functor f => (a -> b) -> f a -> f b
fmap forall (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
doubleDup forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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 (f (f Integer))
lhs = forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f (f (f Integer))
rhs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate forall a b. (a -> b) -> a -> b
$ f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
extendDuplicate forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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
  LinearEquationW f
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ 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 = forall (w :: * -> *).
Comonad w =>
LinearEquationW w -> w Integer -> Integer
runLinearEquationW LinearEquationW f
f'
  let lhs :: f Integer
lhs = forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend f Integer -> Integer
f forall a b. (a -> b) -> a -> b
$ f Integer
x
  let rhs :: f Integer
rhs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f Integer -> Integer
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate forall a b. (a -> b) -> a -> b
$ f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquationW f
f'
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
duplicateExtendId forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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 (f Integer)
lhs = forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate f Integer
x
  let rhs :: f (f Integer)
rhs = forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend forall a. a -> a
id f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
fmapExtendExtract forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x :: f Integer <- 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
  LinearEquation
f' <- 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f f Integer
x
  let rhs :: f Integer
rhs = forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (Integer -> Integer
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> a
extract) f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquation
f'
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  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 (f :: * -> *). ComonadProp f
fmapLiftW forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
x <- 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
  LinearEquation
f' <- 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f f Integer
x
  let rhs :: f Integer
rhs = 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 forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LinearEquation
f'
            , String
"x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f Integer
x
            ]
        }
  forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx f Integer
lhs f Integer
rhs Context
ctx

#endif