{-# 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 Data.Proxy
import Generics.Kind (GenericK)
import Generics.Kind.TH (deriveGenericK)
import Polysemy
import Polysemy.Check.Arbitrary
import Polysemy.Check.Arbitrary.AnyEff
import Polysemy.Check.Arbitrary.Generic (GArbitraryK, ExistentialFor)
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
$ 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 x r1 r2 f
. ( forall a. Show a => Show (f a)
, forall a. Eq a => Eq (f a)
)
=> (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
=> (forall a. Sem r1 a -> IO (f a))
-> (forall a. Sem r2 a -> IO (f a))
-> (forall r. Proxy r -> Members effs r => Gen (Sem r x))
-> Property
prepropEquivalent :: (forall a. Sem r1 a -> IO (f a))
-> (forall a. Sem r2 a -> IO (f a))
-> (forall (r :: EffectRow).
Proxy r -> Members effs r => Gen (Sem r x))
-> Property
prepropEquivalent int1 :: forall a. Sem r1 a -> IO (f a)
int1 int2 :: forall a. Sem r2 a -> IO (f a)
int2 mksem :: forall (r :: EffectRow). Proxy r -> Members effs r => Gen (Sem r x)
mksem = 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 x
sem <- Members effs effs =>
(forall (r :: EffectRow). Members effs r => Gen (Sem r x))
-> Gen (SomeSem effs x)
forall (effs :: EffectRow) a.
Members effs effs =>
(forall (r :: EffectRow). Members effs r => Gen (Sem r a))
-> Gen (SomeSem effs a)
liftGen @effs @x ((forall (r :: EffectRow). Members effs r => Gen (Sem r x))
-> Gen (SomeSem effs x))
-> (forall (r :: EffectRow). Members effs r => Gen (Sem r x))
-> Gen (SomeSem effs x)
forall a b. (a -> b) -> a -> b
$ Proxy r -> Members effs r => Gen (Sem r x)
forall (r :: EffectRow). Proxy r -> Members effs r => Gen (Sem r x)
mksem Proxy r
forall k (t :: k). Proxy t
Proxy
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 x
a1 <- Sem r1 x -> IO (f x)
forall a. Sem r1 a -> IO (f a)
int1 Sem r1 x
forall (r :: EffectRow). Inject effs r => Sem r x
sem
f x
a2 <- Sem r2 x -> IO (f x)
forall a. Sem r2 a -> IO (f a)
int2 Sem r2 x
forall (r :: EffectRow). Inject effs r => Sem r x
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 x
a1 f x -> f x -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== f x
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
. Members effs effs
=> (forall r. Members effs r => Gen (Sem r a))
-> Gen (SomeSem effs a)
liftGen :: (forall (r :: EffectRow). Members effs r => Gen (Sem r a))
-> Gen (SomeSem effs a)
liftGen g :: forall (r :: EffectRow). Members effs r => Gen (Sem r a)
g = do
Sem effs a
a <- Members effs effs => Gen (Sem effs a)
forall (r :: EffectRow). Members effs r => Gen (Sem r a)
g @effs
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