{-|
Module      : Assertion
Description : Assertions and related utilities for TLT
Copyright   : (c) John Maraist, 2022
License     : GPL3
Maintainer  : haskell-tlt@maraist.org
Stability   : experimental
Portability : POSIX

Assertion infrastructure for the @TLT@ testing system.  See `Test.TLT`
for more information.

-}

module Test.TLT.Assertion where

import Control.Monad.Trans.State.Strict
import Test.TLT.Results
import Test.TLT.Buffer
import Test.TLT.Class

-- * Specifying individual tests

-- |An assertion is a computation (typically in the monad wrapped by
-- `TLT`) which returns a list of zero of more reasons for the failure
-- of the assertion.  A successful computation returns an empty list:
-- no reasons for failure, hence success.
type Assertion m = m [TestFail]

-- |This assertion always fails with the given message.
assertFailed :: Monad m => String -> Assertion m
assertFailed :: forall (m :: * -> *). Monad m => String -> Assertion m
assertFailed String
msg = forall (m :: * -> *) a. Monad m => a -> m a
return [String -> TestFail
Asserted String
msg]

-- |This assertion always succeeds.
assertSuccess :: Monad m => Assertion m
assertSuccess :: forall (m :: * -> *). Monad m => Assertion m
assertSuccess = forall (m :: * -> *) a. Monad m => a -> m a
return []

infix 0 ~:, ~::, ~::-

-- |Label and perform a test of an `Assertion`.
--
-- ===== Example
--
-- > test :: Monad m => TLT m ()
-- > test = do
-- >   "2 is 2 as result" ~: 2 @== return 2    -- This test passes.
-- >   "2 not 3" ~: 2 @/=- 3                   -- This test fails.
(~:) :: MonadTLT m n => String -> Assertion m -> m ()
String
s ~: :: forall (m :: * -> *) (n :: * -> *).
MonadTLT m n =>
String -> Assertion m -> m ()
~: Assertion m
a = do
  (TLTopts
opts, TRBuf
oldState) <- forall (m :: * -> *) (n :: * -> *) a.
MonadTLT m n =>
TLT n a -> m a
liftTLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r. StateT (TLTopts, TRBuf) m r -> TLT m r
TLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. Monad m => StateT s m s
get
  [TestFail]
assessment <- Assertion m
a
  forall (m :: * -> *) (n :: * -> *) a.
MonadTLT m n =>
TLT n a -> m a
liftTLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r. StateT (TLTopts, TRBuf) m r -> TLT m r
TLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (TLTopts
opts, TRBuf -> TestResult -> TRBuf
addResult TRBuf
oldState forall a b. (a -> b) -> a -> b
$ String -> [TestFail] -> TestResult
Test String
s [TestFail]
assessment)

-- |Label and perform a test of a (pure) boolean value.
--
-- ===== Example
--
-- > test :: Monad m => TLT m ()
-- > test = do
-- >   "True passes" ~::- return True                 -- This test passes.
-- >   "2 is 2 as single Bool" ~::- return (2 == 2)   -- This test passes.
-- >   "2 is 3!?" ~::- myFn 4 "Hammer"                -- Passes if myFn (which
-- >                                                  -- must be monadic)
-- >                                                  -- returns True.
(~::-) :: MonadTLT m n => String -> Bool -> m ()
String
s ~::- :: forall (m :: * -> *) (n :: * -> *).
MonadTLT m n =>
String -> Bool -> m ()
~::- Bool
b = do
  (TLTopts
opts, TRBuf
oldState) <- forall (m :: * -> *) (n :: * -> *) a.
MonadTLT m n =>
TLT n a -> m a
liftTLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r. StateT (TLTopts, TRBuf) m r -> TLT m r
TLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. Monad m => StateT s m s
get
  forall (m :: * -> *) (n :: * -> *) a.
