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

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

  -- | This is supported by the 'Assertable' and 'Testable' instances
  -- for 'ConcIO'.  These instances try all executions, reporting as
  -- failures the cases which throw an 'HUnitFailure' exception.
  --
  -- @instance Testable   (ConcIO ())@
  -- @instance Assertable (ConcIO ())@
  --
  -- These instances use 'defaultWay' and 'defaultMemType'.

  -- * 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           Control.Monad.Catch    (try)
import qualified Data.Foldable          as F
import           Data.List              (intercalate, intersperse)
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.HUnit             (Assertable(..), Test(..), Testable(..),
                                         assertFailure, assertString)
import           Test.HUnit.Lang        (HUnitFailure(..))

--------------------------------------------------------------------------------
-- HUnit-style unit testing

-- | @since 0.3.0.0
instance Testable (Conc.ConcIO ()) where
  test :: HasCallStack => ConcIO () -> Test
test ConcIO ()
conc = Assertion -> Test
TestCase (forall t. (Assertable t, HasCallStack) => t -> Assertion
assert ConcIO ()
conc)

-- | @since 0.3.0.0
instance Assertable (Conc.ConcIO ()) where
  assert :: HasCallStack => ConcIO () -> Assertion
assert ConcIO ()
conc = do
    [(Either Condition (Either HUnitFailure ()), Trace)]
traces <- forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
SCT.runSCTWithSettings (forall s a. Lens' s a -> a -> s -> s
set forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard (forall a. a -> Maybe a
Just (forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard Predicate (Either HUnitFailure ())
assertableP)) forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings) (forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> m (Either e a)
try ConcIO ()
conc)
    HasCallStack => String -> Assertion
assertString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Result a -> String
showErr forall a b. (a -> b) -> a -> b
$ forall a b.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval Predicate (Either HUnitFailure ())
assertableP [(Either Condition (Either HUnitFailure ()), Trace)]
traces

assertableP :: Predicate (Either HUnitFailure ())
assertableP :: Predicate (Either HUnitFailure ())
assertableP = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue forall a b. (a -> b) -> a -> b
$ \case
  Right (Left HUnitFailure {}) -> Bool
False
  Either Condition (Either HUnitFailure ())
_ -> Bool
True


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

-- | Automatically test a computation. In particular, look for
-- deadlocks, uncaught exceptions, and multiple return values.
--
-- @since 2.0.0.0
testAuto :: (Eq a, Show a)
  => Program pty IO a
  -- ^ The computation to test.
  -> Test
testAuto :: forall a pty. (Eq a, Show a) => Program pty IO a -> Test
testAuto = forall a pty.
(Eq a, Show a) =>
Settings IO a -> Program pty IO a -> Test
testAutoWithSettings 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.0.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.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testAutoWay :: forall a pty.
(Eq a, Show a) =>
Way -> MemType -> Program pty IO a -> Test
testAutoWay Way
way = forall a pty.
(Eq a, Show a) =>
Settings IO a -> Program pty IO a -> Test
testAutoWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

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

-- | Check that a predicate holds.
--
-- @since 2.0.0.0
testDejafu :: Show b
  => String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testDejafu :: forall b a pty.
Show b =>
String -> ProPredicate a b -> Program pty IO a -> Test
testDejafu = forall b a p.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program p IO a -> Test
testDejafuWithSettings 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.
  -> String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testDejafuWay :: forall b a pty.
Show b =>
Way
-> MemType
-> String
-> ProPredicate a b
-> Program pty IO a
-> Test
testDejafuWay Way
way = forall b a p.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program p IO a -> Test
testDejafuWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 SCT settings.
  -> String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program p IO a
  -- ^ The computation to test.
  -> Test
testDejafuWithSettings :: forall b a p.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program p IO a -> Test
testDejafuWithSettings Settings IO a
settings String
name ProPredicate a b
p = forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafusWithSettings Settings IO a
settings [(String
name, ProPredicate a b
p)]

