extrapolate 0.2.1 → 0.2.2

raw patch · 11 files changed

+277/−113 lines, 11 filesdep +extrapolatedep ~leancheckdep ~speculatePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: extrapolate

Dependency ranges changed: leancheck, speculate

API changes (from Hackage documentation)

Files

• README.md +17/−0
• TODO.md +0/−41
• extrapolate.cabal +18/−10
• src/Test/Extrapolate.hs +0/−6
• src/Test/Extrapolate/Basic.hs +59/−0
• src/Test/Extrapolate/Core.hs +44/−21
• src/Test/Extrapolate/TypeBinding.hs +1/−27
• src/Test/Extrapolate/Utils.hs +5/−1
• tests/Test.hs +53/−1
• tests/test-extrapolate.hs +62/−6
• tests/test-utils.hs +18/−0

@@ -3,6 +3,8 @@  [![Extrapolate Build Status][build-status]][build-log] [![Extrapolate on Hackage][hackage-version]][extrapolate-on-hackage]+[![Extrapolate on Stackage LTS][stackage-lts-badge]][extrapolate-on-stackage-lts]+[![Extrapolate on Stackage Nightly][stackage-nightly-badge]][extrapolate-on-stackage-nightly]  Extrapolate is a [property-based testing] library for [Haskell] capable of reporting generalized counter-examples.@@ -118,6 +120,12 @@ For type signatures, other options and uses, see [Extrapolate's API documentation]. +There are two other tools for [Haskell] capable of producing generalized+counter-examples: [SmartCheck] and [Lazy SmallCheck 2012].++Extrapolate was accepted for presentation at [IFL 2017], a link to a+pre-symposium proceedings draft paper will be listed here soon.+ [extrapolate-on-hackage]:          https://hackage.haskell.org/package/extrapolate [Extrapolate from Hackage]:        https://hackage.haskell.org/package/extrapolate [Extrapolate's API documentation]: https://hackage.haskell.org/package/extrapolate/docs/Test-Extrapolate.html@@ -132,6 +140,15 @@ [cabal]:                           https://www.haskell.org/cabal/ [property-based testing]:          https://github.com/rudymatela/leancheck/blob/master/doc/tutorial.md +[IFL 2017]:             http://iflconference.org/+[SmartCheck]:           https://github.com/leepike/SmartCheck+[Lazy SmallCheck 2012]: https://github.com/UoYCS-plasma/lazysmallcheck2012+ [build-status]:    https://travis-ci.org/rudymatela/extrapolate.svg?branch=master [build-log]:       https://travis-ci.org/rudymatela/extrapolate [hackage-version]: https://img.shields.io/hackage/v/extrapolate.svg+[stackage-lts-badge]:            http://stackage.org/package/extrapolate/badge/lts+[stackage-nightly-badge]:        http://stackage.org/package/extrapolate/badge/nightly+[extrapolate-on-stackage]:         http://stackage.org/package/extrapolate+[extrapolate-on-stackage-lts]:     http://stackage.org/lts/package/extrapolate+[extrapolate-on-stackage-nightly]: http://stackage.org/nightly/package/extrapolate

@@ -4,37 +4,9 @@ A non-exhaustive list of things TO DO for Extrapolate.  -cleanup----------* `renames1`:-  rename show functions:-	- move `showCE` to `Core`;-	- add and use `Core.showCCE`;-	- rename `IO.showCEC` to `IO.showCEandGens`;--* `renames2`:-  rename counterexamples:-	- rename `counterExamples*` to `counterExamples*E`;-	- add `counterExamples* :: ... String ...`;--* `cleanup`:-  cleanup and remove unused functions, like `showCEG`;-  thighten exports, removing uneeded functions (`backgroundWith`).-- examples -------- -* `add-redblack-eg`:-  add the redblacktree example from Small/SmartCheck/Okasaki.-  see `ideal-generalization`.-  Also described on: http://matt.might.net/articles/quick-quickcheck/--  It has been added, but cannot generalize the counter-examples found:  during-  generalization, the very exceptions that cause the error, make the-  generalization fail.  Somehow catch those errors on generalization.- * `ideal-generalizations`:   Add examples of ideal generalizations as described in past paper by human   experts.  The counter example is `blah` because the property fails for every@@ -79,14 +51,6 @@    the above is for the last property of the list example -* `add-derive-tests`:-  add tests of derivation;--* `show-and-expr-display`:-  display counterExamples both as Show and Expr, I don't know how easy is to-  use show since counterExamples are represented as Exprs, I don't think I can-  eval because I am not bound in a type context.- * `renaming`:   possibly print          `(Div (C 0) (Add (C x) (C (negate x))))`   which is equivalent to  `(Div (C 0) (Add (C x) (C y))) when y == negate x`@@ -134,11 +98,6 @@ * `single-then-multi`:   only do vassignments *after* finding a failing single variable instance.   I'll have to re-test, but the time I save may pay off.--* `no-listable-tuples`:-  there is no need to include listable tuples in the instances list (or at-  least no need to use it).  Instead of having `xy` we would get `(x,y)`.-  However, maybe it is fine as it is.  won't fix ---------

