-- |
-- Module      : Test.Extrapolate.IO
-- Copyright   : (c) 2017-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Extrapolate,
-- a library for generalization of counter-examples.
--
-- QuickCheck-like interface.
{-# 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)

-- | Use @`for`@ to configure the number of tests performed by @check@.
--
-- > > check `for` 10080 $ \xs -> sort (sort xs) == sort (xs :: [Int])
-- > +++ OK, passed 10080 tests.
--
-- Don't forget the dollar ('$')!
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

-- | Allows the user to customize instance information available when generalized.
--   (For advanced users.)
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

-- | Use @`withBackground`@ to provide additional functions to appear in side-conditions.
--
-- > check `withBackground` [value "isSpace" isSpace] $ \xs -> unwords (words xs) == xs
-- > *** Failed! Falsifiable (after 4 tests):
-- > " "
-- >
-- > Generalization:
-- > ' ':_
-- >
-- > Conditional Generalization:
-- > c:_  when  isSpace c
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]

-- | Use @`withConditionSize`@ to configure the maximum condition size allowed.
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

-- | Checks a property printing results on 'stdout'
--
-- > > check $ \xs -> sort (sort xs) == sort (xs::[Int])
-- > +++ OK, passed 360 tests.
-- >
-- > > check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])
-- > *** Failed! Falsifiable (after 4 tests):
-- > [] [0,0]
-- >
-- > Generalization:
-- > [] (x:x:_)
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

-- | Check a property
--   printing results on 'stdout' and
--   returning 'True' on success.
--
-- There is no option to silence this function:
-- for silence, you should use 'Test.LeanCheck.holds'.
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)

-- WARNING: expressions are unevaluable after this, just good for printing
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