-- | Variant of 'testDejafu' which takes a collection of predicates to
-- test.
--
-- @since 2.0.0.0
testDejafus :: Show b
  => [(String, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testDejafus :: forall b a pty.
Show b =>
[(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafus = forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafusWithSettings 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.0.0.0
testDejafusWay :: Show b
  => Way
  -- ^ How to execute the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> [(String, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testDejafusWay :: forall b a pty.
Show b =>
Way
-> MemType
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> Test
testDejafusWay Way
way = forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafusWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'testDejafus' which takes a settings record.
--
-- @since 2.0.0.0
testDejafusWithSettings :: Show b
  => Settings IO a
  -- ^ The SCT settings.
  -> [(String, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testDejafusWithSettings :: forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafusWithSettings = forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testconc


-------------------------------------------------------------------------------
-- 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))
  => String
  -- ^ The name of the test.
  -> p
  -- ^ The property to check.
  -> Test
testProperty :: forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
String -> p -> Test
testProperty = forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> Test
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.
  -> String
  -- ^ The name of the test.
  -> p
  -- ^ The property to check.
  -> Test
testPropertyFor :: forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> Test
testPropertyFor = forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> Test
testprop


--------------------------------------------------------------------------------
-- HUnit integration

-- | Produce a HUnit 'Test' from a Deja Fu unit test.
testconc :: Show b
  => Settings IO a
  -> [(String, ProPredicate a b)]
  -> Program pty IO a
  -> Test
testconc :: forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testconc Settings IO a
settings [(String, ProPredicate a b)]
tests Program pty IO a
concio = case forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Show a => (String, ProPredicate a a) -> Test
toTest [(String, ProPredicate a b)]
tests of
  [Test
t] -> Test
t
  [Test]
ts  -> [Test] -> Test
TestList [Test]
ts

  where
    toTest :: (String, ProPredicate a a) -> Test
toTest (String
name, ProPredicate a a
p) = String -> Test -> Test
TestLabel String
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assertion -> Test
TestCase forall a b. (a -> b) -> a -> b
$ do
      let discarder :: Either Condition a -> Maybe Discard
discarder = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
D.strengthenDiscard (forall s a. Lens' s a -> s -> a
get forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard Settings IO a
settings) (forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate a a
p)
      [(Either Condition a, Trace)]
traces <- forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
SCT.runSCTWithSettings (forall s a. Lens' s a -> a -> s -> s
set forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard (forall a. a -> Maybe a
Just Either Condition a -> Maybe Discard
discarder) Settings IO a
settings) Program pty IO a
concio
      HasCallStack => String -> Assertion
assertString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Result a -> String
showErr forall a b. (a -> b) -> a -> b
$ forall a b.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a a
p [(Either Condition a, Trace)]
traces

-- | Produce a HUnit 'Test' 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 -> String -> p -> Test
testprop :: forall p.
(Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) =>
Int -> Int -> String -> p -> Test
testprop Int
sn Int
vn String
name p
p = String -> Test -> Test
TestLabel String
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assertion -> Test
TestCase forall a b. (a -> b) -> a -> b
$ do
  Maybe (FailedProperty (O p) (X p))
ce <- 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
  case Maybe (FailedProperty (O p) (X p))
ce of
    Just FailedProperty (O p) (X p)
c -> forall a. HasCallStack => String -> IO a
assertFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
init forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"*** Failure: " forall a. [a] -> [a] -> [a]
++
        (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall o x. FailedProperty o x -> [String]
R.failingArgs FailedProperty (O p) (X p)
c) then String
"" else [String] -> String
unwords (forall o x. FailedProperty o x -> [String]
R.failingArgs FailedProperty (O p) (X p)
c) forall a. [a] -> [a] -> [a]
++ String
" ") forall a. [a] -> [a] -> [a]
++
        String
"(seed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall o x. FailedProperty o x -> x
R.failingSeed FailedProperty (O p) (X p)
c) forall a. [a] -> [a] -> [a]
++ String
")"
      , String
"    left:  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList forall a b. (a -> b) -> a -> b
$ forall o x. FailedProperty o x -> Set (Maybe Condition, o)
R.leftResults  FailedProperty (O p) (X p)
c)
      , String
"    right: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList forall a b. (a -> b) -> a -> b
$ 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


--------------------------------------------------------------------------------
-- Utilities

-- | 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
  | forall a. Result a -> Bool
_pass Result a
res = String
""
  | Bool
otherwise = String
"Failed:\n" forall a. [a] -> [a] -> [a]
++ String
msg forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
failures forall a. [a] -> [a] -> [a]
++ String
rest where

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

  failures :: [String]
failures = forall a. a -> [a] -> [a]
intersperse String
"" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (String -> String
indent forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {b}. Show b => (Either Condition b, Trace) -> String
showres) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
5 forall a b. (a -> b) -> a -> b
$ forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
res

  showres :: (Either Condition b, Trace) -> String
showres (Either Condition b
r, Trace
t) = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> String
Conc.showCondition forall a. Show a => a -> String
show Either Condition b
r forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Trace -> String
Conc.showTrace Trace
t

  rest :: String
rest = if forall a. [a] -> Int -> Bool
moreThan (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 forall a. Ord a => a -> a -> Bool
< Int
0
moreThan [a]
_ Int
0  = Bool
True
moreThan (a
_:[a]
xs) Int
n = forall a. [a] -> Int -> Bool
moreThan [a]
xs (Int
nforall a. Num a => a -> a -> a
-Int
1)

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