{-# LANGUAGE QuantifiedConstraints #-}
module Polysemy.Check
  ( -- * Effect Properties
    prepropCommutative
  , prepropEquivalent
  , prepropLaw

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

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

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

    -- * Re-exports
  , 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)
import Polysemy.Check.Orphans ()
import Polysemy.Internal
import Polysemy.Internal.Union.Inject (Inject, inject)
import Test.QuickCheck


------------------------------------------------------------------------------
-- | 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 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))
       -- ^ 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 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


------------------------------------------------------------------------------
-- | 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 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)
       -- ^ A generator for two equivalent programs.
    -> (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 (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


------------------------------------------------------------------------------
-- | Prove that two interpreters are equivalent. For the given generator, this
-- property ensures that the two interpreters give the same result for every
-- arbitrary program.
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))
       -- ^ 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.
    -> (forall r. Proxy r -> Members effs r => Gen (Sem r x))
       -- ^ A generator producing arbitrary programs in @r@. The property will
       -- hold true if both interpreters produce the same output for every
       -- program generated by this.
    -> 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