polysemy-check 0.2.0.0 → 0.3.0.0

raw patch · 5 files changed

+74/−26 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog.md +7/−0
• polysemy-check.cabal +1/−1
• src/Polysemy/Check.hs +32/−9
• test/EquivSpec.hs +7/−5
• test/LawSpec.hs +27/−11

@@ -1,5 +1,12 @@ # Changelog for polysemy-check +## v0.3.0.0 (2021-10-09)++- `prepropLaw` now synthesizes a monadic prelude and postlude to your laws, to+    ensure they hold under every context. The type has changed as a result.+- `prepropEquivalent` now allows you to produce a functor `f` result, so you can+    check equivalence of the underlying state as well.+ ## v0.2.0.0 (2021-10-09)  - Updated the signature of `prepropEquivalent` to take a `Proxy r`. This lets

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           polysemy-check-version:        0.2.0.0+version:        0.3.0.0 synopsis:       QuickCheck for Polysemy description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme> category:       Polysemy

@@ -29,6 +29,7 @@   , GenericK   ) where +import Control.Monad (void) import Data.Proxy import Generics.Kind (GenericK) import Generics.Kind.TH (deriveGenericK)@@ -102,18 +103,37 @@ -- For example, any lawful interpretation of @State@ must satisfy the @put s1 -- >> put s2 = put s2@ law. prepropLaw-    :: (Eq x, Show x)+    :: 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.-    -> (Sem r a -> IO x)+    -> (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 g lower = property $ do+prepropLaw g lower = property @(Gen Property) $ do+  SomeEff pre <- arbitraryActionFromRow @effs @r   (m1, m2) <- g+  SomeEff post <- arbitraryActionFromRow @effs @r   pure $ ioProperty $ do-    a1 <- lower m1-    a2 <- lower m2+    a1 <-+      lower $ do+        void $ send pre+        a1 <- m1+        r <- send post+        pure (a1, r)+    a2 <-+      lower $ do+        void $ send pre+        a2 <- m2+        r <- send post+        pure (a2, r)     pure $ a1 === a2  @@ -122,12 +142,15 @@ -- property ensures that the two interpreters give the same result for every -- arbitrary program. 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 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 a)+    -> (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

@@ -5,7 +5,7 @@  module EquivSpec where -import Data.IORef (newIORef)+import Data.IORef (newIORef, readIORef) import Data.Proxy (Proxy) import Polysemy import Polysemy.Check@@ -30,12 +30,14 @@             pure $ send e1 >> send e2 >> send e3  -runPureState :: Int -> Sem '[State Int] a -> IO a-runPureState s = pure . run . evalState s+runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)+runPureState s = pure . run . runState s  -runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (a)+runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (Int, a) runIOState s sem = do   ref <- newIORef s-  runM . runStateIORef ref $ sem+  a <- runM . runStateIORef ref $ sem+  r <- readIORef ref+  pure (r, a) 

@@ -37,28 +37,38 @@   putPutLaw-    :: (Arbitrary s, Member (State s) r, Eq x, Show x)-    => (Sem r s -> IO x)+    :: forall s r+     . ( Arbitrary s+       , Member (State s) r+       , Eq s+       , Show s+       , ArbitraryEff '[State s] r+       )+    => (forall a. Sem r ((), a) -> IO (s, ((), a)))     -> Property-putPutLaw = prepropLaw $ do+putPutLaw = prepropLaw @'[State s] $ do   s1 <- arbitrary   s2 <- arbitrary   pure     ( do         put s1         put s2-        get     , do         put s2-        get     )   getPutLaw-    :: (Arbitrary s, Member (State s) r, Eq x, Show x)-    => (Sem r () -> IO x)+    :: forall s r+     . ( Arbitrary s+       , Member (State s) r+       , Eq s+       , Show s+       , ArbitraryEff '[State s] r+       )+    => (forall a. Sem r ((), a) -> IO (s, ((), a)))     -> Property-getPutLaw = prepropLaw $ do+getPutLaw = prepropLaw @'[State s] $ do   pure     ( get >>= put     , pure ()@@ -66,10 +76,16 @@   putGetLaw-    :: (Arbitrary s, Member (State s) r, Eq x, Show x)-    => (Sem r s -> IO x)+    :: forall s r+     . ( Arbitrary s+       , Member (State s) r+       , Eq s+       , Show s+       , ArbitraryEff '[State s] r+       )+    => (forall a. Sem r (s, a) -> IO (s, (s, a)))     -> Property-putGetLaw = prepropLaw $ do+putGetLaw = prepropLaw @'[State s] $ do   s <- arbitrary   pure     ( do