polysemy-check 0.8.1.0 → 0.9.0.0

raw patch · 6 files changed

+214/−62 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• polysemy-check.cabal +2/−1
• src/Polysemy/Check.hs +92/−17
• test/BigKeySpec.hs +74/−0
• test/ExampleSpec.hs +17/−21
• test/LawSpec.hs +23/−23

@@ -1,5 +1,11 @@ # Changelog for polysemy-check +## v0.9.0.0 (2021-12-03)++- `prepropLaw` now generates a new `Law` record, allowing for better control+    over the program prelude and postludes+- `prepropLaw` now takes a labeler, for running QuickCheck coverage+ ## v0.8.1.0 (2021-10-21)  - Added a new function, `prepropAllCommutative` which ensures every effect

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           polysemy-check-version:        0.8.1.0+version:        0.9.0.0 synopsis:       QuickCheck for Polysemy description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme> category:       Polysemy@@ -68,6 +68,7 @@   type: exitcode-stdio-1.0   main-is: Main.hs   other-modules:+      BigKeySpec       CommutativeSpec       CoverageSpec       EquivSpec

@@ -7,6 +7,10 @@   , prepropEquivalent   , prepropLaw +    -- * Law Constructors+  , Law (..)+  , simpleLaw+     -- * Generators for Effects   , arbitraryAction   , arbitraryActionOfType@@ -18,6 +22,9 @@   , SomeEff (..)   , SomeEffOfType (..) +  -- * Common labeling functions+  , constructorLabel+     -- * Support for Existential Types   , ExistentialFor @@ -43,6 +50,7 @@ import Polysemy.Internal import Polysemy.Internal.Union.Inject (Inject, inject) import Test.QuickCheck+import Data.Data (Data, showConstr, toConstr)   ------------------------------------------------------------------------------@@ -121,6 +129,34 @@   ------------------------------------------------------------------------------+-- | Data structure containing programs that should be equal, and under which+-- circumstances.+--+-- @since 0.9.0.0+data Law r z a = Law+  { lawLhs      :: Sem r a+    -- ^ 'lawLhs' and 'lawRhs' are being asserted as equal.+  , lawRhs      :: Sem r a+    -- ^ 'lawLhs' and 'lawRhs' are being asserted as equal.+  , lawPrelude  :: [Sem r ()]+    -- ^ A set of actions to possibly run before checking equality. Useful for+    -- ensuring the existence of something being tested.+  , 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 lhs rhs = Law lhs 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).@@ -128,41 +164,80 @@ -- For example, any lawful interpretation of @State@ must satisfy the @put s1 -- >> put s2 = put s2@ law. prepropLaw-    :: forall effs r a f+    :: 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 (Sem r a, Sem r a)+    => 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 g lower = property @(Gen Property) $ do-  SomeEff pre <- arbitraryActionFromRow @effs @r-  (m1, m2) <- g-  SomeEff post <- arbitraryActionFromRow @effs @r+prepropLaw g labeler lower = property @(Gen Property) $ do+  Law lhs rhs mprel mpost <- g+  SomeEff pre1 <- arbitraryActionFromRow @effs @r+  prel <- maybeOneof mprel+  SomeEff pre2 <- arbitraryActionFromRow @effs @r+  SomeEff post1 <- arbitraryActionFromRow @effs @r+  post <- maybeOneof mpost+  SomeEff post2 <- arbitraryActionFromRow @effs @r   pure $-    counterexample ("before = " <> show pre) $-    counterexample ("after  = " <> show post) $+    counterexample ("before1 = " <> show pre1) $+    counterexample ("before2 = " <> show pre2) $+    counterexample ("after1  = " <> show post1) $+    counterexample ("after2  = " <> show post2) $       ioProperty $ do         a1 <-           lower $ do-            void $ send pre-            a1 <- m1-            r <- send post-            pure (a1, r)+            void $ send pre1+            void $ prel+            void $ send pre2+            a1 <- lhs+            void $ send post1+            z <- post+            r <- send post2+            pure (a1, (z, r))         a2 <-           lower $ do-            void $ send pre-            a2 <- m2-            r <- send post-            pure (a2, r)-        pure $ a1 === a2+            void $ send pre1+            void prel+            void $ send pre2+            a2 <- rhs+            void $ send post1+            z <- post+            r <- send post2+            pure (a2, (z, r))+        pure+          $ maybe property (\lbl -> label $ lbl $ fmap fst a1) labeler+          $ a1 === a2+++maybeOneof :: [Sem r a] -> Gen (Sem r (Maybe a))+maybeOneof [] = pure $ pure Nothing+maybeOneof res = do+  chance <- elements @Int [0..9]+  case chance < 8 of+    True -> fmap (fmap Just) $ elements res+    False -> pure $ pure Nothing++++------------------------------------------------------------------------------+-- | Label an example with its data constructor.+--+-- @since 0.9.0.0+constructorLabel :: Data a => a -> String+constructorLabel = showConstr . toConstr   ------------------------------------------------------------------------------

