-- TODO in some cases it may be useful to indent  messages
-- based on an invariant category above them

{-# LANGUAGE TupleSections,  ScopedTypeVariables, GeneralizedNewtypeDeriving #-}
module Test.QuickCheck.Property.Comb where
import Test.QuickCheck
import Control.Monad.Writer
import Control.Monad.Reader

--A Monad which collects related invariants on the input
type InvM i r = ReaderT i (Writer String) r
type Inv i = InvM i Bool

cause :: (Monad m) => ReaderT i m i
cause = ask

--A Monad which collects distinct invariants on the input
type Invariants i = ReaderT i (Writer [Inv i]) ()

doc :: String -> InvM r ()
doc = lift . tell

sat :: Inv i -> Invariants i
sat p = lift . tell $ (p:[])

satcomp :: forall i i'. (i' -> i) -> Invariants i -> Invariants i'
satcomp f = mapReaderT toWriter . withReaderT f where
  toWriter :: Writer [Inv i] () -> Writer [Inv i'] ()
  toWriter orig = mapWriter (((),) . map toPredicate . snd) orig
  toPredicate :: Inv i -> Inv i'
  toPredicate orig = withReaderT f orig

runInv :: (Show i) => i -> Inv i -> Property
runInv cause' rdr =
  let (effect, msg) = runWriter . (runReaderT rdr) $ cause' in
    printTestCase ("inv: " ++ if null msg then "unknown" else msg)
      . property $ effect

runInvariants :: forall i. (Show i) => i -> Invariants i -> Property
runInvariants cause' preds =
  conjoin . map (runInv cause') . execWriter . runReaderT preds $ cause'