{-# 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
WithOption a -> b
check for :: (WithOption a -> b) -> Int -> a -> b
`for` Int
m = \a
p -> WithOption a -> b
check (WithOption a -> b) -> WithOption a -> b
forall a b. (a -> b) -> a -> b
$ a
p a -> Option -> WithOption a
forall a. a -> Option -> WithOption a
`With` Int -> Option
MaxTests Int
m
withInstances :: Testable a => (WithOption a -> b) -> Instances -> a -> b
WithOption a -> b
check withInstances :: (WithOption a -> b) -> Instances -> a -> b
`withInstances` Instances
is = \a
p -> WithOption a -> b
check (WithOption a -> b) -> WithOption a -> b
forall a b. (a -> b) -> a -> b
$ a
p a -> Option -> WithOption a
forall a. a -> Option -> WithOption a
`With` Instances -> Option
ExtraInstances Instances
is
withBackground :: Testable a => (WithOption a -> b) -> [Expr] -> a -> b
WithOption a -> b
check withBackground :: (WithOption a -> b) -> Instances -> a -> b
`withBackground` Instances
ufs = WithOption a -> b
check (WithOption a -> b) -> Instances -> a -> b
forall a b.
Testable a =>
(WithOption a -> b) -> Instances -> a -> b
`withInstances` [String -> Instances -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"background" Instances
ufs]
withConditionSize :: Testable a => (WithOption a -> b) -> Int -> a -> b
WithOption a -> b
check withConditionSize :: (WithOption a -> b) -> Int -> a -> b
`withConditionSize` Int
s = \a
p -> WithOption a -> b
check (WithOption a -> b) -> WithOption a -> b
forall a b. (a -> b) -> a -> b
$ a
p a -> Option -> WithOption a
forall a. a -> Option -> WithOption a
`With` Int -> Option
MaxConditionSize Int
s
check :: Testable a => a -> IO ()
check :: a -> IO ()
check = IO Bool -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Bool -> IO ()) -> (a -> IO Bool) -> a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IO Bool
forall a. Testable a => a -> IO Bool
checkResult
checkResult :: Testable a => a -> IO Bool
checkResult :: a -> IO Bool
checkResult a
p = do
(Result
r,Instances
ces) <- a -> IO (Result, Instances)
forall a. Testable a => a -> IO (Result, Instances)
resultIO a
p
String -> IO ()
putStr (String -> IO ()) -> (Result -> String) -> Result -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Instances -> Result -> String
forall a. Testable a => a -> Instances -> Result -> String
showResult a
p Instances
ces (Result -> IO ()) -> Result -> IO ()
forall a b. (a -> b) -> a -> b
$ Result
r
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> Bool
isOK Result
r)
where
isOK :: Result -> Bool
isOK (OK Int
_) = Bool
True
isOK Result
_ = Bool
False
data Result = OK Int
| Falsified Int Expr
| Exception Int Expr String
deriving (Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c== :: Result -> Result -> Bool
Eq, Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> Result -> ShowS
Show)
resultsIO :: Testable a => a -> IO [Result]
resultsIO :: a -> IO [Result]
resultsIO = (Int -> (Expr, Bool) -> IO Result)
-> [Int] -> [(Expr, Bool)] -> IO [Result]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> (Expr, Bool) -> IO Result
torio [Int
1..] ([(Expr, Bool)] -> IO [Result])
-> (a -> [(Expr, Bool)]) -> a -> IO [Result]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [(Expr, Bool)]
forall a. Testable a => a -> [(Expr, Bool)]
limitedResults
where
tor :: Int -> (Expr, Bool) -> Result
tor Int
i (Expr
_,Bool
True) = Int -> Result
OK Int
i
tor Int
i (Expr
as,Bool
False) = Int -> Expr -> Result
Falsified Int
i Expr
as
torio :: Int -> (Expr, Bool) -> IO Result
torio Int
i r :: (Expr, Bool)
r@(Expr
as,Bool
_) = Result -> IO Result
forall a. a -> IO a
E.evaluate (Int -> (Expr, Bool) -> Result
tor Int
i (Expr, Bool)
r)
IO Result -> (SomeException -> IO Result) -> IO Result
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` \SomeException
e -> let SomeException
_ = SomeException
e :: SomeException
in Result -> IO Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Expr -> String -> Result
Exception Int
i Expr
as (SomeException -> String
forall a. Show a => a -> String
show SomeException
e))
resultIO :: Testable a => a -> IO (Result, [Expr])
resultIO :: a -> IO (Result, Instances)
resultIO a
p = do
[Result]
rs <- a -> IO [Result]
forall a. Testable a => a -> IO [Result]
resultsIO a
p
(Result, Instances) -> IO (Result, Instances)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Result -> Maybe Result -> Result
forall a. a -> Maybe a -> a
fromMaybe ([Result] -> Result
forall a. [a] -> a
last [Result]
rs) (Maybe Result -> Result) -> Maybe Result -> Result
forall a b. (a -> b) -> a -> b
$ (Result -> Bool) -> [Result] -> Maybe Result
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Result -> Bool
isFailure [Result]
rs
, (Result -> Maybe Expr) -> [Result] -> Instances
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Result -> Maybe Expr
ce [Result]
rs )
where
isFailure :: Result -> Bool
isFailure (OK Int
_) = Bool
False
isFailure Result
_ = Bool
True
ce :: Result -> Maybe Expr
ce (OK Int
_) = Maybe Expr
forall a. Maybe a
Nothing
ce (Falsified Int
_ Expr
es) = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
es
ce (Exception Int
_ Expr
es String
_) = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
es
showResult :: Testable a => a -> [Expr] -> Result -> String
showResult :: a -> Instances -> Result -> String
showResult a
p Instances
ces (OK Int
n) = String
"+++ OK, passed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" tests"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\Char
_ -> Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< a -> Int
forall a. Testable a => a -> Int
testableMaxTests a
p) String
" (exhausted)" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".\n\n"
showResult a
p Instances
ces (Falsified Int
i Expr
ce) = String
"*** Failed! Falsifiable (after "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" tests):\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> Expr -> String
forall a. Testable a => a -> Expr -> String
showCEandGens a
p Expr
ce
showResult a
p Instances
ces (Exception Int
i Expr
ce String
e) = String
"*** Failed! Exception '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' (after "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" tests):\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> Expr -> String
forall a. Testable a => a -> Expr -> String
showCEandGens a
p Expr
ce
showCEandGens :: Testable a => a -> Expr -> String
showCEandGens :: a -> Expr -> String
showCEandGens a
p Expr
e = Expr -> String
showCE Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"Generalization:\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
showCE ((Expr -> [String]) -> Expr -> Expr
canonicalizeUsingHolesWith Expr -> [String]
names Expr
e)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
| Expr
e <- Expr -> Instances
gens Expr
e]
String -> ShowS
forall a. [a] -> [a] -> [a]
++ case Expr -> Instances
cgens Expr
e of
[] -> String
""
(Expr
e:Instances
_) -> String
"Conditional Generalization:\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
showCCE ((Expr -> [String]) -> Expr -> Expr
canonicalizeUsingHolesWith Expr -> [String]
names Expr
e) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"
where
names :: Expr -> [String]
names = a -> Expr -> [String]
forall a. Testable a => a -> Expr -> [String]
testableNames a
p
grounds :: Expr -> Instances
grounds = a -> Expr -> Instances
forall a. Testable a => a -> Expr -> Instances
testableGrounds a
p
gens :: Expr -> Instances
gens = (Expr -> Instances) -> Expr -> Instances
counterExampleGeneralizations Expr -> Instances
grounds
cgens :: Expr -> Instances
cgens = Int
-> [Instances]
-> (Expr -> Instances)
-> (Expr -> Expr -> Expr)
-> Expr
-> Instances
conditionalCounterExampleGeneralizations
(a -> Int
forall a. Testable a => a -> Int
testableMaxConditionSize a
p)
(a -> [Instances]
forall a. Testable a => a -> [Instances]
testableAtoms a
p)
(a -> Expr -> Instances
forall a. Testable a => a -> Expr -> Instances
testableGrounds a
p)
(a -> Expr -> Expr -> Expr
forall a. Testable a => a -> Expr -> Expr -> Expr
testableMkEquation a
p)
showCE :: Expr -> String
showCE :: Expr -> String
showCE = Instances -> String
s (Instances -> String) -> (Expr -> Instances) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instances -> Instances
forall a. [a] -> [a]
tail (Instances -> Instances)
-> (Expr -> Instances) -> Expr -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Instances
unfoldApp
where
s :: Instances -> String
s [Expr
e] = Int -> Expr -> String
showPrecExpr Int
0 Expr
e
s Instances
es = [String] -> String
unwords [Int -> Expr -> String
showPrecExpr Int
11 Expr
e | Expr
e <- Instances
es]
showCCE :: Expr -> String
showCCE :: Expr -> String
showCCE = (Expr, Expr) -> String
s ((Expr, Expr) -> String)
-> (Expr -> (Expr, Expr)) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> (Expr, Expr)
unand
where
s :: (Expr, Expr) -> String
s (Expr
e,Expr
c) = Expr -> String
showCE Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" when " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Expr -> String
showPrecExpr Int
0 (Expr -> Expr
prettify Expr
c)
prettify :: Expr -> Expr
prettify :: Expr -> Expr
prettify (((Value String
"<=" Dynamic
_) :$ Expr
e1) :$ Expr
e2) | Expr -> Int
size Expr
e1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Expr -> Int
size Expr
e2 = (((String -> Dynamic -> Expr
Value String
">=" Dynamic
forall a. HasCallStack => a
undefined) Expr -> Expr -> Expr
:$ Expr
e2) Expr -> Expr -> Expr
:$ Expr
e1)
prettify (((Value String
"<" Dynamic
_) :$ Expr
e1) :$ Expr
e2) | Expr -> Int
size Expr
e1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Expr -> Int
size Expr
e2 = (((String -> Dynamic -> Expr
Value String
">" Dynamic
forall a. HasCallStack => a
undefined) Expr -> Expr -> Expr
:$ Expr
e2) Expr -> Expr -> Expr
:$ Expr
e1)
prettify (Expr
e1 :$ Expr
e2) = Expr -> Expr
prettify Expr
e1 Expr -> Expr -> Expr
:$ Expr -> Expr
prettify Expr
e2
prettify Expr
e = Expr
e