@@ -1,11 +1,11 @@ name:                extrapolate-version:             0.2.1+version:             0.2.2 synopsis:            generalize counter-examples of test properties description:   Extrapolate is a tool able to provide generalized counter-examples of test   properties where irrelevant sub-expressions are replaces with variables.   .-  For the incorrect property @\xs -> nub xs == (xs::[Int])@:+  For the incorrect property @\\xs -> nub xs == (xs::[Int])@:   .   * @[0,0]@ is a counter-example;   .@@ -31,7 +31,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/speculate-  tag:             v0.2.1+  tag:             v0.2.2  library   exposed-modules: Test.Extrapolate@@ -41,12 +41,12 @@                  , Test.Extrapolate.Exprs                  , Test.Extrapolate.IO                  , Test.Extrapolate.TypeBinding-  other-modules:   Test.Extrapolate.Utils+                 , Test.Extrapolate.Utils   other-extensions:    TemplateHaskell, CPP   build-depends: base >= 4 && < 5-               , leancheck >= 0.6.4+               , leancheck >= 0.6.5                , template-haskell-               , speculate >= 0.2.6+               , speculate >= 0.2.8   hs-source-dirs:      src   default-language:    Haskell2010 @@ -54,14 +54,22 @@   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+  hs-source-dirs:      tests+  build-depends:       base >= 4 && < 5, leancheck, speculate, extrapolate   default-language:    Haskell2010  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+  hs-source-dirs:      tests+  build-depends:       base >= 4 && < 5, leancheck, speculate, extrapolate+  default-language:    Haskell2010++test-suite utils+  type:                exitcode-stdio-1.0+  main-is:             test-utils.hs+  other-modules:       Test+  hs-source-dirs:      tests+  build-depends:       base >= 4 && < 5, leancheck, speculate, extrapolate   default-language:    Haskell2010

