{-# 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
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
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
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
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
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
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
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
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