WIP: fix infinite streams

cabal.project

@@ -1,6 +1,6 @@
 index-state:
   -- Bump this if you need newer packages from Hackage
-  , hackage.haskell.org 2024-10-02T00:00:00Z
+  , hackage.haskell.org 2024-12-05T16:34:20Z
 
 packages:
   fs-api

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/Stream.hs

@@ -1,58 +1,59 @@
+{-# 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 +73,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 +101,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 'QC.shrink' will at some point create an infinite sequence 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 tha tthe 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 a 'QC.InfiniteList'.
+--
+-- Infinite streams are shrunk differently than lists that are finite, which is
+-- to ensure that we shrink infinite lists towards finite lists.
 --
--- 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.
+-- * 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.
+--
+-- * 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 ..]]
@@ -155,14 +188,20 @@ genMaybe' ::
 genMaybe' = genMaybe 2
 
 -- | Generate a finite 'Stream' of length @n@.
-genFinite ::
+genFiniteN ::
      Int           -- ^ Requested size of finite stream. Tip: use 'genMaybe'.
   -> Gen (Maybe a)
   -> Gen (Stream a)
-genFinite n gen = Stream Finite <$> replicateM n gen
+genFiniteN n gen = Stream Finite <$> replicateM n gen
+
+-- | Generate a finite 'Stream'.
+genFinite ::
+     Gen (Maybe a) -- ^ Tip: use 'genMaybe'.
+  -> Gen (Stream a)
+genFinite gen = Stream Finite <$> QC.listOf gen
 
 -- | Generate an infinite 'Stream'.
 genInfinite ::
      Gen (Maybe a)  -- ^ Tip: use 'genMaybe'.
   -> Gen (Stream a)
-genInfinite gen = Stream Infinite <$> QC.listOf gen
+genInfinite gen = Stream Infinite <$> QC.infiniteListOf gen

fs-sim/test/Main.hs

@@ -2,6 +2,7 @@ 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
 
@@ -10,4 +11,5 @@ main = defaultMain $ testGroup "fs-sim-test" [
       Test.System.FS.Sim.Error.tests
     , Test.System.FS.Sim.FsTree.tests
     , Test.System.FS.StateMachine.tests
+    , Test.System.FS.Sim.Stream.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