@@ -61,7 +61,6 @@   , module Test.Extrapolate.TypeBinding   , module Test.LeanCheck   , module Test.LeanCheck.Utils.TypeBinding-  , ordering   ) where @@ -83,8 +82,3 @@   , checkResultFor   ) import Test.LeanCheck.Utils.TypeBinding--- TODO: add the following function `ordering` into LeanCheck's TypeBinding---       module; release a new LeanCheck; remove it from here and bump version---       requirement.-ordering :: Ordering-ordering = undefined

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} -- for GHC <= 7.8 -- | -- Module      : Test.Extrapolate.Basic -- Copyright   : (c) 2017 Rudy Matela@@ -23,3 +24,61 @@   instances q = this q id -- The following would allow zero denominators -- expr (n % d) = constant "%" ((%) -:> n) :$ expr n :$ expr d++instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d+         , Generalizable e )+      => Generalizable (a,b,c,d,e) where+  name xyzwv = name x ++ name y ++ name z ++ name w ++ name v+               where (x,y,z,w,v) = xyzwv+  expr (x,y,z,w,v) = constant ",,,," ((,,,,) ->>>>>: (x,y,z,w,v))+                  :$ expr x :$ expr y :$ expr z :$ expr w :$ expr v+  instances xyzwv = this xyzwv $ instances x . instances y . instances z+                               . instances w . instances v+                    where (x,y,z,w,v) = xyzwv++instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d+         , Generalizable e, Generalizable f )+      => Generalizable (a,b,c,d,e,f) where+  name xyzwvu = name x ++ name y ++ name z ++ name w ++ name v ++ name u+          where (x,y,z,w,v,u) = xyzwvu+  expr (x,y,z,w,v,u) = constant ",,,,," ((,,,,,) ->>>>>>: (x,y,z,w,v,u))+                    :$ expr x :$ expr y :$ expr z :$ expr w :$ expr v :$ expr u+  instances xyzwvu = this xyzwvu $ instances x . instances y . instances z+                                 . instances w . instances v . instances u+               where (x,y,z,w,v,u) = xyzwvu++instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d+         , Generalizable e, Generalizable f, Generalizable g )+      => Generalizable (a,b,c,d,e,f,g) where+  name xyzwvut = name x ++ name y ++ name z ++ name w+              ++ name v ++ name u ++ name t+           where (x,y,z,w,v,u,t) = xyzwvut+  expr (x,y,z,w,v,u,t) = constant ",,,,,," ((,,,,,,) ->>>>>>>: (x,y,z,w,v,u,t))+                      :$ expr x :$ expr y :$ expr z :$ expr w+                      :$ expr v :$ expr u :$ expr t+  instances xyzwvut = this xyzwvut+                    $ instances x . instances y . instances z . instances w+                    . instances v . instances u . instances t+                where (x,y,z,w,v,u,t) = xyzwvut++#if __GLASGOW_HASKELL__ < 710+-- No 8-tuples for you:+-- On GHC 7.8, 8-tuples are not Typeable instances.  We could add a standalone+-- deriving clause, but that may cause trouble if some other library does the+-- same.  User should declare Generalizable 8-tuples manually when using GHC <=+-- 7.8.+#else+instance ( Generalizable a, Generalizable b, Generalizable c, Generalizable d+         , Generalizable e, Generalizable f, Generalizable g, Generalizable h )+      => Generalizable (a,b,c,d,e,f,g,h) where+  name xyzwvuts = name x ++ name y ++ name z ++ name w+               ++ name v ++ name u ++ name t ++ name s+    where (x,y,z,w,v,u,t,s) = xyzwvuts+  expr (x,y,z,w,v,u,t,s) = constant ",,,,,,," ((,,,,,,,) ->>>>>>>>: (x,y,z,w,v,u,t,s))+                        :$ expr x :$ expr y :$ expr z :$ expr w+                        :$ expr v :$ expr u :$ expr t :$ expr s+  instances xyzwvuts = this xyzwvuts+                     $ instances x . instances y . instances z . instances w+                     . instances v . instances u . instances t . instances s+    where (x,y,z,w,v,u,t,s) = xyzwvuts+#endif

