{-# LANGUAGE CPP #-}
module Test.Extrapolate.IO
( check
, checkResult
, for
, withInstances
, withBackground
, withConditionSize
)
where
#if __GLASGOW_HASKELL__ <= 704
import Prelude hiding (catch)
#endif
import Test.Extrapolate.Core
import Data.Maybe (mapMaybe, fromMaybe)
import Data.List (find)
import Control.Monad
import Control.Exception as E (SomeException, catch, evaluate)
for :: Testable a => (WithOption a -> b) -> Int -> a -> b
check `for` m = \p -> check $ p `With` MaxTests m
withInstances :: Testable a => (WithOption a -> b) -> Instances -> a -> b
check `withInstances` is = \p -> check $ p `With` ExtraInstances is
withBackground :: Testable a => (WithOption a -> b) -> [Expr] -> a -> b
check `withBackground` ufs = check `withInstances` [value "background" ufs]
withConditionSize :: Testable a => (WithOption a -> b) -> Int -> a -> b
check `withConditionSize` s = \p -> check $ p `With` MaxConditionSize s
check :: Testable a => a -> IO ()
check = void . checkResult
checkResult :: Testable a => a -> IO Bool
checkResult p = do
(r,ces) <- resultIO p
putStr . showResult p ces $ r
return (isOK r)
where
isOK (OK _) = True
isOK _ = False
data Result = OK Int
| Falsified Int Expr
| Exception Int Expr String
deriving (Eq, Show)
resultsIO :: Testable a => a -> IO [Result]
resultsIO = zipWithM torio [1..] . limitedResults
where
tor i (_,True) = OK i
tor i (as,False) = Falsified i as
torio i r@(as,_) = E.evaluate (tor i r)
`catch` \e -> let _ = e :: SomeException
in return (Exception i as (show e))
resultIO :: Testable a => a -> IO (Result, [Expr])
resultIO p = do
rs <- resultsIO p
return ( fromMaybe (last rs) $ find isFailure rs
, mapMaybe ce rs )
where
isFailure (OK _) = False
isFailure _ = True
ce (OK _) = Nothing
ce (Falsified _ es) = Just es
ce (Exception _ es _) = Just es
showResult :: Testable a => a -> [Expr] -> Result -> String
showResult p ces (OK n) = "+++ OK, passed " ++ show n ++ " tests"
++ takeWhile (\_ -> n < testableMaxTests p) " (exhausted)" ++ ".\n\n"
showResult p ces (Falsified i ce) = "*** Failed! Falsifiable (after "
++ show i ++ " tests):\n" ++ showCEandGens p ce
showResult p ces (Exception i ce e) = "*** Failed! Exception '" ++ e ++ "' (after "
++ show i ++ " tests):\n" ++ showCEandGens p ce
showCEandGens :: Testable a => a -> Expr -> String
showCEandGens p e = showCE e ++ "\n\n"
++ concat [ "Generalization:\n"
++ showCE (canonicalizeUsingHolesWith names e)
++ "\n\n"
| e <- gens e]
++ case cgens e of
[] -> ""
(e:_) -> "Conditional Generalization:\n"
++ showCCE (canonicalizeUsingHolesWith names e) ++ "\n\n"
where
names = testableNames p
grounds = testableGrounds p
gens = counterExampleGeneralizations grounds
cgens = conditionalCounterExampleGeneralizations
(testableMaxConditionSize p)
(testableAtoms p)
(testableGrounds p)
(testableMkEquation p)
showCE :: Expr -> String
showCE = s . tail . unfoldApp
where
s [e] = showPrecExpr 0 e
s es = unwords [showPrecExpr 11 e | e <- es]
showCCE :: Expr -> String
showCCE = s . unand
where
s (e,c) = showCE e ++ " when " ++ showPrecExpr 0 (prettify c)
prettify :: Expr -> Expr
prettify (((Value "<=" _) :$ e1) :$ e2) | size e1 < size e2 = (((Value ">=" undefined) :$ e2) :$ e1)
prettify (((Value "<" _) :$ e1) :$ e2) | size e1 < size e2 = (((Value ">" undefined) :$ e2) :$ e1)
prettify (e1 :$ e2) = prettify e1 :$ prettify e2
prettify e = e