{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module      : Test.Tasty.DejaFu
-- Copyright   : (c) 2015--2022 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : stable
-- Portability : FlexibleContexts, FlexibleInstances, GADTs, LambdaCase
--
-- This module allows using Deja Fu predicates with Tasty to test the
-- behaviour of concurrent systems.
module Test.Tasty.DejaFu
  ( -- * Unit testing

  -- | This is supported by an 'IsTest' instance for 'ConcIO'.  This
  -- instance tries all executions, reporting as failures the cases
  -- which return a 'Just' string.
  --
  -- @instance IsTest (ConcIO (Maybe String))@
  -- @instance IsOption Bounds@
  -- @instance IsOption MemType@

  -- * Unit testing
    testAuto
  , testDejafu
  , testDejafus

  , testAutoWay
  , testDejafuWay
  , testDejafusWay

  , testAutoWithSettings
  , testDejafuWithSettings
  , testDejafusWithSettings

  -- ** Re-exports
  , Condition
  , Predicate
  , ProPredicate(..)
  -- *** Settings
  , module Test.DejaFu.Settings
  -- *** Expressing concurrent programs
  , Program
  , Basic
  , ConcT
  , ConcIO
  , WithSetup
  , WithSetupAndTeardown
  , withSetup
  , withTeardown
  , withSetupAndTeardown
  -- *** Invariants
  , Invariant
  , registerInvariant
  , inspectIORef
  , inspectMVar
  , inspectTVar

  -- * Refinement property testing
  , testProperty
  , testPropertyFor

  -- ** Re-exports
  , R.Sig(..)
  , R.RefinementProperty
  , R.Testable(..)
  , R.Listable(..)
  , R.expectFailure
  , R.refines, (R.=>=)
  , R.strictlyRefines, (R.->-)
  , R.equivalentTo, (R.===)
) where

import           Data.Char              (toUpper)
import qualified Data.Foldable          as F
import           Data.List              (intercalate, intersperse)
import           Data.Proxy             (Proxy(..))
import           Data.Tagged            (Tagged(..))
import           Data.Typeable          (Typeable)
import           System.Random          (mkStdGen)
import           Test.DejaFu            hiding (Testable(..))
import qualified Test.DejaFu.Conc       as Conc
import qualified Test.DejaFu.Refinement as R
import qualified Test.DejaFu.SCT        as SCT
import qualified Test.DejaFu.Settings
import qualified Test.DejaFu.Types      as D
import           Test.Tasty             (TestName, TestTree, testGroup)
import           Test.Tasty.Options     (IsOption(..), OptionDescription(..),
                                         lookupOption)
import           Test.Tasty.Providers   (IsTest(..), singleTest, testFailed,
                                         testPassed)

--------------------------------------------------------------------------------
-- Tasty-style unit testing

-- | @since 0.3.0.0
instance IsTest (Conc.ConcIO (Maybe String)) where
  testOptions :: Tagged (ConcIO (Maybe String)) [OptionDescription]
testOptions = [OptionDescription]
-> Tagged (ConcIO (Maybe String)) [OptionDescription]
forall {k} (s :: k) b. b -> Tagged s b
Tagged [OptionDescription]
concOptions

  run :: OptionSet
-> ConcIO (Maybe String) -> (Progress -> IO ()) -> IO Result
run OptionSet
options ConcIO (Maybe String)
conc Progress -> IO ()
callback = do
    let memtype :: MemType
memtype = OptionSet -> MemType
forall v. IsOption v => OptionSet -> v
lookupOption OptionSet
options
    let way :: Way
way     = OptionSet -> Way
forall v. IsOption v => OptionSet -> v
lookupOption OptionSet
options
    let traces :: IO [(Either Condition (Maybe String), Trace)]
traces  = Settings IO (Maybe String)
-> ConcIO (Maybe String)
-> IO [(Either Condition (Maybe String), Trace)]
forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
SCT.runSCTWithSettings (Lens'
  (Settings IO (Maybe String))
  (Maybe (Either Condition (Maybe String) -> Maybe Discard))
-> Maybe (Either Condition (Maybe String) -> Maybe Discard)
-> Settings IO (Maybe String)
-> Settings IO (Maybe String)
forall s a. Lens' s a -> a -> s -> s
set (Maybe (Either Condition (Maybe String) -> Maybe Discard)
 -> f (Maybe (Either Condition (Maybe String) -> Maybe Discard)))
-> Settings IO (Maybe String) -> f (Settings IO (Maybe String))
Lens'
  (Settings IO (Maybe String))
  (Maybe (Either Condition (Maybe String) -> Maybe Discard))
forall (n :: * -> *) a (f :: * -> *).
Functor f =>
(Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
ldiscard ((Either Condition (Maybe String) -> Maybe Discard)
-> Maybe (Either Condition (Maybe String) -> Maybe Discard)
forall a. a -> Maybe a
Just (ProPredicate (Maybe String) (Maybe String)
-> Either Condition (Maybe String) -> Maybe Discard
forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate (Maybe String) (Maybe String)
assertableP)) (Way -> MemType -> Settings IO (Maybe String)
forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way MemType
memtype)) ConcIO (Maybe String)
conc
    OptionSet -> ConcTest -> (Progress -> IO ()) -> IO Result
forall t.
IsTest t =>
OptionSet -> t -> (Progress -> IO ()) -> IO Result
run OptionSet
options (IO [(Either Condition (Maybe String), Trace)]
-> ([(Either Condition (Maybe String), Trace)]
    -> Result (Maybe String))
-> ConcTest
forall p a.
Show p =>
IO [(Either Condition a, Trace)]
-> ([(Either Condition a, Trace)] -> Result p) -> ConcTest
ConcTest IO [(Either Condition (Maybe String), Trace)]
traces (ProPredicate (Maybe String) (Maybe String)
-> [(Either Condition (Maybe String), Trace)]
-> Result (Maybe String)
forall a b.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate (Maybe String) (Maybe String)
assertableP)) Progress -> IO ()
callback

concOptions :: [OptionDescription]
concOptions :: [OptionDescription]
concOptions =
  [ Proxy MemType -> OptionDescription
forall v. IsOption v => Proxy v -> OptionDescription
Option (Proxy MemType
forall {k} (t :: k). Proxy t
Proxy :: Proxy MemType)
  , Proxy Way -> OptionDescription
forall v. IsOption v => Proxy v -> OptionDescription
Option (Proxy Way
forall {k} (t :: k). Proxy t
Proxy :: Proxy Way)
  ]

assertableP :: Predicate (Maybe String)
assertableP :: ProPredicate (Maybe String) (Maybe String)
assertableP = (Either Condition (Maybe String) -> Bool)
-> ProPredicate (Maybe String) (Maybe String)
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue ((Either Condition (Maybe String) -> Bool)
 -> ProPredicate (Maybe String) (Maybe String))
-> (Either Condition (Maybe String) -> Bool)
-> ProPredicate (Maybe String) (Maybe String)
forall a b. (a -> b) -> a -> b
$ \case
  Right (Just String
_) -> Bool
False
  Either Condition (Maybe String)
_ -> Bool
True

-- | @since 0.3.0.0
instance IsOption MemType where
  defaultValue :: MemType
defaultValue = MemType
defaultMemType
  parseValue :: String -> Maybe MemType
parseValue = String -> Maybe MemType
shortName (String -> Maybe MemType)
-> (String -> String) -> String -> Maybe MemType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper where
    shortName :: String -> Maybe MemType
shortName String
"SC"  = MemType -> Maybe MemType
forall a. a -> Maybe a
Just MemType
SequentialConsistency
    shortName String
"TSO" = MemType -> Maybe MemType
forall a. a -> Maybe a
Just MemType
TotalStoreOrder
    shortName String
"PSO" = MemType -> Maybe MemType
forall a. a -> Maybe a
Just MemType
PartialStoreOrder
    shortName String
_ = Maybe MemType
forall a. Maybe a
Nothing
  optionName :: Tagged MemType String
optionName = String -> Tagged MemType String
forall {k} (s :: k) b. b -> Tagged s b
Tagged String
"memory-model"
  optionHelp :: Tagged MemType String
optionHelp = String -> Tagged MemType String
forall {k} (s :: k) b. b -> Tagged s b
Tagged String
"The memory model to use. This should be one of \"sc\", \"tso\", or \"pso\"."

-- | @since 0.5.0.0
instance IsOption Way where
  defaultValue :: Way
defaultValue = Way
defaultWay
  parseValue :: String -> Maybe Way
parseValue = String -> Maybe Way
shortName (String -> Maybe Way) -> (String -> String) -> String -> Maybe Way
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper where
    shortName :: String -> Maybe Way
shortName String
"SYSTEMATICALLY" = Way -> Maybe Way
forall a. a -> Maybe a
Just (Bounds -> Way
systematically Bounds
defaultBounds)
    shortName String
"RANDOMLY"       = Way -> Maybe Way
forall a. a -> Maybe a
Just (StdGen -> Int -> Way
forall g. RandomGen g => g -> Int -> Way
randomly (Int -> StdGen
mkStdGen Int
42) Int
100)
    shortName String
_ = Maybe Way
forall a. Maybe a
Nothing
  optionName :: Tagged Way String
optionName = String -> Tagged Way String
forall {k} (s :: k) b. b -> Tagged s b
Tagged String
"way"
  optionHelp :: Tagged Way String
optionHelp = String -> Tagged Way String
forall {k} (s :: k) b. b -> Tagged s b
Tagged String
"The execution method to use. This should be one of \"systematically\" or \"randomly\"."


--------------------------------------------------------------------------------
-- DejaFu-style unit testing

-- | Automatically test a computation. In particular, look for
-- deadlocks, uncaught exceptions, and multiple return values.
--
-- @since 2.1.0.0
testAuto :: (Eq a, Show a)
  => TestName
  -- ^ The name of the test group.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testAuto :: forall a pty.
(Eq a, Show a) =>
String -> Program pty IO a -> TestTree
testAuto = Settings IO a -> String -> Program pty IO a -> TestTree
forall a pty.
(Eq a, Show a) =>
Settings IO a -> String -> Program pty IO a -> TestTree
testAutoWithSettings Settings IO a
forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings

-- | Variant of 'testAuto' which tests a computation under a given
-- execution way and memory model.
--
-- @since 2.1.0.0
testAutoWay :: (Eq a, Show a)
  => Way
  -- ^ How to execute the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> TestName
  -- ^ The name of the test group.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testAutoWay :: forall a pty.
(Eq a, Show a) =>
Way -> MemType -> String -> Program pty IO a -> TestTree
testAutoWay Way
way = Settings IO a -> String -> Program pty IO a -> TestTree
forall a pty.
(Eq a, Show a) =>
Settings IO a -> String -> Program pty IO a -> TestTree
testAutoWithSettings (Settings IO a -> String -> Program pty IO a -> TestTree)
-> (MemType -> Settings IO a)
-> MemType
-> String
-> Program pty IO a
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings IO a
forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'testAuto' which takes a settings record.
--
-- @since 2.1.0.0
testAutoWithSettings :: (Eq a, Show a)
  => Settings IO a
  -- ^ The SCT settings.
  -> TestName
  -- ^ The name of the test group.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testAutoWithSettings :: forall a pty.
(Eq a, Show a) =>
Settings IO a -> String -> Program pty IO a -> TestTree
testAutoWithSettings Settings IO a
settings String
groupName = Settings IO a
-> String
-> [(String, ProPredicate a a)]
-> Program pty IO a
-> TestTree
forall b a pty.
Show b =>
Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
testDejafusWithSettings Settings IO a
settings String
groupName
  [(String
"Never Deadlocks", ProPredicate a a -> ProPredicate a a
forall b a. Eq b => ProPredicate a b -> ProPredicate a b
representative ProPredicate a a
forall a. Predicate a
deadlocksNever)
  , (String
"No Exceptions", ProPredicate a a -> ProPredicate a a
forall b a. Eq b => ProPredicate a b -> ProPredicate a b
representative ProPredicate a a
forall a. Predicate a
exceptionsNever)
  , (String
"Consistent Result", ProPredicate a a
forall a. Eq a => Predicate a
alwaysSame)
  ]

-- | Check that a predicate holds.
--
-- @since 2.0.0.0
testDejafu :: Show b
  => TestName
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testDejafu :: forall b a pty.
Show b =>
String -> ProPredicate a b -> Program pty IO a -> TestTree
testDejafu = Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> TestTree
forall b a pty.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> TestTree
testDejafuWithSettings Settings IO a
forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings

-- | Variant of 'testDejafu' which takes a way to execute the program
-- and a memory model.
--
-- @since 2.0.0.0
testDejafuWay :: Show b
  => Way
  -- ^ How to execute the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> TestName
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testDejafuWay :: forall b a pty.
Show b =>
Way
-> MemType
-> String
-> ProPredicate a b
-> Program pty IO a
-> TestTree
testDejafuWay Way
way = Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> TestTree
forall b a pty.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> TestTree
testDejafuWithSettings (Settings IO a
 -> String -> ProPredicate a b -> Program pty IO a -> TestTree)
-> (MemType -> Settings IO a)
-> MemType
-> String
-> ProPredicate a b
-> Program pty IO a
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings IO a
forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'testDejafu' which takes a settings record.
--
-- @since 2.0.0.0
testDejafuWithSettings :: Show b
  => Settings IO a
  -- ^ The settings record
  -> TestName
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testDejafuWithSettings :: forall b a pty.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> TestTree
testDejafuWithSettings Settings IO a
settings String
name ProPredicate a b
p Program pty IO a
concio =
  Settings IO a
-> Program pty IO a -> (String, ProPredicate a b) -> TestTree
forall b a pty.
Show b =>
Settings IO a
-> Program pty IO a -> (String, ProPredicate a b) -> TestTree
testconc Settings IO a
settings Program pty IO a
concio (String
name, ProPredicate a b
p)

-- | Variant of 'testDejafu' which takes a collection of predicates to
-- test.
--
-- @since 2.1.0.0
testDejafus :: Show b
  => TestName
  -- ^ The name of the test group.
  -> [(TestName, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testDejafus :: forall b a pty.
Show b =>
String
-> [(String, ProPredicate a b)] -> Program pty IO a -> TestTree
testDejafus = Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
forall b a pty.
Show b =>
Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
testDejafusWithSettings Settings IO a
forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings

-- | Variant of 'testDejafus' which takes a way to execute the program
-- and a memory model.
--
-- @since 2.1.0.0
testDejafusWay :: Show b
  => Way
  -- ^ How to execute the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> TestName
  -- ^ The name of the test group.
  -> [(TestName, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testDejafusWay :: forall b a pty.
Show b =>
Way
-> MemType
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
testDejafusWay Way
way = Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
forall b a pty.
Show b =>
Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
testDejafusWithSettings (Settings IO a
 -> String
 -> [(String, ProPredicate a b)]
 -> Program pty IO a
 -> TestTree)
-> (MemType -> Settings IO a)
-> MemType
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings IO a
forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'testDejafus' which takes a settings record.
--
-- @since 2.1.0.0
testDejafusWithSettings :: Show b
  => Settings IO a
  -- ^ The SCT settings.
  -> TestName
  -- ^ The name of the test group.
  -> [(TestName, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> TestTree
testDejafusWithSettings :: forall b a pty.
Show b =>
Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
testDejafusWithSettings Settings IO a
settings String
groupName [(String, ProPredicate a b)]
tests Program pty IO a
concio =
  String -> [TestTree] -> TestTree
testGroup String
groupName ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ ((String, ProPredicate a b) -> TestTree)
-> [(String, ProPredicate a b)] -> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
map (Settings IO a
-> Program pty IO a -> (String, ProPredicate a b) -> TestTree
forall b a pty.
Show b =>
Settings IO a
-> Program pty IO a -> (String, ProPredicate a b) -> TestTree
testconc Settings IO a
settings Program pty IO a
concio) [(String, ProPredicate a b)]
tests


-------------------------------------------------------------------------------
-- Refinement property testing

-- | Check a refinement property with a variety of seed values and
-- variable assignments.
--
-- @since 0.6.0.0
testProperty :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
  => TestName
  -- ^ The name of the test.
  -> p
  -- ^ The property to check.
  -> TestTree
testProperty :: forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
String -> p -> TestTree
testProperty = Int -> Int -> String -> p -> TestTree
forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> TestTree
testPropertyFor Int
10 Int
100

-- | Like 'testProperty', but takes a number of cases to check.
--
-- The maximum number of cases tried by @testPropertyFor n m@ will be
-- @n * m@.
--
-- @since 0.7.1.0
testPropertyFor :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
  => Int
  -- ^ The number of seed values to try.
  -> Int
  -- ^ The number of variable assignments per seed value to try.
  -> TestName
  -- ^ The name of the test.
  -> p
  -- ^ The property to check.
  -> TestTree
testPropertyFor :: forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> TestTree
testPropertyFor = Int -> Int -> String -> p -> TestTree
forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> TestTree
testprop


--------------------------------------------------------------------------------
-- Tasty integration

data ConcTest where
  ConcTest :: Show b => IO [(Either Condition a, Conc.Trace)] -> ([(Either Condition a, Conc.Trace)] -> Result b) -> ConcTest
  deriving Typeable

data PropTest where
  PropTest :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p)) => Int -> Int -> p -> PropTest
  deriving Typeable

instance IsTest ConcTest where
  testOptions :: Tagged ConcTest [OptionDescription]
testOptions = [OptionDescription] -> Tagged ConcTest [OptionDescription]
forall a. a -> Tagged ConcTest a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

  run :: OptionSet -> ConcTest -> (Progress -> IO ()) -> IO Result
run OptionSet
_ (ConcTest IO [(Either Condition a, Trace)]
iotraces [(Either Condition a, Trace)] -> Result b
p) Progress -> IO ()
_ = do
    [(Either Condition a, Trace)]
traces <- IO [(Either Condition a, Trace)]
iotraces
    let err :: String
err = Result b -> String
forall a. Show a => Result a -> String
showErr (Result b -> String) -> Result b -> String
forall a b. (a -> b) -> a -> b
$ [(Either Condition a, Trace)] -> Result b
p [(Either Condition a, Trace)]
traces
    Result -> IO Result
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
err then String -> Result
testPassed String
"" else String -> Result
testFailed String
err)

instance IsTest PropTest where
  testOptions :: Tagged PropTest [OptionDescription]
testOptions = [OptionDescription] -> Tagged PropTest [OptionDescription]
forall a. a -> Tagged PropTest a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

  run :: OptionSet -> PropTest -> (Progress -> IO ()) -> IO Result
run OptionSet
_ (PropTest Int
sn Int
vn p
p) Progress -> IO ()
_ = do
    Maybe (FailedProperty (O p) (X p))
ce <- Int -> Int -> p -> IO (Maybe (FailedProperty (O p) (X p)))
forall p.
(Testable p, Listable (X p)) =>
Int -> Int -> p -> IO (Maybe (FailedProperty (O p) (X p)))
R.checkFor Int
sn Int
vn p
p
    Result -> IO Result
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result -> IO Result) -> Result -> IO Result
forall a b. (a -> b) -> a -> b
$ case Maybe (FailedProperty (O p) (X p))
ce of
      Just FailedProperty (O p) (X p)
c -> String -> Result
testFailed (String -> Result) -> (String -> String) -> String -> Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. HasCallStack => [a] -> [a]
init (String -> Result) -> String -> Result
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
        [ String
"*** Failure: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
          (if [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (FailedProperty (O p) (X p) -> [String]
forall o x. FailedProperty o x -> [String]
R.failingArgs FailedProperty (O p) (X p)
c) then String
"" else [String] -> String
unwords (FailedProperty (O p) (X p) -> [String]
forall o x. FailedProperty o x -> [String]
R.failingArgs FailedProperty (O p) (X p)
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ") String -> String -> String
forall a. [a] -> [a] -> [a]
++
          String
"(seed " String -> String -> String
forall a. [a] -> [a] -> [a]
++ X p -> String
forall a. Show a => a -> String
show (FailedProperty (O p) (X p) -> X p
forall o x. FailedProperty o x -> x
R.failingSeed FailedProperty (O p) (X p)
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        , String
"    left:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Maybe Condition, O p)] -> String
forall a. Show a => a -> String
show (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)])
-> Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a b. (a -> b) -> a -> b
$ FailedProperty (O p) (X p) -> Set (Maybe Condition, O p)
forall o x. FailedProperty o x -> Set (Maybe Condition, o)
R.leftResults  FailedProperty (O p) (X p)
c)
        , String
"    right: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Maybe Condition, O p)] -> String
forall a. Show a => a -> String
show (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (Set (Maybe Condition, O p) -> [(Maybe Condition, O p)])
-> Set (Maybe Condition, O p) -> [(Maybe Condition, O p)]
forall a b. (a -> b) -> a -> b
$ FailedProperty (O p) (X p) -> Set (Maybe Condition, O p)
forall o x. FailedProperty o x -> Set (Maybe Condition, o)
R.rightResults FailedProperty (O p) (X p)
c)
        ]
      Maybe (FailedProperty (O p) (X p))
Nothing -> String -> Result
testPassed String
""

-- | Produce a Tasty 'Test' from a Deja Fu unit test.
testconc :: Show b
  => Settings IO a
  -> Program pty IO a
  -> (TestName, ProPredicate a b)
  -> TestTree
testconc :: forall b a pty.
Show b =>
Settings IO a
-> Program pty IO a -> (String, ProPredicate a b) -> TestTree
testconc Settings IO a
settings Program pty IO a
concio (String
name, ProPredicate a b
p) = String -> ConcTest -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
name (ConcTest -> TestTree) -> ConcTest -> TestTree
forall a b. (a -> b) -> a -> b
$ IO [(Either Condition a, Trace)]
-> ([(Either Condition a, Trace)] -> Result b) -> ConcTest
forall p a.
Show p =>
IO [(Either Condition a, Trace)]
-> ([(Either Condition a, Trace)] -> Result p) -> ConcTest
ConcTest IO [(Either Condition a, Trace)]
traces (ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
forall a b.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a b
p) where
  discarder :: Either Condition a -> Maybe Discard
discarder = ((Either Condition a -> Maybe Discard)
 -> Either Condition a -> Maybe Discard)
-> ((Either Condition a -> Maybe Discard)
    -> (Either Condition a -> Maybe Discard)
    -> Either Condition a
    -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Either Condition a -> Maybe Discard)
-> Either Condition a -> Maybe Discard
forall a. a -> a
id (Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
D.strengthenDiscard (Lens' (Settings IO a) (Maybe (Either Condition a -> Maybe Discard))
-> Settings IO a -> Maybe (Either Condition a -> Maybe Discard)
forall s a. Lens' s a -> s -> a
get (Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings IO a -> f (Settings IO a)
Lens' (Settings IO a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a (f :: * -> *).
Functor f =>
(Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
ldiscard Settings IO a
settings) (ProPredicate a b -> Either Condition a -> Maybe Discard
forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate a b
p)
  traces :: IO [(Either Condition a, Trace)]
traces    = Settings IO a
-> Program pty IO a -> IO [(Either Condition a, Trace)]
forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
SCT.runSCTWithSettings (Lens' (Settings IO a) (Maybe (Either Condition a -> Maybe Discard))
-> Maybe (Either Condition a -> Maybe Discard)
-> Settings IO a
-> Settings IO a
forall s a. Lens' s a -> a -> s -> s
set (Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings IO a -> f (Settings IO a)
Lens' (Settings IO a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a (f :: * -> *).
Functor f =>
(Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
ldiscard ((Either Condition a -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
forall a. a -> Maybe a
Just Either Condition a -> Maybe Discard
discarder) Settings IO a
settings) Program pty IO a
concio

-- | Produce a Tasty 'TestTree' from a Deja Fu refinement property test.
testprop :: (R.Testable p, R.Listable (R.X p), Eq (R.X p), Show (R.X p), Show (R.O p))
  => Int -> Int -> TestName -> p -> TestTree
testprop :: forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> TestTree
testprop Int
sn Int
vn String
name = String -> PropTest -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
name (PropTest -> TestTree) -> (p -> PropTest) -> p -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> p -> PropTest
forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> p -> PropTest
PropTest Int
sn Int
vn

-- | Convert a test result into an error message on failure (empty
-- string on success).
showErr :: Show a => Result a -> String
showErr :: forall a. Show a => Result a -> String
showErr Result a
res
  | Result a -> Bool
forall a. Result a -> Bool
_pass Result a
res = String
""
  | Bool
otherwise = String
"Failed:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
failures String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rest where

  msg :: String
msg = if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Result a -> String
forall a. Result a -> String
_failureMsg Result a
res) then String
"" else Result a -> String
forall a. Result a -> String
_failureMsg Result a
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"

  failures :: [String]
failures = String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
"" ([String] -> [String])
-> ([(Either Condition a, Trace)] -> [String])
-> [(Either Condition a, Trace)]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Either Condition a, Trace) -> String)
-> [(Either Condition a, Trace)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Either Condition a
r, Trace
t) -> String -> String
indent (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Condition -> String)
-> (a -> String) -> Either Condition a -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> String
Conc.showCondition a -> String
forall a. Show a => a -> String
show Either Condition a
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Trace -> String
Conc.showTrace Trace
t) ([(Either Condition a, Trace)] -> [String])
-> ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)])
-> [(Either Condition a, Trace)]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. Int -> [a] -> [a]
take Int
5 ([(Either Condition a, Trace)] -> [String])
-> [(Either Condition a, Trace)] -> [String]
forall a b. (a -> b) -> a -> b
$ Result a -> [(Either Condition a, Trace)]
forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
res

  rest :: String
rest = if [(Either Condition a, Trace)] -> Int -> Bool
forall a. [a] -> Int -> Bool
moreThan (Result a -> [(Either Condition a, Trace)]
forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
res) Int
5 then String
"\n\t..." else String
""

-- | Check if a list has more than some number of elements.
moreThan :: [a] -> Int -> Bool
moreThan :: forall a. [a] -> Int -> Bool
moreThan [] Int
n = Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
moreThan [a]
_ Int
0  = Bool
True
moreThan (a
_:[a]
xs) Int
n = [a] -> Int -> Bool
forall a. [a] -> Int -> Bool
moreThan [a]
xs (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

-- | Indent every line of a string.
indent :: String -> String
indent :: String -> String
indent = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char
'\t'Char -> String -> String
forall a. a -> [a] -> [a]
:) ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines