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 Text.Printf (printf)
import Language.Fixpoint.Names
import Language.Fixpoint.SmtLib2 hiding (verbose)
import Test.Target.Monad
import Test.Target.Targetable (Targetable(..))
import Test.Target.Targetable.Function ()
import Test.Target.Testable
import Test.Target.TH
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)
runTarget opts (initState path sp ctx) (do
ty <- safeFromJust "targetResultWith" . lookup (symbol name) <$> gets sigs
test f ty)
`finally` killContext ctx
where
mkContext = if logging opts then flip makeContext (".target/" ++ name) else makeContextNoLog
killContext ctx = terminateProcess (pId ctx) >> cleanupContext ctx
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