@@ -0,0 +1,74 @@+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}++module BigKeySpec where++import qualified Data.Map as M+import Data.Map (Map)+import Polysemy+import Polysemy.Check+import Test.Hspec+import Test.QuickCheck+import Test.Hspec.QuickCheck+import Polysemy.State+import Data.Functor.Identity+import Data.Word++data KVStore k v m a where+  Store :: k -> v -> KVStore k v m ()+  Delete :: k -> KVStore k v m ()+  Retrieve :: k -> KVStore k v m (Maybe v)++deriving instance (Show k, Show v) => Show (KVStore k v m a)++makeSem ''KVStore+deriveGenericK ''KVStore+++data Bug = HasBug | NoBug++runKVStore :: forall k v r a. Ord k => Bug -> Sem (KVStore k v ': r) a -> Sem r a+runKVStore bug = (evalState (mempty @(Map k v)) .) $  reinterpret $ \case+  Store k v -> modify $ M.insert k v+  Delete k ->+    case bug of+      HasBug -> pure ()+      NoBug -> modify $ M.delete k+  Retrieve k -> gets $ M.lookup k+++deleteGetLaw+    :: forall r+     . r ~ '[KVStore Word64 Bool]+    => Bug+    -> (Word64 -> Bool -> [Sem r ()])+    -> Property+deleteGetLaw bug prel =+  prepropLaw @r+    (do+      k <- arbitrary+      v <- arbitrary+      pure $ Law+        { lawLhs = do+            delete k+            retrieve k+        , lawRhs = do+            delete k+            pure Nothing+        , lawPrelude = prel k v+        , lawPostlude = [] :: [Sem r ()]+        }+    )+    Nothing  -- (Just $ constructorLabel . runIdentity)+    (pure . Identity . run . runKVStore @Word64 @Bool bug)+++spec :: Spec+spec = do+  describe "without prelude" $ do+    -- prop "with bug"    $ deleteGetLaw HasBug $ \_ _ -> []+    prop "without bug" $ deleteGetLaw NoBug $ \_ _ -> []++  describe "with prelude" $ do+    prop "with bug"    $ expectFailure $ deleteGetLaw HasBug $ \k v -> [store k v]+    prop "without bug" $ deleteGetLaw NoBug $ \k v -> [store k v]+

@@ -29,44 +29,40 @@ spec :: Spec spec = do   describe "Laws" $ do-    let law x = prepropLaw @'[Stack Int] x $ pure . run . runStack []+    let law x = prepropLaw @'[Stack Int] x (Just $ constructorLabel . fst) $ pure . run . runStack []      prop "push >> pop is pure" $ do       law $ do         s <- arbitrary-        pure-          ( push s >> pop-          , pure $ Just s-          )+        pure $ simpleLaw+          (push s >> pop)+          (pure $ Just s)      prop "pop >> push is id" $ do       law $-        pure-          ( pop >>= maybe (pure ()) push-          , pure ()-          )+        pure $ simpleLaw+          (pop >>= maybe (pure ()) push)+          (pure ()) +     prop "removeAll sets size to 0" $ do       law $-        pure-          ( removeAll >> size-          , removeAll >> pure 0-          )+        pure $ simpleLaw+          (removeAll >> size)+          (removeAll >> pure 0)      prop "push increases size by 1" $ do       law $ do         s <- arbitrary-        pure-          ( push s >> size-          , fmap (+1) size <* push s-          )+        pure $ simpleLaw+          (push s >> size)+          (fmap (+1) size <* push s)      prop "pop decreases size by 1" $ do       law $ do-        pure-          ( pop >> size-          , fmap (max 0 . subtract 1) size <* pop-          )+        pure $ simpleLaw+          (pop >> size)+          (fmap (max 0 . subtract 1) size <* pop)     describe "Equivalence" $ do

@@ -16,24 +16,24 @@   describe "pure state" $ do     prop "put >> put = put" $ do       s <- arbitrary-      pure $ putPutLaw $ runPureState s+      pure $ putPutLaw Nothing $ runPureState s     prop "get >>= put = pure ()" $ do       s <- arbitrary-      pure $ getPutLaw $ runPureState s+      pure $ getPutLaw Nothing $ runPureState s     prop "put >> get = put >> pure" $ do       s <- arbitrary-      pure $ putGetLaw $ runPureState s+      pure $ putGetLaw Nothing $ runPureState s    describe "io state" $ do     prop "put >> put = put" $ do       s <- arbitrary-      pure $ putPutLaw $ runIOState s+      pure $ putPutLaw Nothing $ runIOState s     prop "get >>= put = pure ()" $ do       s <- arbitrary-      pure $ getPutLaw $ runIOState s+      pure $ getPutLaw Nothing $ runIOState s     prop "put >> get = put >> pure" $ do       s <- arbitrary-      pure $ putGetLaw $ runIOState s+      pure $ putGetLaw Nothing $ runIOState s   type LawConstraints f effs s r =@@ -52,18 +52,18 @@      . ( res ~ ()        , LawConstraints f effs s r        )-    => (forall a. Sem r (res, a) -> IO (f (res, a)))+    => Maybe (f res -> String)+    -> (forall a. Sem r (res, a) -> IO (f (res, a)))     -> Property putPutLaw = prepropLaw @effs $ do   s1 <- arbitrary   s2 <- arbitrary-  pure+  pure $ simpleLaw     ( do         put s1-        put s2-    , do-        put s2-    )+        put s2)+    ( do+        put s2)   getPutLaw@@ -71,13 +71,13 @@      . ( res ~ ()        , LawConstraints f effs s r        )-    => (forall a. Sem r (res, a) -> IO (f (res, a)))+    => Maybe (f res -> String)+    -> (forall a. Sem r (res, a) -> IO (f (res, a)))     -> Property getPutLaw = prepropLaw @effs $ do-  pure-    ( get >>= put-    , pure ()-    )+  pure $ simpleLaw+    (get >>= put)+    (pure ())   putGetLaw@@ -85,18 +85,18 @@      . ( res ~ s        , LawConstraints f effs s r        )-    => (forall a. Sem r (res, a) -> IO (f (res, a)))+    => Maybe (f res -> String)+    -> (forall a. Sem r (res, a) -> IO (f (res, a)))     -> Property putGetLaw = prepropLaw @effs $ do   s <- arbitrary-  pure+  pure $ simpleLaw     ( do         put s-        get-    , do+        get)+    ( do         put s-        pure s-    )+        pure s)   runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)