-- TODO in some cases it may be useful to indent messages
-- based on a documented "context" above them
{-# LANGUAGE TupleSections, ScopedTypeVariables, GeneralizedNewtypeDeriving #-}
module Test.QuickCheck.Property.Comb (
cause, Inv, Invariants, doc, sat, satcomp, runInv, runInvariants
) where
import Test.QuickCheck
import Control.Monad.Writer
import Control.Monad.Reader
-- A Monad which collects related invariants on the input
type InvM c r = ReaderT c (Writer String) r
type Inv c = InvM c Bool
cause :: (Monad m) => ReaderT c m c
cause = ask
-- A Monad which collects invariants on the input
type Invariants c = ReaderT c (Writer [Inv c]) ()
doc :: String -> InvM r ()
doc = lift . tell
sat :: Inv c -> Invariants c
sat p = lift . tell $ [p]
satcomp :: forall c c'. (c' -> c) -> Invariants c -> Invariants c'
satcomp f = mapReaderT toWriter . withReaderT f where
toWriter :: Writer [Inv c] () -> Writer [Inv c'] ()
toWriter = mapWriter (((),) . map toPredicate . snd)
toPredicate :: Inv c -> Inv c'
toPredicate = withReaderT f
runInv :: (Show c) => c -> Inv c -> Property
runInv checked rdr =
let (effect, msg) = runWriter . runReaderT rdr $ checked in
printTestCase ("invariant: " ++ if null msg then "unknown" else msg)
. property $ effect
runInvariants :: (Show c) => c -> Invariants c -> Property
runInvariants checked preds =
conjoin . map (runInv checked) . execWriter . runReaderT preds $ checked