Make Streams definitely finite or definitely infinite

fs-sim/fs-sim.cabal

@@ -63,6 +63,7 @@ test-suite fs-sim-test
   other-modules:
     Test.System.FS.Sim.Error
     Test.System.FS.Sim.FsTree
+    Test.System.FS.Sim.Stream
     Test.System.FS.StateMachine
     Test.Util
     Test.Util.RefEnv

fs-sim/src/System/FS/Sim/Error.hs

@@ -433,8 +433,10 @@ genErrors genPartialWrites genSubstituteWithJunk = do
     hPutBufSomeAtE <- commonPutErrors
     return Errors {..}
   where
-    streamGen l = Stream.genInfinite . Stream.genMaybe' l . QC.elements
-    streamGen' l = Stream.genInfinite . Stream.genMaybe' l . QC.frequency
+    genMaybe' = Stream.genMaybe 2
+
+    streamGen l = Stream.genInfinite . genMaybe' l . QC.elements
+    streamGen' l = Stream.genInfinite . genMaybe' l . QC.frequency
 
     commonGetErrors = streamGen' 20
       [ (1, return $ Left FsReachedEOF)

fs-sim/src/System/FS/Sim/Stream.hs

@@ -1,58 +1,58 @@
+{-# LANGUAGE BangPatterns        #-}
 {-# LANGUAGE DeriveFunctor       #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
--- | Possibly infinite streams of @'Maybe' a@s.
+-- | Finite and infinite streams of @'Maybe' a@s.
 module System.FS.Sim.Stream (
     -- * Streams
     Stream
     -- * Running
   , runStream
+  , runStreamN
     -- * Construction
   , always
   , empty
-  , mkInfinite
+  , unsafeMkInfinite
   , repeating
   , unsafeMkFinite
     -- * Query
   , null
+  , isFinite
+  , isInfinite
     -- * Generation and shrinking
   , genFinite
+  , genFiniteN
   , genInfinite
   , genMaybe
-  , genMaybe'
   , shrinkStream
   ) where
 
 import           Control.Monad (replicateM)
-import           Prelude hiding (null)
+import           Prelude hiding (isInfinite, null)
 import qualified Test.QuickCheck as QC
 import           Test.QuickCheck (Gen)
 
 {-------------------------------------------------------------------------------
   Streams
 -------------------------------------------------------------------------------}
 
--- | A 'Stream' is a stream of @'Maybe' a@s, which is /possibly/ infinite or
--- /definitely/ finite.
---
--- Finiteness is tracked internally and used for 'QC.shrink'ing and the 'Show'
--- instance.
+-- | A 'Stream' of @'Maybe' a@s that can be infinite.
 data Stream a = Stream {
-      -- | Info about the size of the stream.
+      -- | Info about the size of the stream. It is used for 'QC.shrink'ing and
+      -- the 'Show' instance.
       _streamInternalInfo :: InternalInfo
     , _getStream          :: [Maybe a]
     }
   deriving Functor
 
--- | Tag for 'Stream's that describes whether it is either /definitely/ a finite
--- stream, or /possibly/ an infinite stream.
+-- | Tag for 'Stream's that describes whether it is finite or infinite.
 --
--- Useful for the 'Show' instance of 'Stream': when a 'Stream' is /definitely/
--- finite, we can safely print the full stream.
+-- Useful for the 'Show' instance of 'Stream': when a 'Stream' is finite, we can
+-- safely print the full stream.
 data InternalInfo = Infinite | Finite
 
--- | Fully shows a 'Stream' if it is /definitely/ finite, or prints a
--- placeholder string if it is /possibly/ infinite.
+-- | Fully shows a 'Stream' if it is finite, or prints a placeholder string if
+-- it is infinite.
 instance Show a => Show (Stream a) where
   showsPrec n (Stream info xs) = case info of
       Infinite -> ("<infinite stream>" ++)
@@ -72,6 +72,20 @@ runStream :: Stream a -> (Maybe a, Stream a)
 runStream s@(Stream _    []    ) = (Nothing, s)
 runStream   (Stream info (a:as)) = (a, Stream info as)
 
+-- | Like 'runStream', but advancing the stream @n@ times.
+runStreamN :: Int -> Stream a -> ([Maybe a], Stream a)
+runStreamN n0 s0
+  | n0 < 0
+  = error "take: n should be >= 0"
+  | otherwise
+  = go n0 s0
+  where
+    go 0 s = ([], s)
+    go !n s =
+      let (x, s') = runStream s
+          (xs, s'') = go (n-1) s'
+      in  (x : xs, s'')
+
 {-------------------------------------------------------------------------------
   Construction
 -------------------------------------------------------------------------------}
@@ -86,45 +100,63 @@ always x = Stream Infinite (repeat (Just x))
 
 -- | Make a 'Stream' that infinitely repeats the given list.
 repeating :: [Maybe a] -> Stream a
-repeating xs = Stream Infinite $ concat (repeat xs)
+repeating xs = Stream Infinite $ cycle xs
 
--- | UNSAFE: Make a 'Stream' that is marked as definitely finite.
+-- | UNSAFE: Make a 'Stream' that is marked as finite.
 --
--- This is unsafe since a user can pass in any list, and evaluating
--- 'Test.QuickCheck.shrink' or 'show' on the resulting 'Stream' will diverge. It
--- is the user's responsibility to only pass in a finite list.
+-- This is unsafe since a user can pass in any list, and if the list is infinite
+-- then evaluating 'QC.shrink' or 'show' on the resulting 'Stream' will diverge.
+-- It is the user's responsibility to only pass in finite lists.
 unsafeMkFinite :: [Maybe a] -> Stream a
 unsafeMkFinite = Stream Finite
 
--- | Make a 'Stream' that is marked as possibly infinite.
-mkInfinite :: [Maybe a] -> Stream a
-mkInfinite = Stream Infinite
+-- | UNSAFE: Make a 'Stream' that is marked as infinite.
+--
+-- This is unsafe since a user can pass in any list, and if the list is finite
+-- then the result of 'QC.shrink' will degrade to an infinite list of empty
+-- streams. It is the user's responsibility to only pass in infinite lists.
+unsafeMkInfinite :: [Maybe a] -> Stream a
+unsafeMkInfinite = Stream Infinite
 
 {-------------------------------------------------------------------------------
   Query
 -------------------------------------------------------------------------------}
 
--- | Return 'True' if the stream is empty.
+-- | Check that the stream is empty. This is equivalen to checking @(==
+-- 'empty')@.
 --
--- A stream consisting of only 'Nothing's (even if it is only one) is not
--- considered to be empty.
+-- A finite\/infinite stream consisting of only 'Nothing's is not considered to
+-- be empty. In particular, @'null' ('always' Nothing) /= True@.
 null :: Stream a -> Bool
 null (Stream _ []) = True
 null _             = False
 
+-- | Check that the stream is finite
+isFinite :: Stream a -> Bool
+isFinite (Stream Finite _)   = True
+isFinite (Stream Infinite _) = False
+
+-- | Check that the stream is infinite
+isInfinite :: Stream a -> Bool
+isInfinite (Stream Finite _)   = False
+isInfinite (Stream Infinite _) = True
+
 {-------------------------------------------------------------------------------
   Generation and shrinking
 -------------------------------------------------------------------------------}
 
--- | Shrink a stream like it is an 'Test.QuickCheck.InfiniteList'.
+-- | Shrink a stream like it is an 'QC.InfiniteList'.
+--
+-- Infinite streams are shrunk differently than lists that are finite, which is
+-- to ensure that we shrink infinite lists towards finite lists.
+--
+-- * Infinite streams are shrunk by taking finite prefixes of the argument
+--   stream. Note that there are an infinite number of finite prefixes, so even
+--   though the *shrink list* is infinite, the individual *list elements* are
+--   finite.
 --
--- Possibly infinite streams are shrunk differently than lists that are
--- definitely finite, which is to ensure that shrinking terminates.
--- * Possibly infinite streams are shrunk by taking finite prefixes of the
---  argument stream. As such, shrinking a possibly infinite stream creates
---  definitely finite streams.
--- * Definitely finite streams are shrunk like lists are shrunk normally,
---   preserving that the created streams are still definitely finite.
+-- * Finite streams are shrunk like lists are shrunk normally, preserving
+--   finiteness.
 shrinkStream :: Stream a -> [Stream a]
 shrinkStream (Stream info xs0) = case info of
     Infinite -> Stream Finite <$> [take n xs0 | n <- map (2^) [0 :: Int ..]]
@@ -133,36 +165,33 @@ shrinkStream (Stream info xs0) = case info of
 -- | Make a @'Maybe' a@ generator based on an @a@ generator.
 --
 -- Each element has a chance of being either 'Nothing' or an element generated
--- with the given @a@ generator (wrapped in a 'Just').
---
--- The first argument is the likelihood (as used by 'QC.frequency') of a
--- 'Just' where 'Nothing' has likelihood 2.
+-- with the given @a@ generator (wrapped in a 'Just'). Thes /likelihoods/ are
+-- passed to 'QC.frequency'.
 genMaybe ::
-     Int   -- ^ Likelihood of 'Nothing'
-  -> Int   -- ^ Likelihood of @'Just' a@
+     Int -- ^ Likelihood of 'Nothing'
+  -> Int -- ^ Likelihood of @'Just' a@
   -> Gen a
   -> Gen (Maybe a)
 genMaybe nLi jLi genA = QC.frequency
     [ (nLi, return Nothing)
     , (jLi, Just <$> genA)
     ]
 
--- | Like 'genMaybe', but with the likelihood of 'Nothing' fixed to @2@. 'QC.frequency'
-genMaybe' ::
-     Int   -- ^ Likelihood of @'Just' a@
-  -> Gen a
+-- | Generate a finite 'Stream' of length @n@.
+genFiniteN ::
+     Int -- ^ Requested size of finite stream.
   -> Gen (Maybe a)
-genMaybe' = genMaybe 2
+  -> Gen (Stream a)
+genFiniteN n gen = Stream Finite <$> replicateM n gen
 
--- | Generate a finite 'Stream' of length @n@.
+-- | Generate a finite 'Stream'.
 genFinite ::
-     Int           -- ^ Requested size of finite stream. Tip: use 'genMaybe'.
-  -> Gen (Maybe a)
+     Gen (Maybe a)
   -> Gen (Stream a)
-genFinite n gen = Stream Finite <$> replicateM n gen
+genFinite gen = Stream Finite <$> QC.listOf gen
 
 -- | Generate an infinite 'Stream'.
 genInfinite ::
-     Gen (Maybe a)  -- ^ Tip: use 'genMaybe'.
+     Gen (Maybe a)
   -> Gen (Stream a)
 genInfinite gen = Stream Infinite <$> QC.infiniteListOf gen

fs-sim/test/Main.hs

@@ -2,12 +2,14 @@ module Main (main) where
 
 import qualified Test.System.FS.Sim.Error
 import qualified Test.System.FS.Sim.FsTree
+import qualified Test.System.FS.Sim.Stream
 import qualified Test.System.FS.StateMachine
 import           Test.Tasty
 
 main :: IO ()
 main = defaultMain $ testGroup "fs-sim-test" [
       Test.System.FS.Sim.Error.tests
     , Test.System.FS.Sim.FsTree.tests
+    , Test.System.FS.Sim.Stream.tests
     , Test.System.FS.StateMachine.tests
     ]

fs-sim/test/Test/System/FS/Sim/Stream.hs

@@ -0,0 +1,65 @@
+{-# LANGUAGE BangPatterns       #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE TypeApplications   #-}
+
+module Test.System.FS.Sim.Stream (tests) where
+
+import           Data.Maybe (isJust, isNothing)
+import           System.FS.Sim.Stream
+import           Test.Tasty
+import           Test.Tasty.QuickCheck
+import           Test.Util
+
+tests :: TestTree
+tests = testGroup "Test.System.FS.Sim.Stream" [
+      testProperty "shrinkCheck InfiniteStream" $
+        \(InfiniteStream s) -> shrinkCheck @Int s
+    , testProperty "shrinkCheck FiniteStream" $
+        \(FiniteStream s) -> shrinkCheck @Int s
+    , testProperty "prop_eventuallyJust InfiniteStream" $
+        \(InfiniteStream s) -> prop_eventuallyJust @Int s
+    , testProperty "prop_eventuallyNothing InfiniteStream" $
+        \(InfiniteStream s) -> prop_eventuallyNothing @Int s
+    , testProperty "prop_eventuallyNothing FiniteStream" $
+        \(FiniteStream s) -> prop_eventuallyNothing @Int s
+    ]
+
+eventually :: (Maybe a -> Bool) -> Stream a -> Property
+eventually p = go 1
+  where
+    go !n s =
+      let (x, s') = runStream s in
+      if p x
+        then tabulate "Number of elements inspected" [showPowersOf 2 n] $ property True
+        else go (n+1) s'
+
+prop_eventuallyJust :: Stream a -> Property
+prop_eventuallyJust = eventually isJust
+
+prop_eventuallyNothing :: Stream a -> Property
+prop_eventuallyNothing = eventually isNothing
+
+-- | A simple property that is expected to fail, but should exercise the
+-- shrinker a little bit.
+shrinkCheck :: Stream a -> Property
+shrinkCheck s = expectFailure $
+    let xs = fst (runStreamN 10 s)
+    in  property $ length (filter isJust xs) /= length (filter isNothing xs)
+
+newtype FiniteStream a = FiniteStream {
+    getFiniteStream :: Stream a
+  }
+  deriving stock Show
+
+instance Arbitrary a => Arbitrary (FiniteStream a) where
+  arbitrary = FiniteStream <$> genFinite arbitrary
+  shrink (FiniteStream s) = FiniteStream <$> shrinkStream s
+
+newtype InfiniteStream a = InfiniteStream {
+    getInfiniteStream :: Stream a
+  }
+  deriving stock Show
+
+instance Arbitrary a => Arbitrary (InfiniteStream a) where
+  arbitrary = InfiniteStream <$> genInfinite arbitrary
+  shrink (InfiniteStream s) = InfiniteStream <$> shrinkStream s