MonadTLT m n =>
TLT n a -> m a
liftTLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r. StateT (TLTopts, TRBuf) m r -> TLT m r
TLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (TLTopts
opts, TRBuf -> TestResult -> TRBuf
addResult TRBuf
oldState forall a b. (a -> b) -> a -> b
$ String -> [TestFail] -> TestResult
Test String
s forall a b. (a -> b) -> a -> b
$
        if Bool
b then [] else [String -> TestFail
Asserted forall a b. (a -> b) -> a -> b
$ String
"Expected True but got False"])

-- |Label and perform a test of a boolean value returned by a
-- computation in the wrapped monad @m@.
--
-- ===== Example
--
-- > test :: Monad m => TLT m ()
-- > test = do
-- >   "True passes" ~::- True               -- This test passes.
-- >   "2 is 2 as single Bool" ~::- 2 == 2   -- This test passes.
-- >   "2 is 3!?" ~::- 2 == 2                -- This test fails.
(~::) :: MonadTLT m n => String -> m Bool -> m ()
String
s ~:: :: forall (m :: * -> *) (n :: * -> *).
MonadTLT m n =>
String -> m Bool -> m ()
~:: m Bool
bM = do
  Bool
b <- m Bool
bM
  (TLTopts
opts, TRBuf
oldState) <- forall (m :: * -> *) (n :: * -> *) a.
MonadTLT m n =>
TLT n a -> m a
liftTLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r. StateT (TLTopts, TRBuf) m r -> TLT m r
TLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. Monad m => StateT s m s
get
  forall (m :: * -> *) (n :: * -> *) a.
MonadTLT m n =>
TLT n a -> m a
liftTLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) r. StateT (TLTopts, TRBuf) m r -> TLT m r
TLT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (TLTopts
opts, TRBuf -> TestResult -> TRBuf
addResult TRBuf
oldState forall a b. (a -> b) -> a -> b
$ String -> [TestFail] -> TestResult
Test String
s forall a b. (a -> b) -> a -> b
$
        if Bool
b then [] else [String -> TestFail
Asserted forall a b. (a -> b) -> a -> b
$ String
"Expected True but got False"])

-- |Transform a binary function on an expected and an actual value
-- (plus a binary generator of a failure message) into an `Assertion`
-- for a pure given actual value.
--
-- ===== Example
--
-- TLT's scalar-testing operators like @\@==-@ are defined with this
-- function:
--
-- > (@==-) :: (Monad m, Eq a, Show a) => a -> a -> Assertion m
-- > (@==-) = liftAssertion2Pure (==) $
-- >   \ exp actual -> "Expected " ++ show exp ++ " but got " ++ show actual
--
-- The `(==)` operator tests equality, and the result here allows the
-- assertion that a value should be exactly equal to a target.  The
-- second argument formats the detail reported when the assertion
-- fails.
liftAssertion2Pure ::
  (Monad m) => (a -> a -> Bool) -> (a -> a -> String) -> a -> a -> Assertion m
liftAssertion2Pure :: forall (m :: * -> *) a.
Monad m =>
(a -> a -> Bool) -> (a -> a -> String) -> a -> a -> Assertion m
liftAssertion2Pure a -> a -> Bool
tester a -> a -> String
explainer a
exp a
actual = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
  if (a -> a -> Bool
tester a
exp a
actual) then [] else [String -> TestFail
Asserted forall a b. (a -> b) -> a -> b
$ a -> a -> String
explainer a
exp a
actual]

-- |Given an `Assertion` for two pure values (expected and actual),
-- lift it to an `Assertion` expecting the actual value to be returned
-- from a computation.
--
-- ===== Examples
--
-- The TLT assertion `Test.TLT.(@==)` lifts `Test.TLT.(@==-)` (both
-- defined in `Test.TLT.Standard`) from expecting a pure actual result
-- to expecting a computation returning a value to test.
--
-- > (@==) :: (Monad m, Eq a, Show a) => a -> m a -> Assertion m
-- > (@==) = assertion2PtoM (@==-)
assertion2PtoM ::
  (Monad m) => (a -> a -> Assertion m) -> a -> m a -> Assertion m
