{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
module Control.Eff.Satisfy where

import Control.Eff
import Control.Eff.Lift
import Control.Eff.Choose
import Control.Monad
import Data.Maybe
import Data.Maybe.HT
import Data.Typeable
import Test.QuickCheck (Testable, quickCheckWithResult, stdArgs, Property, property, Result)
import Test.QuickCheck.Test (isSuccess, chatty)
import Control.Monad.IO.Class (MonadIO, liftIO)

data Satisfy b v = Satisfy (b -> Property) v deriving (Typeable)
instance Functor (Satisfy b) where
    fmap f (Satisfy p k) = Satisfy p (f k)

satisfy :: (Typeable b, Testable prop, Member (Satisfy b) r) => (b -> prop) -> Eff r ()
satisfy w = send $ \f -> inj $ Satisfy (property . w) $ f ()

silentCheckResult :: Testable prop => prop -> IO Result
silentCheckResult = quickCheckWithResult $ stdArgs { chatty = False }

runSatisfy' :: Typeable b => Eff (Satisfy b :> r) b -> Eff r (IO (Maybe b))
runSatisfy' = loop . admin where
    loop :: Typeable b => VE (Satisfy b :> r) b -> Eff r (IO (Maybe b))
    loop (Val x) = return $ return $ Just x
    loop (E u) = handleRelay u loop handle
    handle :: Typeable b => Satisfy b (VE (Satisfy b :> r) b) -> Eff r (IO (Maybe b))
    handle (Satisfy p k) = do
        (v :: IO (Maybe a)) <- loop k
        return $ do
            (w :: Maybe a) <- v
            case w of
                Just z -> do
                    result <- silentCheckResult $ p z
                    return $ isSuccess result `toMaybe` z
                Nothing -> return Nothing

runSatisfy :: (Typeable b, MonadIO m, Typeable1 m, SetMember Lift (Lift m) r) => Eff (Satisfy b :> r) b -> Eff r (Maybe b)
runSatisfy = lift . liftIO <=< runSatisfy'

runFilter :: (Typeable b, Member Choose r, MonadIO m, Typeable1 m, SetMember Lift (Lift m) r) => Eff (Satisfy b :> r) b -> Eff r b
runFilter = (choose . maybeToList) <=< runSatisfy
