speculate 0.4.12 → 0.4.14

raw patch · 11 files changed

+245/−36 lines, 11 filesdep ~express

Dependency ranges changed: express

Files

• .gitignore +1/−0
• Makefile +2/−1
• bench/lowtests.hs +26/−0
• bench/runtime-zero +30/−29
• changelog.md +12/−2
• mk/depend.mk +32/−0
• speculate.cabal +3/−3
• src/Test/Speculate/Reason.hs +25/−0
• stack.yaml +1/−1
• test/model/lowtests-s4.out +56/−0
• test/model/lowtests.out +57/−0

@@ -86,6 +86,7 @@ bench/representatives bench/representatives2 bench/arithficial+bench/lowtests bench/nord bench/unit bench/trilean

@@ -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

@@ -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)+                  ]+    }

@@ -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

@@ -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

@@ -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 \

@@ -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

@@ -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)

@@ -5,4 +5,4 @@  extra-deps: - leancheck-0.9.10-- express-0.2.0+- express-1.0.6

@@ -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++

@@ -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++