{-# 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 = 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 = forall v. IsOption v => OptionSet -> v
lookupOption OptionSet
options
    let way :: Way
way     = forall v. IsOption v => OptionSet -> v
lookupOption OptionSet
options
    let traces :: IO [(Either Condition (Maybe String), 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 (Maybe String)
assertableP)) (forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way MemType
memtype)) ConcIO (Maybe String)
conc
    forall t.
IsTest t =>
OptionSet -> t -> (Progress -> IO ()) -> IO Result
run OptionSet
options (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 (forall a b.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval Predicate (Maybe String)
assertableP)) Progress -> IO ()
callback

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

assertableP :: Predicate (Maybe String)
assertableP :: Predicate (Maybe String)
assertableP = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper where
    shortName :: String -> Maybe MemType
shortName String
"SC"  = forall a. a -> Maybe a
Just MemType
SequentialConsistency
    shortName String
"TSO" = forall a. a -> Maybe a
Just MemType
TotalStoreOrder
    shortName String
"PSO" = forall a. a -> Maybe a
Just MemType
PartialStoreOrder
    shortName String
_ = forall a. Maybe a
Nothing
  optionName :: Tagged MemType String
optionName = forall {k} (s :: k) b. b -> Tagged s b
Tagged String
"memory-model"
  optionHelp :: Tagged MemType String
optionHelp = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper where
    shortName :: String -> Maybe Way
shortName String
"SYSTEMATICALLY" = forall a. a -> Maybe a
Just (Bounds -> Way
systematically Bounds
defaultBounds)
    shortName String
"RANDOMLY"       = forall a. a -> Maybe a
Just (forall g. RandomGen g => g -> Int -> Way
randomly (Int -> StdGen
mkStdGen Int
42) Int
100)
    shortName String
_ = forall a. Maybe a
Nothing
  optionName :: Tagged Way String
optionName = forall {k} (s :: k) b. b -> Tagged s b
Tagged String
"way"
  optionHelp :: Tagged Way String
optionHelp = 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 = forall a pty.
(Eq a, Show a) =>
Settings IO a -> String -> Program pty IO a -> TestTree
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.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 = forall a pty.
(Eq a, Show a) =>
Settings IO a -> String -> Program pty IO a -> TestTree
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.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 = 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", 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
  => 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 = forall b a pty.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> TestTree
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.
  -> 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 = forall b a pty.
Show b =>
Settings IO a
-> String -> ProPredicate a b -> Program pty IO a -> TestTree
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 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 =
  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 = forall b a pty.
Show b =>
Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
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.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 = forall b a pty.
Show b =>
Settings IO a
-> String
-> [(String, ProPredicate a b)]
-> Program pty IO a
-> TestTree
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.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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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 = 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 = 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 = 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 = forall a. Show a => Result a -> String
showErr forall a b. (a -> b) -> a -> b
$ [(Either Condition a, Trace)] -> Result b
p [(Either Condition a, Trace)]
traces
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (if 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 = 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 <- 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
    forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 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 -> 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) = forall t. IsTest t => String -> t -> TestTree
singleTest String
name forall a b. (a -> b) -> a -> b
$ forall p a.
Show p =>
IO [(Either Condition a, Trace)]
-> ([(Either Condition a, Trace)] -> Result p) -> ConcTest
ConcTest IO [(Either Condition a, Trace)]
traces (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 = 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 b
p)
  traces :: IO [(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

-- | 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 = forall t. IsTest t => String -> t -> TestTree
singleTest String
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
  | 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 (\(Either Condition a
r, Trace
t) -> String -> String
indent forall a b. (a -> b) -> a -> b
$ 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 a
r forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Trace -> String
Conc.showTrace Trace
t) 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

  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