assertion2PtoM :: forall (m :: * -> *) a.
Monad m =>
(a -> a -> Assertion m) -> a -> m a -> Assertion m
assertion2PtoM a -> a -> Assertion m
pa a
exp m a
actualM = do a
actual <- m a
actualM
                                   a -> a -> Assertion m
pa a
exp a
actual

-- |Transform a binary function on expected and actual values (plus
-- a generator of a failure message) into an `Assertion` where the
-- actual value is to be returned from a subcomputation.
liftAssertion2M ::
  (Monad m) => (a -> a -> Bool) -> (a -> a -> String) -> a -> m a -> Assertion m
liftAssertion2M :: forall (m :: * -> *) a.
Monad m =>
(a -> a -> Bool) -> (a -> a -> String) -> a -> m a -> Assertion m
liftAssertion2M a -> a -> Bool
tester a -> a -> String
explainer a
exp m a
actualM =
  let assertPure :: a -> Assertion m
assertPure = forall (m :: * -> *) a.
Monad m =>
(a -> a -> Bool) -> (a -> a -> String) -> a -> a -> Assertion m
liftAssertion2Pure a -> a -> Bool
tester a -> a -> String
explainer a
exp
  in do a
actual <- m a
actualM
        a -> Assertion m
assertPure a
actual

-- |Transform a unary function on a value (plus a generator of a
-- failure message) into a unary function returning an `Assertion` for
-- a pure given actual value.
--
-- ===== Example
--
-- The TLT assertion `Test.TLT.emptyP` (defined in
-- `Test.TLT.Standard`) is built from the `Traversable` predicate
-- `null`
--
-- > emptyP :: (Monad m, Traversable t) => t a -> Assertion m
-- > emptyP = liftAssertionPure null
-- >            (\ _ -> "Expected empty structure but got non-empty")

liftAssertionPure ::
  (Monad m) => (a -> Bool) -> (a -> String) -> a -> Assertion m
liftAssertionPure :: forall (m :: * -> *) a.
Monad m =>
(a -> Bool) -> (a -> String) -> a -> Assertion m
liftAssertionPure a -> Bool
tester a -> String
explainer a
actual = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
  if (a -> Bool
tester a
actual) then [] else [String -> TestFail
Asserted forall a b. (a -> b) -> a -> b
$ a -> String
explainer a
actual]

-- |Given an `Assertion` for a pure (actual) value, lift it to an
-- `Assertion` expecting the value to be returned from a computation.
--
-- ===== Example
--
-- The TLT assertion `Test.TLT.empty` (defined in `Test.TLT.Standard`)
-- on monadic computations returning lists is defined in terms of the
-- corresponging assertion on pure list-valued expressions.
--
-- > empty :: (Monad m, Traversable t) => m (t a) -> Assertion m
-- > empty = assertionPtoM emptyP
assertionPtoM :: (Monad m) => (a -> Assertion m) -> m a -> Assertion m
assertionPtoM :: forall (m :: * -> *) a.
Monad m =>
(a -> Assertion m) -> m a -> Assertion m
assertionPtoM a -> Assertion m
pa m a
actualM = do a
actual <- m a
actualM
                              a -> Assertion m
pa a
actual

-- |Transform a unary function on an actual value (plus a generator of
-- a failure message) into an `Assertion` where the value is to be
-- returned from a subcomputation.
liftAssertionM ::
  (Monad m) => (a -> Bool) -> (a -> String) -> m a -> Assertion m
liftAssertionM :: forall (m :: * -> *) a.
Monad m =>
(a -> Bool) -> (a -> String) -> m a -> Assertion m
liftAssertionM a -> Bool
tester a -> String
explainer m a
actualM =
  let assertPure :: a -> Assertion m
assertPure = forall (m :: * -> *) a.
Monad m =>
(a -> Bool) -> (a -> String) -> a -> Assertion m
liftAssertionPure a -> Bool
tester a -> String
explainer
  in do a
actual <- m a
actualM
        a -> Assertion m
assertPure a
actual