diff --git a/extrapolate.cabal b/extrapolate.cabal --- a/extrapolate.cabal +++ b/extrapolate.cabal @@ -1,5 +1,5 @@ name: extrapolate -version: 0.2.0 +version: 0.2.1 synopsis: generalize counter-examples of test properties description: Extrapolate is a tool able to provide generalized counter-examples of test @@ -31,7 +31,7 @@ source-repository this type: git location: https://github.com/rudymatela/speculate - tag: v0.2.0 + tag: v0.2.1 library exposed-modules: Test.Extrapolate @@ -53,6 +53,7 @@ test-suite test type: exitcode-stdio-1.0 main-is: test-extrapolate.hs + other-modules: Test hs-source-dirs: src, tests build-depends: base >= 4 && < 5, leancheck, speculate, template-haskell default-language: Haskell2010 @@ -60,6 +61,7 @@ test-suite derive type: exitcode-stdio-1.0 main-is: test-derive.hs + other-modules: Test hs-source-dirs: src, tests build-depends: base >= 4 && < 5, leancheck, speculate, template-haskell default-language: Haskell2010 diff --git a/src/Test/Extrapolate/Core.hs b/src/Test/Extrapolate/Core.hs --- a/src/Test/Extrapolate/Core.hs +++ b/src/Test/Extrapolate/Core.hs @@ -28,6 +28,8 @@ , maxTests , extraInstances , maxConditionSize + , hasEq + , (*==*) , counterExampleGen , counterExampleGens @@ -66,7 +68,7 @@ , checkResultFor ) import Test.Extrapolate.Exprs (fold, unfold) -import Data.Maybe (listToMaybe, fromJust, isJust) +import Data.Maybe (listToMaybe, fromJust, fromMaybe, isJust, listToMaybe, catMaybes) import Data.Either (isRight) import Data.List (insert) import Data.Functor ((<$>)) -- for GHC <= 7.8 @@ -185,8 +187,13 @@ expr (xs@[]) = showConstant ([] -: xs) expr (xs@(y:ys)) = constant ":" ((:) ->>: xs) :$ expr y :$ expr ys background xs = [ constant "length" (length -:> xs) + , constant "any" (any ->:> xs) + , constant "all" (all ->:> xs) , constant "filter" (filter ->:> xs) ] + ++ [ constant "elem" (elemBy (*==*) ->:> xs) | hasEq (head xs) ] instances xs = this xs $ instances (head xs) +-- TODO: add (==) and (/=) when list element type has (==) and (/=) +-- TODO: add (<=) and (<) when list element type has (<=) and (<) instance Generalizable Ordering where name o = "o" @@ -450,3 +457,20 @@ isVar :: Expr -> Bool isVar (Var _ _) = True isVar _ = False + +hasEq :: Generalizable a => a -> Bool +hasEq x = isJust $ "==" `fromBackgroundOf` x -: mayb (x >- x >- bool) + +(*==*) :: Generalizable a => a -> a -> Bool +x *==* y = x == y + where + (==) = fromMaybe (error "(*==*): no (==) operator in background") + $ "==" `fromBackgroundOf` x +-- TODO: rename (*==*) to (-==-), use it in the Test module. + +fromBackgroundOf :: (Generalizable a, Typeable b) => String -> a -> Maybe b +fromBackgroundOf nm = listToMaybe + . catMaybes + . map evaluate + . filter (`isConstantNamed` nm) + . background diff --git a/src/Test/Extrapolate/Utils.hs b/src/Test/Extrapolate/Utils.hs --- a/src/Test/Extrapolate/Utils.hs +++ b/src/Test/Extrapolate/Utils.hs @@ -16,6 +16,7 @@ , foldr0 , fromLeft , fromRight + , elemBy ) where @@ -52,3 +53,6 @@ fromRight :: Either a b -> b fromRight (Right x) = x fromRight _ = error "fromRight: not a right" + +elemBy :: (a -> a -> Bool) -> a -> [a] -> Bool +elemBy (==) x = any (== x) diff --git a/tests/Test.hs b/tests/Test.hs new file mode 100644 --- /dev/null +++ b/tests/Test.hs @@ -0,0 +1,212 @@ +-- 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 + + , zero, one + + , false, true + + , nothing, nothingBool, just + + , comma + + -- * Properties and Tests + , generalizableOK + , 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 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]) + +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) + +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)) + + +-- Properties and tests -- + +generalizableOK :: (Eq a, Show a, Generalizable a) => Int -> a -> Bool +generalizableOK n x = holds n (exprOK -:> x) + && instancesOK x + +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 diff --git a/tests/test-extrapolate.hs b/tests/test-extrapolate.hs --- a/tests/test-extrapolate.hs +++ b/tests/test-extrapolate.hs @@ -104,9 +104,11 @@ ] listBackgroundOK :: Generalizable a => a -> Bool -listBackgroundOK x = backgroundOf [x] =$ sort $= backgroundListOf x +listBackgroundOK x = backgroundListOf x `subset` backgroundOf [x] where backgroundListOf x = [ constant "length" $ length -:> [x] + , constant "any" $ any ->:> [x] + , constant "all" $ all ->:> [x] , constant "filter" $ filter ->:> [x] ] +++ backgroundOf x