-- Copyright (c) 2017 Rudy Matela.
-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
module Test
( module Test.Extrapolate
, module Test.Extrapolate.Core
, module Test.LeanCheck.Utils.Operators
, reportTests
, getMaxTestsFromArgs
, mainTest
, printLines
, (-:-), ll, llb, llmi
, _i, xx, yy
, _is, xxs, yys
, _mi, mxx
, zero, one
, false, true
, elem'
, nothing, nothingBool, just
, comma
, (-==-)
, (-/=-)
, (-<-)
, (-<=-)
-- * Properties and Tests
, generalizableOK
, exprOK
, idExprEval, showOK
, instancesOK
, namesOK, sameNamesIn, namesIn
, tiersOK, sameTiersIn, tiersIn
, subset, bgSubset
, instancesSubset
)
where
import System.Exit (exitFailure)
import Data.List (elemIndices)
import System.Environment (getArgs)
import Test.Speculate.Expr (typ)
import Test.Speculate.Expr.Instance as I
import Data.Typeable (typeOf)
import Data.List (isPrefixOf, sort)
import Data.Maybe (fromMaybe)
import Test.Extrapolate
import Test.Extrapolate.Utils
import Test.Extrapolate.Core hiding (false, true)
import qualified Test.Extrapolate.Core as Core
import Test.LeanCheck.Utils.Operators
reportTests :: [Bool] -> IO ()
reportTests tests =
case elemIndices False tests of
[] -> putStrLn "Tests passed!"
is -> do putStrLn ("Failed tests:" ++ show is)
exitFailure
getMaxTestsFromArgs :: Int -> IO Int
getMaxTestsFromArgs n = do
as <- getArgs
return $ case as of
(s:_) -> read s
_ -> n
mainTest :: (Int -> [Bool]) -> Int -> IO ()
mainTest tests n' = do
n <- getMaxTestsFromArgs n'
reportTests (tests n)
printLines :: Show a => [a] -> IO ()
printLines = putStrLn . unlines . map show
(-:-) :: Expr -> Expr -> Expr
x -:- xs = consE :$ x :$ xs
where
consE = case show $ typ x of
"Int" -> consEint
"Bool" -> consEbool
"Maybe Int" -> consEmint
t -> error $ "(-:-): unhandled type " ++ t
consEint = constant ":" ((:) -:> int)
consEbool = constant ":" ((:) -:> bool)
consEmint = constant ":" ((:) -:> mayb int)
infixr 5 -:-
ll :: Expr
ll = expr ([] :: [Int])
_i, xx, yy :: Expr
_i = var "" int
xx = var "x" int
yy = var "y" int
_is, xxs, yys :: Expr
_is = var "" [int]
xxs = var "xs" [int]
yys = var "ys" [int]
_mi, mxx :: Expr
_mi = var "" (mayb int)
mxx = var "mx" (mayb int)
zero :: Expr
zero = expr (0 :: Int)
one :: Expr
one = expr (1 :: Int)
llb :: Expr
llb = expr ([] :: [Bool])
llmi :: Expr
llmi = expr ([] :: [Maybe Int])
false :: Expr
false = expr False
true :: Expr
true = expr True
nothing :: Expr
nothing = constant "Nothing" (Nothing :: Maybe Int)
nothingBool :: Expr
nothingBool = constant "Nothing" (Nothing :: Maybe Bool)
elem' :: Expr -> Expr -> Expr
elem' x xs = elemE :$ x :$ xs
where
elemE = constant "elem" (elem :: Int -> [Int] -> Bool)
just :: Expr -> Expr
just x = justE :$ x
where
justE = case show $ typ x of
"Int" -> justEint
"Bool" -> justEbool
t -> error $ "(-:-): unhandled type " ++ t
justEint = constant "Just" (Just -:> int)
justEbool = constant "Just" (Just -:> bool)
comma :: Expr -> Expr -> Expr
comma x y = commaE :$ x :$ y
where
commaE = case (show $ typ x, show $ typ y) of
("Int", "Int") -> commaEii
("Int", "Bool") -> commaEib
("Bool","Int") -> commaEbi
("Bool","Bool") -> commaEbb
(t,t') -> error $ "(-:-): unhandled types " ++ t ++ " " ++ t'
commaEii = constant "," ((,) ->>: (int,int))
commaEib = constant "," ((,) ->>: (int,bool))
commaEbi = constant "," ((,) ->>: (bool,int))
commaEbb = constant "," ((,) ->>: (bool,bool))
(-==-) :: Expr -> Expr -> Expr
e1 -==- e2 =
fromMaybe (error $ "(-==-): cannot equate " ++ show e1 ++ " and " ++ show e2)
(equation preludeInstances e1 e2)
infix 4 -==-
(-/=-) :: Expr -> Expr -> Expr
e1 -/=- e2 =
fromMaybe (error $ "(-/=-): cannot inequate " ++ show e1 ++ " and " ++ show e2)
(inequality preludeInstances e1 e2)
infix 4 -/=-
(-<=-) :: Expr -> Expr -> Expr
e1 -<=- e2 =
fromMaybe (error $ "(-<=-): cannot lessEq " ++ show e1 ++ " and " ++ show e2)
(comparisonLE preludeInstances e1 e2)
infix 4 -<=-
(-<-) :: Expr -> Expr -> Expr
e1 -<- e2 =
fromMaybe (error $ "(-<-): cannot less " ++ show e1 ++ " and " ++ show e2)
(comparisonLT preludeInstances e1 e2)
infix 4 -<-
-- Properties and tests --
generalizableOK :: (Eq a, Show a, Generalizable a) => Int -> a -> Bool
generalizableOK n x = holds n (exprOK -:> x)
&& instancesOK (und -: x)
where
und = error "generalizableOK: this should not get evaluated"
exprOK :: (Eq a, Show a, Generalizable a) => a -> Bool
exprOK = idExprEval &&& showOK
idExprEval :: (Eq a, Generalizable a) => a -> Bool
idExprEval x = eval (error "idExprEval: could not eval") (expr x) == x
showOK :: (Show a, Generalizable a) => a -> Bool
showOK x = show x == dropType (show (expr x))
where
dropType :: String -> String
dropType cs | " :: " `isPrefixOf` cs = ""
dropType "" = ""
dropType (c:cs) = c : dropType cs
instancesOK :: (Eq a, Generalizable a) => a -> Bool
instancesOK = namesOK &&& tiersOK
namesOK :: Generalizable a => a -> Bool
namesOK x = Core.name x == head (x `namesIn` x)
&& x `sameNamesIn` [x]
&& x `sameNamesIn` [[x]]
&& x `sameNamesIn` mayb x
&& x `sameNamesIn` (x,x)
&& x `sameNamesIn` (x,())
&& x `sameNamesIn` ((),x)
&& x `sameNamesIn` (x,(),())
&& x `sameNamesIn` ((),x,())
&& x `sameNamesIn` ((),(),x)
sameNamesIn :: (Generalizable a, Generalizable b) => a -> b -> Bool
x `sameNamesIn` c = x `namesIn` x
=| 12 |= x `namesIn` c
namesIn :: (Generalizable a, Generalizable b) => a -> b -> [String]
x `namesIn` c = I.names (instances c []) (typeOf x)
tiersOK :: (Eq a, Generalizable a) => a -> Bool
tiersOK x = x `sameTiersIn` x
&& x `sameTiersIn` [x]
&& x `sameTiersIn` [[x]]
&& x `sameTiersIn` (mayb x)
&& x `sameTiersIn` (x,x)
&& x `sameTiersIn` (x,())
&& x `sameTiersIn` ((),x)
&& x `sameTiersIn` (x,(),())
&& x `sameTiersIn` ((),x,())
&& x `sameTiersIn` ((),(),x)
sameTiersIn :: (Eq a, Generalizable a, Generalizable b) => a -> b -> Bool
x `sameTiersIn` cx = isListable (instances cx []) (typeOf x)
&& (tiers -: [[x]]) =| 6 |= tiersIn cx
tiersIn :: (Generalizable a, Generalizable b) => b -> [[a]]
tiersIn c = ret
where
ret = mapT (eval . error $ "tiersIn: the imposible happened")
$ tiersE (instances c []) (typeOf (head (head ret)))
subset :: Ord a => [a] -> [a] -> Bool
xs `subset` ys = sort xs `isSubsequenceOf` sort ys
bgSubset :: (Generalizable a, Generalizable b) => a -> b -> Bool
x `bgSubset` y = backgroundOf x `subset` backgroundOf y
instancesSubset :: (Eq a, Eq b, Generalizable a, Generalizable b) => a -> b -> Bool
x `instancesSubset` y = x `bgSubset` y
&& x `sameTiersIn` y
&& x `sameNamesIn` y
-- available on Data.List since GHC >= 8.0
isSubsequenceOf :: Eq a => [a] -> [a] -> Bool
isSubsequenceOf [] _ = True
isSubsequenceOf (_:_) [] = False
isSubsequenceOf (x:xs) (y:ys)
| x == y = xs `isSubsequenceOf` ys
| otherwise = (x:xs) `isSubsequenceOf` ys