diff --git a/.gitignore b/.gitignore --- a/.gitignore +++ b/.gitignore @@ -86,6 +86,7 @@ bench/representatives bench/representatives2 bench/arithficial +bench/lowtests bench/nord bench/unit bench/trilean diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -50,6 +50,7 @@ eg/tuples \ eg/speculate-reason \ bench/arithficial \ + bench/lowtests \ bench/nord \ bench/trilean \ bench/unit @@ -69,7 +70,7 @@ eg/arith \ eg/bool \ eg/list -LIST_ALL_HSS = find src test eg bench/*.hs -name \*.hs | grep -vE 'eg/(regexes|pretty-compact|algebraic-graphs)' +LIST_ALL_HSS = find src test eg bench/*.hs mk -name \*.hs | grep -vE 'eg/(regexes|pretty-compact|algebraic-graphs)' LIST_LIB_HSS = find src -name \*.hs LIB_DEPS = base template-haskell $(INSTALL_DEPS) INSTALL_DEPS = leancheck express cmdargs containers diff --git a/bench/lowtests.hs b/bench/lowtests.hs new file mode 100644 --- /dev/null +++ b/bench/lowtests.hs @@ -0,0 +1,26 @@ +import Test.Speculate +import Data.List (sort) + +-- needed for GHC <= 7.8, exported by Data.List on GHC >= 7.10. +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 + +main :: IO () +main = do + speculate args + { constants = [ constant "sort" (sort :: [Int] -> [Int]) + , constant "`isSubsequenceOf`" (isSubsequenceOf :: [Int] -> [Int] -> Bool) + ] + } + + -- a low number of tests may produce incorrect equations + speculate args + { maxTests = 60 + , constants = [ constant "sort" (sort :: [Int] -> [Int]) + , constant "`isSubsequenceOf`" (isSubsequenceOf :: [Int] -> [Int] -> Bool) + ] + } diff --git a/bench/runtime-zero b/bench/runtime-zero --- a/bench/runtime-zero +++ b/bench/runtime-zero @@ -1,35 +1,36 @@ GHC 8.10.4 -express-0.1.5 -leancheck-0.9.4 +express-1.0.6 +leancheck-0.9.10 arith 0.233 -arith-c 0.593 -arithficial 0.636 -arith-negate-abs 1.776 -binarytree 1.666 -binarytree0 0.506 -bool 1.973 -bool-c 1.776 -colour 2.006 -digraphs 1.513 -fun 1.086 -insertsort 7.743 -insertsort0 0.913 -length 0.480 -list 2.593 -list-c 1.660 -minus 0.516 +arith-c 0.570 +arithficial 0.606 +arith-negate-abs 1.656 +binarytree 1.630 +binarytree0 0.513 +bool 2.043 +bool-c 1.806 +colour 2.003 +digraphs 1.486 +fun 1.100 +insertsort 7.676 +insertsort0 0.896 +length 0.463 +list 2.530 +list-c 1.580 +lowtests 0.436 +minus 0.513 minus-c 0.880 -monad 0.570 +monad 0.566 nord 0.010 -oddeven 6.593 -plus-abs 3.663 -pretty 9.030 -ratio 8.336 -sets 7.230 -speculate-reason 2.950 -string 0.860 -tauts 4.070 +oddeven 6.506 +plus-abs 3.510 +pretty 8.743 +ratio 8.030 +sets 7.193 +speculate-reason 2.770 +string 0.850 +tauts 3.980 trilean 0.010 -tuples 1.233 +tuples 1.210 unit 0.010 -zip 2.323 +zip 2.283 diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,8 +1,18 @@ Changelog for Speculate ======================= -upcoming --------- + +v0.4.14 +------- + +* `Test.Speculate.Reason`: add `doubleCheck`; +* add `lowtests` benchmark; +* bump [express] requirement to v1.0.0; +* fix parallel compilation when using the Makefile. + + +v0.4.12 +------- * bump [express] requirement to v0.2.0 * add this changelog diff --git a/mk/depend.mk b/mk/depend.mk --- a/mk/depend.mk +++ b/mk/depend.mk @@ -946,6 +946,38 @@ src/Test/Speculate/CondReason.hs \ src/Test/Speculate/Args.hs \ eg/zip.hs +mk/Toplibs.o: \ + test/Test.hs \ + test/Test/ListableExpr.hs \ + src/Test/Speculate/Utils/Tuple.hs \ + src/Test/Speculate/Utils/Timeout.hs \ + src/Test/Speculate/Utils/Tiers.hs \ + src/Test/Speculate/Utils/String.hs \ + src/Test/Speculate/Utils/PrettyPrint.hs \ + src/Test/Speculate/Utils.hs \ + src/Test/Speculate/Utils/Ord.hs \ + src/Test/Speculate/Utils/Misc.hs \ + src/Test/Speculate/Utils/Memoize.hs \ + src/Test/Speculate/Utils/List.hs \ + src/Test/Speculate/Utils/Digraph.hs \ + src/Test/Speculate/Utils/Colour.hs \ + src/Test/Speculate/Utils/Class.hs \ + src/Test/Speculate/SemiReason.hs \ + src/Test/Speculate/Sanity.hs \ + src/Test/Speculate/Report.hs \ + src/Test/Speculate/Reason.hs \ + src/Test/Speculate/Reason/Order.hs \ + src/Test/Speculate/Pretty.hs \ + src/Test/Speculate.hs \ + src/Test/Speculate/Expr.hs \ + src/Test/Speculate/Expr/Instance.hs \ + src/Test/Speculate/Expr/Ground.hs \ + src/Test/Speculate/Expr/Equate.hs \ + src/Test/Speculate/Expr/Core.hs \ + src/Test/Speculate/Engine.hs \ + src/Test/Speculate/CondReason.hs \ + src/Test/Speculate/Args.hs \ + mk/Toplibs.hs src/Test/Speculate/Args.o: \ src/Test/Speculate/Utils/Tuple.hs \ src/Test/Speculate/Utils/Timeout.hs \ diff --git a/speculate.cabal b/speculate.cabal --- a/speculate.cabal +++ b/speculate.cabal @@ -1,5 +1,5 @@ name: speculate -version: 0.4.12 +version: 0.4.14 synopsis: discovery of properties about Haskell functions description: Speculate automatically discovers laws about Haskell functions. @@ -87,7 +87,7 @@ source-repository this type: git location: https://github.com/rudymatela/speculate - tag: v0.4.12 + tag: v0.4.14 library @@ -124,7 +124,7 @@ , Test.Speculate.Utils.Tuple build-depends: base >= 4 && < 5 , leancheck >= 0.9.6 - , express >= 0.2.0 + , express >= 1.0.0 , cmdargs , containers hs-source-dirs: src diff --git a/src/Test/Speculate/Reason.hs b/src/Test/Speculate/Reason.hs --- a/src/Test/Speculate/Reason.hs +++ b/src/Test/Speculate/Reason.hs @@ -47,6 +47,7 @@ , finalize , initialize , defaultKeep + , doubleCheck , reductions1 @@ -78,6 +79,7 @@ , compareE :: Expr -> Expr -> Ordering -- ^ total order used to "sort" equations , closureLimit :: Int , keepE :: Expr -> Bool + , invalid :: [Equation] -- ^ reserved for rules and equations that were later found to be invalid through testing } compareEqn :: Thy -> Equation -> Equation -> Ordering @@ -137,6 +139,7 @@ , compareE = compare , closureLimit = 0 , keepE = const True + , invalid = [] } ruleFilter :: Thy -> [Rule] -> [Rule] @@ -440,6 +443,28 @@ -- you 'complete', redundant equations might pop-up again. finalize :: Thy -> Thy finalize = discardRedundantEquations + +-- | Double-checks a resulting theory moving untrue rules and equations to the +-- invalid list. +-- +-- As a side-effect of using testing to conjecturing equations, +-- we may get smaller equations that are obviously incorrect +-- when we consider a bigger (harder-to-test) equation that is incorrect. +-- +-- For example, given an incorrect large equation, it may follow that +-- False=True. +-- +-- This function can be used to double-check the generated theory. +-- If any equation or rule is discarded, that means the number of tests +-- should probably be increased. +doubleCheck :: (Expr -> Expr -> Bool) -> Thy -> Thy +doubleCheck (===) thy = thy + { rules = filter correct (rules thy) + , equations = filter correct (equations thy) + , invalid = filter (not . correct) (rules thy ++ equations thy) + } + where + correct = uncurry (===) theorize :: [Equation] -> Thy theorize = theorizeBy (canReduceTo emptyThy) diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -5,4 +5,4 @@ extra-deps: - leancheck-0.9.10 -- express-0.2.0 +- express-1.0.6 diff --git a/test/model/lowtests-s4.out b/test/model/lowtests-s4.out new file mode 100644 --- /dev/null +++ b/test/model/lowtests-s4.out @@ -0,0 +1,56 @@ +max expr size = 4 + |- on ineqs = 3 + |- on conds = 3 +max #-tests = 500 +min #-tests = 25 (to consider p ==> q true) +max #-vars = 2 (for inequational and conditional laws) + +_ :: Bool +_ :: Int +_ :: [Int] +sort :: [Int] -> [Int] +isSubsequenceOf :: [Int] -> [Int] -> Bool +True :: Bool +False :: Bool +(==) :: Bool -> Bool -> Bool +(==) :: Int -> Int -> Bool +(==) :: [Int] -> [Int] -> Bool + + xs `isSubsequenceOf` xs == True +sort xs `isSubsequenceOf` xs == xs `isSubsequenceOf` sort xs + (xs == sort xs) == xs `isSubsequenceOf` sort xs + sort (sort xs) == sort xs + +xs == ys ==> xs `isSubsequenceOf` ys + sort xs <= xs + + +max expr size = 4 + |- on ineqs = 3 + |- on conds = 3 +max #-tests = 60 +min #-tests = 3 (to consider p ==> q true) +max #-vars = 2 (for inequational and conditional laws) + +_ :: Bool +_ :: Int +_ :: [Int] +sort :: [Int] -> [Int] +isSubsequenceOf :: [Int] -> [Int] -> Bool +True :: Bool +False :: Bool +(==) :: Bool -> Bool -> Bool +(==) :: Int -> Int -> Bool +(==) :: [Int] -> [Int] -> Bool + + xs `isSubsequenceOf` xs == True +xs `isSubsequenceOf` sort xs == True + (xs == sort xs) == True +sort xs `isSubsequenceOf` ys == xs `isSubsequenceOf` sort ys + (sort xs == ys) == (xs == sort ys) + sort (sort xs) == sort xs + +xs == ys ==> xs `isSubsequenceOf` ys + sort xs <= xs + + diff --git a/test/model/lowtests.out b/test/model/lowtests.out new file mode 100644 --- /dev/null +++ b/test/model/lowtests.out @@ -0,0 +1,57 @@ +max expr size = 5 + |- on ineqs = 4 + |- on conds = 4 +max #-tests = 500 +min #-tests = 25 (to consider p ==> q true) +max #-vars = 2 (for inequational and conditional laws) + +_ :: Bool +_ :: Int +_ :: [Int] +sort :: [Int] -> [Int] +isSubsequenceOf :: [Int] -> [Int] -> Bool +True :: Bool +False :: Bool +(==) :: Bool -> Bool -> Bool +(==) :: Int -> Int -> Bool +(==) :: [Int] -> [Int] -> Bool + + xs `isSubsequenceOf` xs == True +sort xs `isSubsequenceOf` xs == xs `isSubsequenceOf` sort xs + (xs == sort xs) == xs `isSubsequenceOf` sort xs + sort (sort xs) == sort xs + + xs == ys ==> xs `isSubsequenceOf` ys +xs `isSubsequenceOf` sort ys ==> xs `isSubsequenceOf` sort xs + sort xs <= xs + + +max expr size = 5 + |- on ineqs = 4 + |- on conds = 4 +max #-tests = 60 +min #-tests = 3 (to consider p ==> q true) +max #-vars = 2 (for inequational and conditional laws) + +_ :: Bool +_ :: Int +_ :: [Int] +sort :: [Int] -> [Int] +isSubsequenceOf :: [Int] -> [Int] -> Bool +True :: Bool +False :: Bool +(==) :: Bool -> Bool -> Bool +(==) :: Int -> Int -> Bool +(==) :: [Int] -> [Int] -> Bool + + xs `isSubsequenceOf` xs == True +xs `isSubsequenceOf` sort xs == True + (xs == sort xs) == True +sort xs `isSubsequenceOf` ys == xs `isSubsequenceOf` sort ys + (sort xs == ys) == (xs == sort ys) + sort (sort xs) == sort xs + +xs == ys ==> xs `isSubsequenceOf` ys + sort xs <= xs + +