module Test.Target
( target, targetResult, targetWith, targetResultWith
, targetTH, targetResultTH, targetWithTH, targetResultWithTH
, Result(..), Testable, Targetable(..)
, TargetOpts(..), defaultOpts
, Test(..)
, monomorphic
) where
import Control.Applicative
import Control.Monad
import Control.Monad.Catch
import Control.Monad.State
import qualified Language.Haskell.TH as TH
import System.Process (terminateProcess)
import Test.QuickCheck.All (monomorphic)
import Text.Printf (printf)
import Language.Fixpoint.Names
import Language.Fixpoint.Smt.Interface hiding (verbose)
import Test.Target.Monad
import Test.Target.Targetable (Targetable(..))
import Test.Target.Targetable.Function ()
import Test.Target.Testable
import Test.Target.Types
import Test.Target.Util
target :: Testable f
=> f
-> String
-> FilePath
-> IO ()
target f name path
= targetWith f name path defaultOpts
targetTH :: TH.Name -> FilePath -> TH.ExpQ
targetTH f m = [| target $(monomorphic f) $(TH.stringE $ show f) m |]
targetResult :: Testable f => f -> String -> FilePath -> IO Result
targetResult f name path
= targetResultWith f name path defaultOpts
targetResultTH :: TH.Name -> FilePath -> TH.ExpQ
targetResultTH f m = [| targetResult $(monomorphic f) $(TH.stringE $ show f) m |]
targetWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO ()
targetWith f name path opts
= do res <- targetResultWith f name path opts
case res of
Passed n -> printf "OK. Passed %d tests\n\n" n
Failed x -> printf "Found counter-example: %s\n\n" x
Errored x -> printf "Error! %s\n\n" x
targetWithTH :: TH.Name -> FilePath -> TargetOpts -> TH.ExpQ
targetWithTH f m opts = [| targetWith $(monomorphic f) $(TH.stringE $ show f) m opts |]
targetResultWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO Result
targetResultWith f name path opts
= do when (verbose opts) $
printf "Testing %s\n" name
sp <- getSpec (ghcOpts opts) path
ctx <- mkContext (solver opts)
do r <- runTarget opts (initState path sp ctx) $ do
ty <- safeFromJust "targetResultWith" . lookup (symbol name) <$> gets sigs
test f ty
_ <- cleanupContext ctx
return r
`onException` terminateProcess (pId ctx)
where
mkContext = if logging opts then flip makeContext (".target/" ++ name) else makeContextNoLog
targetResultWithTH :: TH.Name -> FilePath -> TargetOpts -> TH.ExpQ
targetResultWithTH f m opts = [| targetResultWith $(monomorphic f) $(TH.stringE $ show f) m opts |]
data Test = forall t. Testable t => T t