{-# 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 :: ConcIO () -> Test
test ConcIO ()
conc = Assertion -> Test
TestCase (ConcIO () -> Assertion
forall t. (Assertable t, HasCallStack) => t -> Assertion
assert ConcIO ()
conc)

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

assertableP :: Predicate (Either HUnitFailure ())
assertableP :: ProPredicate (Either HUnitFailure ()) (Either HUnitFailure ())
assertableP = (Either Condition (Either HUnitFailure ()) -> Bool)
-> ProPredicate (Either HUnitFailure ()) (Either HUnitFailure ())
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue ((Either Condition (Either HUnitFailure ()) -> Bool)
 -> ProPredicate (Either HUnitFailure ()) (Either HUnitFailure ()))
-> (Either Condition (Either HUnitFailure ()) -> Bool)
-> ProPredicate (Either HUnitFailure ()) (Either HUnitFailure ())
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 :: Program pty IO a -> Test
testAuto = Settings IO a -> Program pty IO a -> Test
forall a pty.
(Eq a, Show a) =>
Settings IO a -> Program pty IO a -> Test
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.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 :: Way -> MemType -> Program pty IO a -> Test
testAutoWay Way
way = Settings IO a -> Program pty IO a -> Test
forall a pty.
(Eq a, Show a) =>
Settings IO a -> Program pty IO a -> Test
testAutoWithSettings (Settings IO a -> Program pty IO a -> Test)
-> (MemType -> Settings IO a)
-> MemType
-> Program pty IO a
-> Test
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.0.0.0
testAutoWithSettings :: (Eq a, Show a)
  => Settings IO a
  -- ^ The SCT settings.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testAutoWithSettings :: Settings IO a -> Program pty IO a -> Test
testAutoWithSettings Settings IO a
settings = Settings IO a
-> [(String, ProPredicate a a)] -> Program pty IO a -> Test
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", 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
  => String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testDejafu :: String -> ProPredicate a b -> Program pty IO a -> Test
testDejafu = Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> Test
forall b a p.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program p IO a -> Test
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.
  -> String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty IO a
  -- ^ The computation to test.
  -> Test
testDejafuWay :: Way
-> MemType
-> String
-> ProPredicate a b
-> Program pty IO a
-> Test
testDejafuWay Way
way = Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> Test
forall b a p.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program p IO a -> Test
testDejafuWithSettings (Settings IO a
 -> String -> ProPredicate a b -> Program pty IO a -> Test)
-> (MemType -> Settings IO a)
-> MemType
-> String
-> ProPredicate a b
-> Program pty IO a
-> Test
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 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 :: Settings IO a
-> String -> ProPredicate a b -> Program p IO a -> Test
testDejafuWithSettings Settings IO a
settings String
name ProPredicate a b
p = Settings IO a
-> [(String, ProPredicate a b)] -> Program p IO a -> Test
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. This will share work between the predicates, rather than
-- running the concurrent computation many times for each predicate.
--
-- @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 :: [(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafus = Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
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.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 :: Way
-> MemType
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> Test
testDejafusWay Way
way = Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
forall b a pty.
Show b =>
Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafusWithSettings (Settings IO a
 -> [(String, ProPredicate a b)] -> Program pty IO a -> Test)
-> (MemType -> Settings IO a)
-> MemType
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> Test
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.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 :: Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
testDejafusWithSettings = Settings IO a
-> [(String, ProPredicate a b)] -> Program pty IO a -> Test
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 :: String -> p -> Test
testProperty = Int -> Int -> String -> p -> Test
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 :: Int -> Int -> String -> p -> Test
testPropertyFor = Int -> Int -> String -> p -> Test
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 :: 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 ((String, ProPredicate a b) -> Test)
-> [(String, ProPredicate a b)] -> [Test]
forall a b. (a -> b) -> [a] -> [b]
map (String, ProPredicate a b) -> Test
forall b. Show b => (String, ProPredicate a b) -> Test
toTest [(String, ProPredicate a b)]
tests of
  [Test
t] -> Test
t
  [Test]
ts  -> [Test] -> Test
TestList [Test]
ts

  where
    toTest :: (String, ProPredicate a b) -> Test
toTest (String
name, ProPredicate a b
p) = String -> Test -> Test
TestLabel String
name (Test -> Test) -> (Assertion -> Test) -> Assertion -> Test
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ do
      let 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 Lens' (Settings IO a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
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)
      [(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 Lens' (Settings IO a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
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
      HasCallStack => String -> Assertion
String -> Assertion
assertString (String -> Assertion)
-> (Result b -> String) -> Result b -> Assertion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result b -> String
forall a. Show a => Result a -> String
showErr (Result b -> Assertion) -> Result b -> Assertion
forall a b. (a -> b) -> a -> b
$ 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 [(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 :: Int -> Int -> String -> p -> Test
testprop Int
sn Int
vn String
name p
p = String -> Test -> Test
TestLabel String
name (Test -> Test) -> (Assertion -> Test) -> Assertion -> Test
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ 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
  case Maybe (FailedProperty (O p) (X p))
ce of
    Just FailedProperty (O p) (X p)
c -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure (String -> Assertion) -> (String -> String) -> String -> Assertion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
init (String -> Assertion) -> String -> Assertion
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"*** Failure: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
        (if [String] -> 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 (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 (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 -> () -> Assertion
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 :: 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 (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 (String -> String
indent (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
forall a. Show a => (Either Condition a, Trace) -> String
showres) ([(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

  showres :: (Either Condition a, Trace) -> String
showres (Either Condition a
r, Trace
t) = (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

  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 :: [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