{-# LANGUAGE QuantifiedConstraints #-}

module Polysemy.Check
  ( -- * Effect Properties
    prepropCommutative
  , prepropAllCommutative
  , prepropEquivalent
  , prepropLaw

    -- * Law Constructors
  , Law (..)
  , simpleLaw

    -- * Generators for Effects
  , arbitraryAction
  , arbitraryActionOfType
  , arbitraryActionFromRow
  , arbitraryActionFromRowOfType

    -- * Types for Generators for Effects
  , SomeAction (..)
  , SomeEff (..)
  , SomeEffOfType (..)

  -- * Common labeling functions
  , constructorLabel

    -- * Support for Existential Types
  , ExistentialFor

    -- * Constraints for Generators of Effects
  , GArbitraryK
  , ArbitraryAction
  , ArbitraryEff
  , ArbitraryEffOfType
  , TypesOf

    -- * Re-exports
  , 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)


------------------------------------------------------------------------------
-- | Prove that two effects are commutative (a la
-- <https://dl.acm.org/doi/10.1145/3473578 Reasoning about effect interaction by fusion>)
-- under the given interpreter.
--
-- Humans naturally expect that disparate effects do not interact, thus
-- commutativity is an important property for reasoning about the correctness
-- of your program.
--
-- For example,
--
-- @
-- 'prepropCommutative' \@'[State Int] \@'[Trace] \@EffStack runEffStack
-- @
--
-- will interleave random @State Int@ and @Trace@ actions, within a bigger
-- context of @EffStack@ actions. The resulting 'Property' will fail if
-- permuting the @State Int@ and @Trace@ effects changes the outcome of the
-- entire computation.
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))
       -- ^ An interpreter for the effect stack down to 'IO'. Pure effect
       -- stacks can be lifted into 'IO' via 'pure' after the final 'run'.
    -> Property
prepropCommutative :: (forall a. Sem r a -> IO (f a)) -> Property
prepropCommutative 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 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 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 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 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 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 (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' \@effs \@r interpreter@ generates an invocation
  -- of 'prepropCommutative' for every tail in @effs@. In essence, this ensures
  -- that every effect in @effs@ commutes with every other one.
  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 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 a. Sem r a -> IO (f a)) -> [Property]
prepropAllCommutative 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 structure containing programs that should be equal, and under which
-- circumstances.
--
-- @since 0.9.0.0
data Law r z a = Law
  { Law r z a -> Sem r a
lawLhs      :: Sem r a
    -- ^ 'lawLhs' and 'lawRhs' are being asserted as equal.
  , Law r z a -> Sem r a
lawRhs      :: Sem r a
    -- ^ 'lawLhs' and 'lawRhs' are being asserted as equal.
  , Law r z a -> [Sem r ()]
lawPrelude  :: [Sem r ()]
    -- ^ A set of actions to possibly run before checking equality. Useful for
    -- ensuring the existence of something being tested.
  , Law r z a -> [Sem r z]
lawPostlude :: [Sem r z]
    -- ^ A set of actions to possibly run after checking equality. Useful for
    -- checking the existence after something was created.
  }


------------------------------------------------------------------------------
-- | Like 'Law', but for the common case when you don't need a custom prelude
-- or postlude.
--
-- @since 0.9.0.0
simpleLaw :: Sem r a -> Sem r a -> Law r () a
simpleLaw :: 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 [] []


------------------------------------------------------------------------------
-- | Prove that two programs in @r@ are equivalent under a given
-- interpretation. This is useful for proving laws about particular effects (or
-- stacks of effects).
--
-- For example, any lawful interpretation of @State@ must satisfy the @put s1
-- >> put s2 = put s2@ law.
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)
       -- ^ A generator for two equivalent programs.
    -> Maybe (f a -> String)
       -- ^ How to label the results for QuickCheck coverage.
    -> (forall z. Sem r (a, z) -> IO (f (a, z)))
       -- ^ An interpreter for the effect stack down to 'IO'. Pure effect
       -- stacks can be lifted into 'IO' via 'pure' after the final 'run'.
    -> Property
prepropLaw :: 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 = 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 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 <- 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 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 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 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 (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 (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 (\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 [Sem r a]
res = do
  Int
chance <- [Int] -> Gen Int
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 (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
    Bool
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



------------------------------------------------------------------------------
-- | Label an example with its data constructor.
--
-- @since 0.9.0.0
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


------------------------------------------------------------------------------
-- | Prove that two interpreters are equivalent. This property ensures that the
-- two interpreters give the same result for every arbitrary program.
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))
       -- ^ The first interpreter for the effect stack.Pure effect stacks can
       -- be lifted into 'IO' via 'pure' after the final 'run'.
    -> (forall a. Sem r2 a -> IO (f a))
       -- ^ The second interpreter to prove equivalence for.
    -> Property
prepropEquivalent :: (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 <- 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