-- 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 , _i, xx, yy , _is, xxs, yys , 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.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 t -> error $ "(-:-): unhandled type " ++ t consEint = constant ":" ((:) -:> int) consEbool = constant ":" ((:) -:> bool) 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] zero :: Expr zero = expr (0 :: Int) one :: Expr one = expr (1 :: Int) llb :: Expr llb = expr ([] :: [Bool]) 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 = constant "/=" ((/=) :: Int -> Int -> Bool) :$ e1 :$ e2 infix 4 -/=- -- TODO: improve above after changing Speculate (-<=-) :: 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