@@ -34,10 +34,14 @@   , counterExampleGen   , counterExampleGens +  , generalizations   , generalizationsCE   , generalizationsCEC   , generalizationsCounts +  , weakestCondition+  , candidateConditions+   , conditionalGeneralization   , matchList   , newMatches@@ -168,20 +172,27 @@   instances xy  =  this xy $ instances (fst xy)                            . instances (snd xy) -instance (Generalizable a, Generalizable b, Generalizable c) => Generalizable (a,b,c) where-  name xyz  =  name ((\(x,_,_) -> x) xyz)-            ++ name ((\(_,y,_) -> y) xyz)-            ++ name ((\(_,_,z) -> z) xyz)+instance (Generalizable a, Generalizable b, Generalizable c)+      => Generalizable (a,b,c) where+  name xyz  =  name x ++ name y ++ name z+               where  (x,y,z) = xyz   expr (x,y,z)  =  constant ",," ((,,) ->>>: (x,y,z))                 :$ expr x :$ expr y :$ expr z-  instances xyz  =  this xyz $ instances (fst xyz)-                             . instances (snd xyz)-                             . instances (trd xyz)-    where-    fst (x,_,_) = x-    snd (_,y,_) = y-    trd (_,_,z) = z+  instances xyz  =  this xyz $ instances x . instances y . instances z+                    where (x,y,z) = xyz +instance (Generalizable a, Generalizable b, Generalizable c, Generalizable d)+      => Generalizable (a,b,c,d) where+  name xyzw  =  name x ++ name y ++ name z ++ name w+                where (x,y,z,w) = xyzw+  expr (x,y,z,w)  =  constant ",,," ((,,,) ->>>>: (x,y,z,w))+                  :$ expr x :$ expr y :$ expr z :$ expr w+  instances xyzw  =  this xyzw $ instances x+                               . instances y+                               . instances z+                               . instances w+                     where (x,y,z,w) = xyzw+ instance Generalizable a => Generalizable [a] where   name xs  =  name (head xs) ++ "s"   expr (xs@[])      =  showConstant  ([]    -: xs)@@ -428,22 +439,34 @@  weakestCondition :: Testable a => Int -> a -> [Expr] -> Expr weakestCondition m p es = head $+  [ c | c <- candidateConditions p es+      , isCounterExampleUnder m p c es+      ] ++ [expr False]+  where++candidateConditions :: Testable a => a -> [Expr] -> [Expr]+candidateConditions p es = expr True :   [ c-  | c <- constant "True" True : candidates+  | c <- candidateExpressions p es   , typ c == boolTy+  , hasVar c   , not (isAssignment c)-  , not (isAssignmentTest is m c)-  , isCounterExampleUnder m p c es-  ] ++ [ constant "False" False ]+  , not (isAssignmentTest is (maxTests p) c)+  ]   where   is = tinstances p-  candidates = concat . take (maxConditionSize p) . expressionsTT-             . foldr (\/) [vs ++ esU]-             $ [ eval (error msg :: [[Expr]]) ess-               | Instance "Listable" _ [ess] <- tinstances p ]++-- | Canditate expressions to appear in conditions+candidateExpressions :: Testable a => a -> [Expr] -> [Expr]+candidateExpressions p es = concat . take (maxConditionSize p) . expressionsTT+                         . foldr (\/) [vs ++ esU]+                         $ [ eval (error msg :: [[Expr]]) ess+                           | Instance "Listable" _ [ess] <- is ]+  where   vs = [Var n t | (t,n) <- vars es]-  esU = concat [es | Instance "Background" _ es <- tinstances p]-  msg = "weakestCondition: wrong type, not [[Expr]]"+  esU = concat [es | Instance "Background" _ es <- is]+  msg = "canditateConditions: wrong type, not [[Expr]]"+  is = tinstances p  isCounterExampleUnder :: Testable a => Int -> a -> Expr -> [Expr] -> Bool isCounterExampleUnder m p c es = and'

