{-# 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
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 a. Sem r a -> IO (f a)) -> Property
prepropCommutative lower :: forall a. Sem r a -> IO (f a)
lower = Testable (Gen Property) => Gen Property -> Property
forall prop. Testable prop => prop -> Property
property @(Gen Property) (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
SomeEff m1 :: e (Sem r) a
m1 <- ArbitraryEff r r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @r @r
SomeEff e1 :: e (Sem r) a
e1 <- ArbitraryEff effs1 r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs1 @r
SomeEff e2 :: e (Sem r) a
e2 <- ArbitraryEff effs2 r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs2 @r
SomeEff m2 :: e (Sem r) a
m2 <- ArbitraryEff r r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @r @r
Property -> Gen Property
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 "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 "" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("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 ("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 ("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 ("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 "" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample "(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 (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 (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 (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 (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 (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 (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 (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 a. Sem r a -> IO (f a)) -> [Property]
prepropAllCommutative _ = []
instance (ArbitraryEff r r, ArbitraryEff es r, ArbitraryEff '[e] r, AllCommutative es r)
=> AllCommutative (e ': es) r where
prepropAllCommutative :: (forall a. Sem r a -> IO (f a)) -> [Property]
prepropAllCommutative lower :: forall a. Sem r a -> IO (f a)
lower
= (forall a. Sem r a -> IO (f a)) -> Property
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 forall a. Sem r a -> IO (f a)
lower
Property -> [Property] -> [Property]
forall a. a -> [a] -> [a]
: (forall a. Sem r a -> IO (f a)) -> [Property]
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 forall a. Sem r a -> IO (f a)
lower
data Law r z a = Law
{ Law r z a -> Sem r a
lawLhs :: Sem r a
, Law r z a -> Sem r a
lawRhs :: Sem r a
, Law r z a -> [Sem r ()]
lawPrelude :: [Sem r ()]
, Law r z a -> [Sem r z]
lawPostlude :: [Sem r z]
}
simpleLaw :: Sem r a -> Sem r a -> Law r () a
simpleLaw :: Sem r a -> Sem r a -> Law r () a
simpleLaw lhs :: Sem r a
lhs rhs :: 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 :: Gen (Law r x a)
-> Maybe (f a -> String)
-> (forall z. Sem r (a, z) -> IO (f (a, z)))
-> Property
prepropLaw g :: Gen (Law r x a)
g labeler :: Maybe (f a -> String)
labeler lower :: forall z. Sem r (a, z) -> IO (f (a, z))
lower = Testable (Gen Property) => Gen Property -> Property
forall prop. Testable prop => prop -> Property
property @(Gen Property) (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
Law lhs :: Sem r a
lhs rhs :: Sem r a
rhs mprel :: [Sem r ()]
mprel mpost :: [Sem r x]
mpost <- Gen (Law r x a)
g
SomeEff pre1 :: e (Sem r) a
pre1 <- ArbitraryEff effs r => Gen (SomeEff r)
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 pre2 :: e (Sem r) a
pre2 <- ArbitraryEff effs r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
SomeEff post1 :: e (Sem r) a
post1 <- ArbitraryEff effs r => Gen (SomeEff r)
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 post2 :: e (Sem r) a
post2 <- ArbitraryEff effs r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
Property -> Gen Property
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 ("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 ("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 ("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 ("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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure (a
a2, (Maybe x
z, a
r))
Property -> IO Property
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 (\lbl :: 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 (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 :: [Sem r a] -> Gen (Sem r (Maybe a))
maybeOneof [] = Sem r (Maybe a) -> Gen (Sem r (Maybe 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 (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
maybeOneof res :: [Sem r a]
res = do
Int
chance <- [Int] -> Gen Int
forall a. [a] -> Gen a
elements @Int [0..9]
case Int
chance Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 8 of
True -> (Sem r a -> Sem r (Maybe a))
-> Gen (Sem r a) -> Gen (Sem r (Maybe a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Maybe a) -> Sem r a -> Sem r (Maybe a)
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
False -> Sem r (Maybe a) -> Gen (Sem r (Maybe 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 (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing
constructorLabel :: Data a => a -> String
constructorLabel :: 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 a. Sem r1 a -> IO (f a))
-> (forall a. Sem r2 a -> IO (f a)) -> Property
prepropEquivalent int1 :: forall a. Sem r1 a -> IO (f a)
int1 int2 :: 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 sem :: forall (r :: EffectRow). Inject effs r => Sem r Int
sem <- Arbitrary (Sem effs Int) => Gen (SomeSem effs Int)
forall (effs :: EffectRow) a.
Arbitrary (Sem effs a) =>
Gen (SomeSem effs a)
liftGen @effs @Int
Property -> Gen Property
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 (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
{ 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 :: Gen (SomeSem effs a)
liftGen = do
Sem effs a
a <- Arbitrary (Sem effs a) => Gen (Sem effs a)
forall a. Arbitrary a => Gen a
arbitrary @(Sem effs a)
SomeSem effs a -> Gen (SomeSem effs 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