{-# LANGUAGE QuantifiedConstraints #-}
module Polysemy.Check
(
prepropCommutative
, prepropAllCommutative
, prepropEquivalent
, prepropLaw
, Law (..)
, simpleLaw
, arbitraryAction
, arbitraryActionOfType
, arbitraryActionFromRow
, arbitraryActionFromRowOfType
, SomeAction (..)
, SomeEff (..)
, SomeEffOfType (..)
, constructorLabel
, ExistentialFor
, GArbitraryK
, ArbitraryAction
, ArbitraryEff
, ArbitraryEffOfType
, TypesOf
, send
, deriveGenericK
, GenericK
) where
import Control.Monad (void)
import Generics.Kind (GenericK)
import Generics.Kind.TH (deriveGenericK)
import Polysemy
import Polysemy.Check.Arbitrary
import Polysemy.Check.Orphans ()
import Polysemy.Internal.Union.Inject (Inject, inject)
import Test.QuickCheck
import Data.Data (Data, showConstr, toConstr)
prepropCommutative
:: forall effs1 effs2 r f
. ( forall a. Show a => Show (f a)
, forall a. Eq a => Eq (f a)
)
=> ( ArbitraryEff r r
, ArbitraryEff effs1 r
, ArbitraryEff effs2 r
)
=> (forall a. Sem r a -> IO (f a))
-> Property
prepropCommutative :: forall (effs1 :: EffectRow) (effs2 :: EffectRow) (r :: EffectRow)
(f :: * -> *).
(forall a. Show a => Show (f a), forall a. Eq a => Eq (f a),
ArbitraryEff r r, ArbitraryEff effs1 r, ArbitraryEff effs2 r) =>
(forall a. Sem r a -> IO (f a)) -> Property
prepropCommutative forall a. Sem r a -> IO (f a)
lower = forall prop. Testable prop => prop -> Property
property @(Gen Property) (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
SomeEff e (Sem r) a
m1 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @r @r
SomeEff e (Sem r) a
e1 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs1 @r
SomeEff e (Sem r) a
e2 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs2 @r
SomeEff e (Sem r) a
m2 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @r @r
Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Effects are not commutative!" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"k1 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
m1) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"e1 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
e1) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"e2 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
e2) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"k2 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
m2) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"(k1 >> e1 >> e2 >> k2) /= (k1 >> e2 >> e1 >> k2)" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
f a
r1 <- Sem r a -> IO (f a)
forall a. Sem r a -> IO (f a)
lower (Sem r a -> IO (f a)) -> Sem r a -> IO (f a)
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m1 Sem r a -> Sem r a -> Sem r a
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e1 Sem r a -> Sem r a -> Sem r a
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e2 Sem r a -> Sem r a -> Sem r a
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m2
f a
r2 <- Sem r a -> IO (f a)
forall a. Sem r a -> IO (f a)
lower (Sem r a -> IO (f a)) -> Sem r a -> IO (f a)
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m1 Sem r a -> Sem r a -> Sem r a
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e2 Sem r a -> Sem r a -> Sem r a
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
e1 Sem r a -> Sem r a -> Sem r a
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
m2
Property -> IO Property
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ f a
r1 f a -> f a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f a
r2
class AllCommutative (effs :: EffectRow) r where
prepropAllCommutative
:: ( forall a. Show a => Show (f a)
, forall a. Eq a => Eq (f a)
, Members effs r
)
=> (forall a. Sem r a -> IO (f a))
-> [Property]
instance {-# OVERLAPPING #-} AllCommutative '[e] r where
prepropAllCommutative :: forall (f :: * -> *).
(forall a. Show a => Show (f a), forall a. Eq a => Eq (f a),
Members '[e] r) =>
(forall a. Sem r a -> IO (f a)) -> [Property]
prepropAllCommutative forall a. Sem r a -> IO (f a)
_ = []
instance (ArbitraryEff r r, ArbitraryEff es r, ArbitraryEff '[e] r, AllCommutative es r)
=> AllCommutative (e ': es) r where
prepropAllCommutative :: forall (f :: * -> *).
(forall a. Show a => Show (f a), forall a. Eq a => Eq (f a),
Members (e : es) r) =>
(forall a. Sem r a -> IO (f a)) -> [Property]
prepropAllCommutative forall a. Sem r a -> IO (f a)
lower
= forall (effs1 :: EffectRow) (effs2 :: EffectRow) (r :: EffectRow)
(f :: * -> *).
(forall a. Show a => Show (f a), forall a. Eq a => Eq (f a),
ArbitraryEff r r, ArbitraryEff effs1 r, ArbitraryEff effs2 r) =>
(forall a. Sem r a -> IO (f a)) -> Property
prepropCommutative @'[e] @es @r Sem r a -> IO (f a)
forall a. Sem r a -> IO (f a)
lower
Property -> [Property] -> [Property]
forall a. a -> [a] -> [a]
: forall (effs :: EffectRow) (r :: EffectRow) (f :: * -> *).
(AllCommutative effs r, forall a. Show a => Show (f a),
forall a. Eq a => Eq (f a), Members effs r) =>
(forall a. Sem r a -> IO (f a)) -> [Property]
prepropAllCommutative @es @r Sem r a -> IO (f a)
forall a. Sem r a -> IO (f a)
lower
data Law r z a = Law
{ forall (r :: EffectRow) z a. Law r z a -> Sem r a
lawLhs :: Sem r a
, forall (r :: EffectRow) z a. Law r z a -> Sem r a
lawRhs :: Sem r a
, forall (r :: EffectRow) z a. Law r z a -> [Sem r ()]
lawPrelude :: [Sem r ()]
, forall (r :: EffectRow) z a. Law r z a -> [Sem r z]
lawPostlude :: [Sem r z]
}
simpleLaw :: Sem r a -> Sem r a -> Law r () a
simpleLaw :: forall (r :: EffectRow) a. Sem r a -> Sem r a -> Law r () a
simpleLaw Sem r a
lhs Sem r a
rhs = Sem r a -> Sem r a -> [Sem r ()] -> [Sem r ()] -> Law r () a
forall (r :: EffectRow) z a.
Sem r a -> Sem r a -> [Sem r ()] -> [Sem r z] -> Law r z a
Law Sem r a
lhs Sem r a
rhs [] []
prepropLaw
:: forall effs x r a f
. ( (forall z. Eq z => Eq (f z))
, (forall z. Show z => Show (f z))
)
=> ( Eq a
, Show a
, Functor f
, ArbitraryEff effs r
, Eq x
, Show x
)
=> Gen (Law r x a)
-> Maybe (f a -> String)
-> (forall z. Sem r (a, z) -> IO (f (a, z)))
-> Property
prepropLaw :: forall (effs :: EffectRow) x (r :: EffectRow) a (f :: * -> *).
(forall z. Eq z => Eq (f z), forall z. Show z => Show (f z), Eq a,
Show a, Functor f, ArbitraryEff effs r, Eq x, Show x) =>
Gen (Law r x a)
-> Maybe (f a -> String)
-> (forall z. Sem r (a, z) -> IO (f (a, z)))
-> Property
prepropLaw Gen (Law r x a)
g Maybe (f a -> String)
labeler forall z. Sem r (a, z) -> IO (f (a, z))
lower = forall prop. Testable prop => prop -> Property
property @(Gen Property) (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
Law Sem r a
lhs Sem r a
rhs [Sem r ()]
mprel [Sem r x]
mpost <- Gen (Law r x a)
g
SomeEff e (Sem r) a
pre1 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
Sem r (Maybe ())
prel <- [Sem r ()] -> Gen (Sem r (Maybe ()))
forall (r :: EffectRow) a. [Sem r a] -> Gen (Sem r (Maybe a))
maybeOneof [Sem r ()]
mprel
SomeEff e (Sem r) a
pre2 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
SomeEff e (Sem r) a
post1 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
Sem r (Maybe x)
post <- [Sem r x] -> Gen (Sem r (Maybe x))
forall (r :: EffectRow) a. [Sem r a] -> Gen (Sem r (Maybe a))
maybeOneof [Sem r x]
mpost
SomeEff e (Sem r) a
post2 <- forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"before1 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
pre1) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"before2 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
pre2) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"after1 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
post1) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"after2 = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> e (Sem r) a -> String
forall a. Show a => a -> String
show e (Sem r) a
post2) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
f (a, (Maybe x, a))
a1 <-
Sem r (a, (Maybe x, a)) -> IO (f (a, (Maybe x, a)))
forall z. Sem r (a, z) -> IO (f (a, z))
lower (Sem r (a, (Maybe x, a)) -> IO (f (a, (Maybe x, a))))
-> Sem r (a, (Maybe x, a)) -> IO (f (a, (Maybe x, a)))
forall a b. (a -> b) -> a -> b
$ do
Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
pre1
Sem r (Maybe ()) -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r (Maybe ()) -> Sem r ()) -> Sem r (Maybe ()) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r (Maybe ())
prel
Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
pre2
a
a1 <- Sem r a
lhs
Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
post1
Maybe x
z <- Sem r (Maybe x)
post
a
r <- e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
post2
(a, (Maybe x, a)) -> Sem r (a, (Maybe x, a))
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a1, (Maybe x
z, a
r))
f (a, (Maybe x, a))
a2 <-
Sem r (a, (Maybe x, a)) -> IO (f (a, (Maybe x, a)))
forall z. Sem r (a, z) -> IO (f (a, z))
lower (Sem r (a, (Maybe x, a)) -> IO (f (a, (Maybe x, a))))
-> Sem r (a, (Maybe x, a)) -> IO (f (a, (Maybe x, a)))
forall a b. (a -> b) -> a -> b
$ do
Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
pre1
Sem r (Maybe ()) -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Sem r (Maybe ())
prel
Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
pre2
a
a2 <- Sem r a
rhs
Sem r a -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Sem r a -> Sem r ()) -> Sem r a -> Sem r ()
forall a b. (a -> b) -> a -> b
$ e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
post1
Maybe x
z <- Sem r (Maybe x)
post
a
r <- e (Sem r) a -> Sem r a
forall (e :: Effect) (r :: EffectRow) a.
Member e r =>
e (Sem r) a -> Sem r a
send e (Sem r) a
post2
(a, (Maybe x, a)) -> Sem r (a, (Maybe x, a))
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a2, (Maybe x
z, a
r))
Property -> IO Property
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ (Property -> Property)
-> ((f a -> String) -> Property -> Property)
-> Maybe (f a -> String)
-> Property
-> Property
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Property -> Property
forall prop. Testable prop => prop -> Property
property (\f a -> String
lbl -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
label (String -> Property -> Property) -> String -> Property -> Property
forall a b. (a -> b) -> a -> b
$ f a -> String
lbl (f a -> String) -> f a -> String
forall a b. (a -> b) -> a -> b
$ ((a, (Maybe x, a)) -> a) -> f (a, (Maybe x, a)) -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, (Maybe x, a)) -> a
forall a b. (a, b) -> a
fst f (a, (Maybe x, a))
a1) Maybe (f a -> String)
labeler
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ f (a, (Maybe x, a))
a1 f (a, (Maybe x, a)) -> f (a, (Maybe x, a)) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f (a, (Maybe x, a))
a2
maybeOneof :: [Sem r a] -> Gen (Sem r (Maybe a))
maybeOneof :: forall (r :: EffectRow) a. [Sem r a] -> Gen (Sem r (Maybe a))
maybeOneof [] = Sem r (Maybe a) -> Gen (Sem r (Maybe a))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sem r (Maybe a) -> Gen (Sem r (Maybe a)))
-> Sem r (Maybe a) -> Gen (Sem r (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Sem r (Maybe a)
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
maybeOneof [Sem r a]
res = do
Int
chance <- forall a. [a] -> Gen a
elements @Int [Int
0..Int
9]
case Int
chance Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
8 of
Bool
True -> (Sem r a -> Sem r (Maybe a))
-> Gen (Sem r a) -> Gen (Sem r (Maybe a))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Maybe a) -> Sem r a -> Sem r (Maybe a)
forall a b. (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just) (Gen (Sem r a) -> Gen (Sem r (Maybe a)))
-> Gen (Sem r a) -> Gen (Sem r (Maybe a))
forall a b. (a -> b) -> a -> b
$ [Sem r a] -> Gen (Sem r a)
forall a. [a] -> Gen a
elements [Sem r a]
res
Bool
False -> Sem r (Maybe a) -> Gen (Sem r (Maybe a))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sem r (Maybe a) -> Gen (Sem r (Maybe a)))
-> Sem r (Maybe a) -> Gen (Sem r (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> Sem r (Maybe a)
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
constructorLabel :: Data a => a -> String
constructorLabel :: forall a. Data a => a -> String
constructorLabel = Constr -> String
showConstr (Constr -> String) -> (a -> Constr) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Constr
forall a. Data a => a -> Constr
toConstr
prepropEquivalent
:: forall effs r1 r2 f
. ( forall a. Show a => Show (f a)
, forall a. Eq a => Eq (f a)
)
=> ( Inject effs r1
, Inject effs r2
, Arbitrary (Sem effs Int)
)
=> (forall a. Sem r1 a -> IO (f a))
-> (forall a. Sem r2 a -> IO (f a))
-> Property
prepropEquivalent :: forall (effs :: EffectRow) (r1 :: EffectRow) (r2 :: EffectRow)
(f :: * -> *).
(forall a. Show a => Show (f a), forall a. Eq a => Eq (f a),
Inject effs r1, Inject effs r2, Arbitrary (Sem effs Int)) =>
(forall a. Sem r1 a -> IO (f a))
-> (forall a. Sem r2 a -> IO (f a)) -> Property
prepropEquivalent forall a. Sem r1 a -> IO (f a)
int1 forall a. Sem r2 a -> IO (f a)
int2 = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
SomeSem forall (r :: EffectRow). Inject effs r => Sem r Int
sem <- forall (effs :: EffectRow) a.
Arbitrary (Sem effs a) =>
Gen (SomeSem effs a)
liftGen @effs @Int
Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
f Int
a1 <- Sem r1 Int -> IO (f Int)
forall a. Sem r1 a -> IO (f a)
int1 Sem r1 Int
forall (r :: EffectRow). Inject effs r => Sem r Int
sem
f Int
a2 <- Sem r2 Int -> IO (f Int)
forall a. Sem r2 a -> IO (f a)
int2 Sem r2 Int
forall (r :: EffectRow). Inject effs r => Sem r Int
sem
Property -> IO Property
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IO Property) -> Property -> IO Property
forall a b. (a -> b) -> a -> b
$ f Int
a1 f Int -> f Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f Int
a2
newtype SomeSem effs a = SomeSem
{ forall (effs :: EffectRow) a.
SomeSem effs a -> forall (r :: EffectRow). Inject effs r => Sem r a
_getSomeSem :: forall r. (Inject effs r) => Sem r a
}
liftGen
:: forall effs a
. Arbitrary (Sem effs a)
=> Gen (SomeSem effs a)
liftGen :: forall (effs :: EffectRow) a.
Arbitrary (Sem effs a) =>
Gen (SomeSem effs a)
liftGen = do
Sem effs a
a <- forall a. Arbitrary a => Gen a
arbitrary @(Sem effs a)
SomeSem effs a -> Gen (SomeSem effs a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeSem effs a -> Gen (SomeSem effs a))
-> SomeSem effs a -> Gen (SomeSem effs a)
forall a b. (a -> b) -> a -> b
$ (forall (r :: EffectRow). Inject effs r => Sem r a)
-> SomeSem effs a
forall (effs :: EffectRow) a.
(forall (r :: EffectRow). Inject effs r => Sem r a)
-> SomeSem effs a
SomeSem ((forall (r :: EffectRow). Inject effs r => Sem r a)
-> SomeSem effs a)
-> (forall (r :: EffectRow). Inject effs r => Sem r a)
-> SomeSem effs a
forall a b. (a -> b) -> a -> b
$ Sem effs a -> Sem r a
forall (effs :: EffectRow) (r :: EffectRow) a.
Inject effs r =>
Sem effs a -> Sem r a
inject Sem effs a
a