{-# LANGUAGE QuantifiedConstraints #-}
module Polysemy.Check
(
prepropCommutative
, prepropEquivalent
, prepropLaw
, arbitraryAction
, arbitraryActionOfType
, arbitraryActionFromRow
, arbitraryActionFromRowOfType
, SomeAction (..)
, SomeEff (..)
, SomeEffOfType (..)
, 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
prepropCommutative
:: forall e1 e2 r f
. ( forall a. Show a => Show (f a)
, forall a. Eq a => Eq (f a)
)
=> ( ArbitraryEff r r
, ArbitraryEff '[e1] r
, ArbitraryEff '[e2] 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 '[e1] r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @'[e1] @r
SomeEff e2 :: e (Sem r) a
e2 <- ArbitraryEff '[e2] r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @'[e2] @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 "(e1 >> e2 >> k) /= (e2 >> e1 >> k)" (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
prepropLaw
:: forall effs r a f
. ( (forall z. Eq z => Eq (f z))
, (forall z. Show z => Show (f z))
)
=> ( Eq a
, Show a
, ArbitraryEff effs r
)
=> Gen (Sem r a, Sem r a)
-> (forall z. Sem r (a, z) -> IO (f (a, z)))
-> Property
prepropLaw :: Gen (Sem r a, Sem r a)
-> (forall z. Sem r (a, z) -> IO (f (a, z))) -> Property
prepropLaw g :: Gen (Sem r a, Sem r a)
g 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
SomeEff pre :: e (Sem r) a
pre <- ArbitraryEff effs r => Gen (SomeEff r)
forall (effs :: EffectRow) (r :: EffectRow).
ArbitraryEff effs r =>
Gen (SomeEff r)
arbitraryActionFromRow @effs @r
(m1 :: Sem r a
m1, m2 :: Sem r a
m2) <- Gen (Sem r a, Sem r a)
g
SomeEff post :: e (Sem r) a
post <- 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 ("before = " 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
pre) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ("after = " 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
post) (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, a)
a1 <-
Sem r (a, a) -> IO (f (a, a))
forall z. Sem r (a, z) -> IO (f (a, z))
lower (Sem r (a, a) -> IO (f (a, a))) -> Sem r (a, a) -> IO (f (a, 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
pre
a
a1 <- Sem r a
m1
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
post
(a, a) -> Sem r (a, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a1, a
r)
f (a, a)
a2 <-
Sem r (a, a) -> IO (f (a, a))
forall z. Sem r (a, z) -> IO (f (a, z))
lower (Sem r (a, a) -> IO (f (a, a))) -> Sem r (a, a) -> IO (f (a, 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
pre
a
a2 <- Sem r a
m2
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
post
(a, a) -> Sem r (a, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a2, 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
$ f (a, a)
a1 f (a, a) -> f (a, a) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f (a, a)
a2
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