-- 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
, _b, pp, qq
, _mi, mxx
, zero, one
, false, true
, not'
, notE
, elem', length'
, elemE, lengthE
, nothing, nothingBool, just
, comma
, operatorE
, (-==-)
, (-/=-)
, (-<-)
, (-<=-)
-- * Properties and Tests
, generalizableOK
, exprOK
, idExprEval, showOK
, instancesOK
, namesOK, sameNamesIn, namesIn
, tiersOK, sameTiersIn, tiersIn
, bgEqOK, bgEqOrdOK
, 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.Speculate.Reason
import Test.Speculate.Reason.Order
import Test.Extrapolate
import Test.Extrapolate.Utils
import Test.Extrapolate.Core hiding (false, true, lengthE)
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)
_b, pp, qq :: Expr
_b = var "" bool
pp = var "p" bool
qq = var "q" bool
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
elemE :: Expr
elemE = constant "elem" (elem :: Int -> [Int] -> Bool)
length' :: Expr -> Expr
length' xs = lengthE :$ xs
lengthE = constant "length" (length :: [Int] -> Int)
not' :: Expr -> Expr
not' p = notE :$ p
notE :: Expr
notE = constant "not" not
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 = plusE :$ e1 :$ e2
infixl 6 -+-
plusE :: Expr
plusE = constant "+" ((+) :: Int -> Int -> Int)
operatorE :: Expr -> Expr
operatorE ((opE :$ _) :$ _) = opE
(-==-) :: 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)
bgEqOK :: (Eq a, Generalizable a) => a -> a -> Bool
bgEqOK = (*==*) ==== (==)
&&&& (*/=*) ==== (/=)
bgEqOrdOK :: (Eq a, Ord a, Generalizable a) => a -> a -> Bool
bgEqOrdOK = bgEqOK &&&& (*<=*) ==== (<=)
&&&& (*<*) ==== (<)
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
-- Quick and Dirty!
instance Show Thy where
show Thy { rules = rs
, equations = eqs
, canReduceTo = (->-)
, closureLimit = cl
, keepE = keep
}
= "Thy { rules = "
++ drop 14 (indent 14 . listLines $ map showEquation rs)
++ " , equations = "
++ drop 18 (indent 18 . listLines $ map showEquation eqs)
++ " , canReduceTo = " ++ showCanReduceTo (->-) ++ "\n"
++ " , closureLimit = " ++ show cl ++ "\n"
++ " , keepE = " ++ showKeepE keep ++ "\n"
++ " }"
where
showEquation (e1,e2) = showExpr e1 ++ " == " ++ showExpr e2
listLines [] = "[]"
listLines ss = '[':(tail . unlines $ map (", " ++) ss) ++ "]"
showCanReduceTo (->-) = "(??)"
showKeepE keep = "\\e -> ??"
indent :: Int -> String -> String
indent n = unlines . map (replicate n ' ' ++) . lines