polysemy-check 0.5.0.0 → 0.6.0.0

raw patch · 6 files changed

+153/−27 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog.md +8/−0
• polysemy-check.cabal +2/−1
• src/Polysemy/Check.hs +14/−16
• src/Polysemy/Check/Arbitrary.hs +6/−4
• test/EquivSpec.hs +0/−6
• test/ExampleSpec.hs +123/−0

@@ -1,5 +1,13 @@ # Changelog for polysemy-check +## v0.6.0.0 (2021-10-16)++- Changed the frequencies of `Sem`'s `Arbitrary` instance, to create more+    interesting programs.+- Removed the program generator parameter of `prepropEquivalent`. It now just+    uses the `Arbitrary` instance for `Sem`.+- Added some new examples to the test suite.+ ## v0.5.0.0 (2021-10-14)  - Flattened the module structure of `Polysemy.Check.Arbitrary`.

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           polysemy-check-version:        0.5.0.0+version:        0.6.0.0 synopsis:       QuickCheck for Polysemy description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme> category:       Polysemy@@ -71,6 +71,7 @@       CommutativeSpec       CoverageSpec       EquivSpec+      ExampleSpec       LawSpec       WeirdEffectsSpec       Paths_polysemy_check

@@ -33,7 +33,6 @@   ) where  import Control.Monad (void)-import Data.Proxy import Generics.Kind (GenericK) import Generics.Kind.TH (deriveGenericK) import Polysemy@@ -142,27 +141,27 @@   --------------------------------------------------------------------------------- | 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.+-- | Prove that two interpreters are equivalent. 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)+    => ( Eq x+       , Show x+       , Inject effs r1+       , Inject effs r2+       , Arbitrary (Sem effs x)+       )     => (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 int1 int2 mksem = property $ do-  SomeSem sem <- liftGen @effs @x $ mksem Proxy+prepropEquivalent int1 int2 = property $ do+  SomeSem sem <- liftGen @effs @x   pure $ ioProperty $ do     a1 <- int1 sem     a2 <- int2 sem@@ -176,10 +175,9 @@  liftGen     :: forall effs a-     . Members effs effs-    => (forall r. Members effs r => Gen (Sem r a))-    -> Gen (SomeSem effs a)-liftGen g = do-  a <- g @effs+     . Arbitrary (Sem effs a)+    => Gen (SomeSem effs a)+liftGen = do+  a <- arbitrary @(Sem effs a)   pure $ SomeSem $ inject a 

@@ -1,3 +1,5 @@+{-# LANGUAGE TupleSections #-}+ {-# OPTIONS_GHC -Wno-orphans #-}  module Polysemy.Check.Arbitrary where@@ -85,15 +87,15 @@      in sized $ \n ->           case n <= 1 of             True -> oneof terminal-            False -> oneof $-              [ do+            False -> frequency $+              [ (2,) $ do                   SomeEffOfType e <- arbitraryActionFromRowOfType @r @r @a                   pure $ send e-              , do+              , (8,) $ do                   SomeEff e <- arbitraryActionFromRow @r @r                   k <- liftArbitrary $ scale (`div` 2) arbitrary                   pure $ send e >>= k-              ] <> terminal+              ] <> fmap (1,) terminal  ------------------------------------------------------------------------------ -- | @genEff \@e \@r \@a@ gets a generator capable of producing every

@@ -6,7 +6,6 @@ module EquivSpec where  import Data.IORef (newIORef, readIORef)-import Data.Proxy (Proxy) import Polysemy import Polysemy.Check import Polysemy.State@@ -23,11 +22,6 @@       prepropEquivalent @'[State Int] @Int         (runPureState s0)         (runIOState s0)-        $ \(_ :: Proxy r) -> do-            SomeAction e1 <- arbitraryAction @(State Int) @r-            SomeAction e2 <- arbitraryAction @(State Int) @r-            e3 <- arbitraryActionOfType @(State Int) @Int @r-            pure $ send e1 >> send e2 >> send e3   runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)

@@ -0,0 +1,123 @@+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE DeriveGeneric #-}++module ExampleSpec where++import Control.Monad+import Data.Maybe (listToMaybe)+import Polysemy+import Polysemy.Check+import Polysemy.State+import Test.Hspec+import Test.Hspec.QuickCheck+import Test.QuickCheck+++data Stack s m a where+  Push      :: s -> Stack s m ()+  Pop       :: Stack s m (Maybe s)+  RemoveAll :: Stack s m ()+  Size      :: Stack s m Int++deriving instance Show s => Show (Stack s m a)+deriveGenericK ''Stack++makeSem ''Stack+++spec :: Spec+spec = do+  describe "Laws" $ do+    let law x = prepropLaw @'[Stack Int] x $ pure . run . runStack []++    prop "push >> pop is pure" $ do+      law $ do+        s <- arbitrary+        pure+          ( push s >> pop+          , pure $ Just s+          )++    prop "pop >> push is id" $ do+      law $+        pure+          ( pop >>= maybe (pure ()) push+          , pure ()+          )++    prop "removeAll sets size to 0" $ do+      law $+        pure+          ( 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+          )++    prop "pop decreases size by 1" $ do+      law $ do+        pure+          ( pop >> size+          , fmap (max 0 . subtract 1) size <* pop+          )+++  describe "Equivalence" $ do+    let equiv b1 b2 =+          prepropEquivalent @'[Stack Int] @Int+            (pure . run . runStack b1)+            (pure . run . runStack b2)++    prop "All interpreters are equivalent to itself" $ do+      bugs <- arbitrary+      pure $ equiv bugs bugs++    prop "DontRemove bug interpreter isn't equivalent to the correct version" $+      expectFailure $ equiv [DontRemove] []++    prop "PushTwice bug interpreter isn't equivalent to the correct version" $+      expectFailure $ equiv [PushTwice] []++    prop "The buggy interpreters are not equivalent to one another" $+      expectFailure $ equiv [PushTwice] [DontRemove]+++data Bug+  = PushTwice+  | DontRemove+  deriving stock (Eq, Ord, Show, Enum, Bounded)++instance Arbitrary Bug where+  arbitrary = elements [minBound..maxBound]+++hasBug :: [Bug] -> Bug -> Bool+hasBug = flip elem+++runStack+    :: [Bug]+    -> Sem (Stack s ': r) a+    -> Sem r ([s], a)+runStack bugs =+  (runState [] .) $ reinterpret $ \case+    Push s -> do+      modify (s :)+      when (hasBug bugs PushTwice) $+        modify (s :)+    Pop -> do+      r <- gets listToMaybe+      modify (drop 1)+      pure r+    RemoveAll ->+      unless (hasBug bugs DontRemove) $+        put []+    Size -> gets length+