@@ -10,24 +10,7 @@ -- Some type binding operators that are useful when defining Generalizable -- instances. module Test.Extrapolate.TypeBinding-  ( argTypes0-  , argTypes1-  , argTypes2-  , argTypes3-  , argTypes4-  , argTypes5-  , argTypes6-  , argTypes7-  , argTypes8-  , argTypes9-  , argTypes10-  , argTypes11-  , argTypes12--  , argTys1-  , argTys2--  , argTy1of1+  ( argTy1of1   , argTy1of2, argTy2of2   , argTy1of3, argTy2of3, argTy3of3   , argTy1of4, argTy2of4, argTy3of4, argTy4of4@@ -38,8 +21,6 @@  -- TODO: reexport LeanCheck's typebinding operators --- TODO: remove argTypesN and argTysN, unused and uneeded- argTypes0 :: a -> a argTypes0 f = f @@ -100,13 +81,6 @@            ->  a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l            -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) argTypes12 f _ _ _ _ _ _ _ _ _ _ _ _ = f---argTys1 :: con a -> a -> con a-argTys1 x _ = x--argTys2 :: con a b -> a -> b -> con a b-argTys2 x _ _ = x   argTy1of1 :: con a -> a

@@ -7,7 +7,11 @@ -- This module is part of Extrapolate, -- a library for generalization of counter-examples. ----- Misc. utilities.+-- Miscellaneous utility functions.+--+-- This is not intended to be used by users of Extrapolate, only by modules of+-- Extrapolate itself.  Expect symbols exported here to come and go with every+-- minor version. module Test.Extrapolate.Utils   ( (+++)   , nubMerge

@@ -12,16 +12,26 @@    , (-:-), 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@@ -40,6 +50,7 @@ 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)@@ -82,6 +93,16 @@ 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) @@ -103,6 +124,11 @@ 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@@ -127,12 +153,38 @@   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 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

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} -- Copyright (c) 2017 Rudy Matela. -- Distributed under the 3-Clause BSD licence (see the file LICENSE). import Test@@ -60,17 +61,20 @@   , generalizableOK n (int,bool)   , generalizableOK n ((),integer)   , generalizableOK n ((),bool,integer)--- TODO: implement further tuple instances (4,5,6) and uncomment below---, generalizableOK n (int,(),bool,integer)---, generalizableOK n (int,(),bool,integer,char)---, generalizableOK n (string,int,(),bool,integer,char)+  , generalizableOK n (int,(),bool,integer)+  , generalizableOK n (int,(),bool,integer,char)+  , generalizableOK n (string,int,(),bool,integer,char) -- TODO: implement further tuple instances (7,8,9,10,11,12) and uncomment below---, generalizableOK n ((),(),(),(),(),(),())---, generalizableOK n ((),(),(),(),(),(),(),())+  , generalizableOK n ((),(),(),(),(),(),())+#if __GLASGOW_HASKELL__ < 710+-- no 8-tuples for you+#else+  , generalizableOK n ((),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),(),(),()) --, generalizableOK n ((),(),(),(),(),(),(),(),(),(),(),())+#endif    -- Silly test, as it basically replicates the actual implementation:   , backgroundOf int =$ sort $= [ constant "==" $ (==) -:> int@@ -101,6 +105,58 @@   , not $ mayb int `bgSubset`        [mayb [int]]   , not $ mayb int `sameNamesIn`     [mayb [int]]   , not $ mayb int `sameTiersIn`     [mayb [int]]++  , generalizations (instances (undefined :: [Int]) []) [expr [0,0::Int]]+    == map (:[])+       [ _is+       , _i -:- _is+       , _i -:- _i -:- _is+       , _i -:- _i -:- ll+       , _i -:- zero -:- _is+       , _i -:- zero -:- ll+       , zero -:- _is+       , zero -:- _i -:- _is+       , zero -:- _i -:- ll+       , zero -:- zero -:- _is+       ]++  , [ canonicalizeWith (instances (undefined :: [Int]) []) g'+    | g <- generalizations (instances (undefined :: [Int]) []) [expr [0,0::Int]]+    , g' <- vassignments g ]+    == map (:[])+       [ _is+       , _i -:- _is+       , _i -:- _i -:- _is+       , xx -:- xx -:- _is+       , _i -:- _i -:- ll+       , xx -:- xx -:- ll+       , _i -:- zero -:- _is+       , _i -:- zero -:- ll+       , zero -:- _is+       , zero -:- _i -:- _is+       , zero -:- _i -:- ll+       , zero -:- zero -:- _is+       ]++  , candidateConditions (([int] >- bool) `With` MaxConditionSize 3) [xxs]+    == [ true, elem' zero xxs ]++  , candidateConditions (([int] >- bool) `With` MaxConditionSize 3) [xx -:- xxs]+    =$ sort+    $= [ true+       , elem' zero xxs+       , elem' xx ll+       , elem' xx xxs+       , zero -/=- xx+       , xx   -/=- zero+       , xx   -/=- xx+       , zero -<- xx+       , xx   -<- zero+       , xx   -<- xx+       , zero -<=- xx+       , xx   -<=- zero+       , xx   -<=- xx+       ]   ]  listBackgroundOK :: Generalizable a => a -> Bool

@@ -0,0 +1,18 @@+-- Copyright (c) 2017 Rudy Matela.+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Test+import Test.Extrapolate.Utils++main :: IO ()+main = mainTest tests 1000++tests :: Int -> [Bool]+tests n =+  [ True++  , holds n $ elemBy (==) ==== elem -:> ()+  , holds n $ elemBy (==) ==== elem -:> int+  , holds n $ elemBy (==) ==== elem -:> bool+  , holds n $ elemBy (==) ==== elem -:> [int]+  , holds n $ elemBy (==) ==== elem -:> [bool]+  ]