{-# LANGUAGE QuantifiedConstraints #-}
module Polysemy.Check
(
prepropCommutative
, prepropEquivalent
, prepropLaw
, arbitraryAction
, arbitraryActionOfType
, arbitraryActionFromRow
, arbitraryActionFromRowOfType
, SomeAction (..)
, SomeEff (..)
, SomeEffOfType (..)
, GArbitraryK
, ArbitraryAction
, ArbitraryEff
, ArbitraryEffOfType
, TypesOf
, send
, deriveGenericK
, GenericK
) where
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)
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
:: (Eq x, Show x)
=> Gen (Sem r a, Sem r a)
-> (Sem r a -> IO x)
-> Property
prepropLaw :: Gen (Sem r a, Sem r a) -> (Sem r a -> IO x) -> Property
prepropLaw g :: Gen (Sem r a, Sem r a)
g lower :: Sem r a -> IO x
lower = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
(m1 :: Sem r a
m1, m2 :: Sem r a
m2) <- Gen (Sem r a, Sem r a)
g
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
x
a1 <- Sem r a -> IO x
lower Sem r a
m1
x
a2 <- Sem r a -> IO x
lower 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
$ x
a1 x -> x -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== x
a2
prepropEquivalent
:: forall effs x r1 r2
. (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
=> (forall a. Sem r1 a -> IO a)
-> (forall a. Sem r2 a -> IO a)
-> (forall r. Proxy r -> Members effs r => Gen (Sem r x))
-> Property
prepropEquivalent :: (forall a. Sem r1 a -> IO a)
-> (forall a. Sem r2 a -> IO a)
-> (forall (r :: EffectRow).
Proxy r -> Members effs r => Gen (Sem r x))
-> Property
prepropEquivalent int1 :: forall a. Sem r1 a -> IO a
int1 int2 :: forall a. Sem r2 a -> IO 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
x
a1 <- Sem r1 x -> IO x
forall a. Sem r1 a -> IO a
int1 Sem r1 x
forall (r :: EffectRow). Inject effs r => Sem r x
sem
x
a2 <- Sem r2 x -> IO x
forall a. Sem r2 a -> IO 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
$ x
a1 x -> x -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== 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