packages feed

extrapolate (empty) → 0.0.1

raw patch · 14 files changed

+1579/−0 lines, 14 filesdep +basedep +leancheckdep +speculatesetup-changed

Dependencies added: base, leancheck, speculate, template-haskell

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2017, Rudy Matela++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Rudy Matela nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,48 @@+Extrapolate+===========++[![Extrapolate Build Status][build-status]][build-log]+[![Extrapolate on Hackage][hackage-version]][extrapolate-on-hackage]++Extrapolate automatically generalizes counter-examples to test properties.+++Example+-------++Consider the following (faulty) sort function and property:++    sort :: Ord a => [a] -> [a]+    sort [] = []+    sort (x:xs) = sort (filter (< x) xs)+               ++ [x]+               ++ sort (filter (> x) xs)++    prop_sortCount :: Ord a => a -> [a] -> Bool+    prop_sortCount x xs = count x (sort xs) == count x xs+      where+      count x = length . filter (== x)++Extrapolate both returns a fully defined counter-example along with a+generalization:++    > import Test.Extrapolate+    > check (prop_sortCount :: Int -> [Int] -> Bool)+    *** Failed! Falsifiable (after 4 tests):+    0 [0,0]+    Generalization:+    x (x:x:xs)++This hopefully makes it easier to find the source of the bug.+In this case, the faulty sort function discard repeated elements.+++More documentation+------------------++For more examples, see the [eg](eg) folder.++[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+[extrapolate-on-hackage]: https://hackage.haskell.org/package/extrapolate
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ TODO.md view
@@ -0,0 +1,147 @@+TODO+====++A non-exhaustive list of things TO DO for Extrapolate.++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+  `bleh` and `blih`.  I found:++  - one on Duregard's licentiate Thesis:  `prop_cycle` from `BNFC-meta`.+  - one on Duregard's doctorate Thesis.+  - one on SmallCheck's paper: `prop_insertRB` from RedBlack++  there are none on:++  - QuickCheck+  - Testing and Tracing with Quickcheck and Hat+  - SmartCheck+  - Feat+  - Real World Haskell+  - Learn-you-a-haskell+  - Growing and shrinking polygons+  - QuickFuzz++* `add-th-eg`:+  add the parser example from the Feat paper;++* `apply-lazysmallcheck`:+  apply Lazy SmallCheck to calculator and parse and record the results.++feature+-------++* `report-multiple-generalizations`:+  when there is more than one generalization and they don't encompass+  one-another, report both.++* `detect-silly-conditionals`:+  eg:++    xs  when  0 /= length xs++  that's just:++    _:_++  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`+  instead of              `(Div (C 0) (Add (C 0) (C 0)))`;++  I got it to print the  middle one, by just: `-- not (isAssignment wc)` and+  `constant "negate" (negate -:> x) in the background`.+++* `improve-record-printing`:+  Improve the record printing by explictly printing records and _not_ showing+  variables.  For example, when testing `prop_delete`, currently we get:++	StackSet (Screen (Workspace x y (Just s)) z x’) ss ws crs++  but we could get instead, with the actual following indentation:++    > check prop_delete+    StackSet { current  = Screen+                        { workspace = Workspace+                                    { tag    = x+                                    , layout = y+                                    , stack  = Just s+                                    }+                        , screen       = z+                        , screenDetail = x'+                        }+             , visible  = ss+             , hidden   = ws+             , floating = crs+             }++  which could be further summarized to:++	stackset {current = scr {workspace = ws {stack = Just s}}}+++performance and improvements in the algorithm (only later)+----------------------------------------------------------++* `type-after-type`:+  to improve performance, instead of working with all types at once, perform+  the algorithm type after type++* `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+---------++* `nlp-example`:+  add the NLP example from the SmartCheck paper.  I don't think I'll use this+  because of a few issues.++  GenI has the bit-rot:++  - GenI 0.24.3 refuses to build on GHC 8.0.1;++  - GenI 0.24.3 builds on GHC 7.8 but test files are missing;++  - The version on git is the most up-to-date contradicting the fact that it is+	supposed to be a mirror from Darcs.  It does not seem to be building on+	Travis.  It has tests, but I have not tried compiling it.++  Lee Pike's paper does not list the exact property and fault for which+  SmartCheck recuces its counterexample.  I also looked at the TeX comments,+  and the info is also not there.  The mentioned stackoverflow question does+  not help with that either.  I could certainly ask of course if I choose to+  carry on with this.++  Thinking again, maybe it is a good idea to use this.  It is a real library+  with real bugs in the git history.
+ extrapolate.cabal view
@@ -0,0 +1,65 @@+name:                extrapolate+version:             0.0.1+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])@:+  .+  * @[0,0]@ is a counter-example;+  .+  * @x:x:_@ is a generalized counter-example.++homepage:            https://github.com/rudymatela/extrapolate#readme+license:             BSD3+license-file:        LICENSE+author:              Rudy Matela+maintainer:          Rudy Matela <rudy@matela.com.br>+category:            Testing+build-type:          Simple+cabal-version:       >=1.18++extra-doc-files: README.md+               , TODO.md+tested-with: GHC==8.0++source-repository head+  type:            git+  location:        https://github.com/rudymatela/speculate++source-repository this+  type:            git+  location:        https://github.com/rudymatela/speculate+  tag:             v0.0.1++library+  exposed-modules: Test.Extrapolate+                 , Test.Extrapolate.Core+                 , Test.Extrapolate.Basic+                 , Test.Extrapolate.Derive+                 , Test.Extrapolate.Exprs+                 , Test.Extrapolate.IO+                 , Test.Extrapolate.TypeBinding+  other-modules:   Test.Extrapolate.Utils+  other-extensions:    TemplateHaskell, CPP+  build-depends: base >=4.9 && <4.10+               , leancheck+               , template-haskell+               , speculate+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -dynamic++test-suite test+  type:                exitcode-stdio-1.0+  main-is:             test-extrapolate.hs+  hs-source-dirs:      src, tests+  build-depends:       base >= 4 && < 5, leancheck, speculate, template-haskell+  default-language:    Haskell2010+  ghc-options:         -dynamic++-- NOTE: for some reason, my system is not able to compile extrapolate using+-- cabal unless the -dynamic flag is present in ghc-options.  I do not know if+-- this affects other systems, so I am including it by default.+--           --  Rudy  2017-08-01
+ src/Test/Extrapolate.hs view
@@ -0,0 +1,39 @@+-- |+-- Module      : Test.Extrapolate+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- Extrapolate is a library for generalization of counter-examples.+--+-- Consider the following faulty implementation of sort:+--+-- > sort :: Ord a => [a] -> [a]+-- > sort [] = []+-- > sort (x:xs) = sort (filter (< x) xs)+-- >            ++ [x]+-- >            ++ sort (filter (> x) xs)+--+-- Extrapolate works like so:+--+-- > > check $ \xs -> ordered (sort xs)+-- > +++ OK, passed 360 tests!+-- > > check $ \x xs -> count x (sort xs) == count x xs+-- > *** Failed! Falsifiable (after 4 tests):+-- > 0 [0,0]+-- > Generalization:+-- > x (x:x:xs)+module Test.Extrapolate+  ( module Test.Extrapolate.Core+  , module Test.Extrapolate.Basic+  , module Test.Extrapolate.Derive+  , module Test.Extrapolate.TypeBinding+  , module Test.Extrapolate.IO+  )+where++import Test.Extrapolate.Core+import Test.Extrapolate.Basic+import Test.Extrapolate.Derive+import Test.Extrapolate.TypeBinding+import Test.Extrapolate.IO
+ src/Test/Extrapolate/Basic.hs view
@@ -0,0 +1,24 @@+-- |+-- Module      : Test.Extrapolate.Basic+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Extrapolate,+-- a library for generalization of counter-examples.+--+-- This provides the basic functionality of extrapolate.  You will have better+-- luck importing "Test.Extrapolate" directly.+module Test.Extrapolate.Basic+  ( module Test.Extrapolate.Core+  )+where++import Test.Extrapolate.Core+import Data.Ratio++instance (Integral a, Generalizable a) => Generalizable (Ratio a) where+  expr = showConstant+  instances q = this "q" q id+-- The following would allow zero denominators+-- expr (n % d) = constant "%" ((%) -:> n) :$ expr n :$ expr d
+ src/Test/Extrapolate/Core.hs view
@@ -0,0 +1,404 @@+-- |+-- Module      : Test.Extrapolate.Core+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Extrapolate,+-- a library for generalization of counter-examples.+--+-- This is the core of extrapolate.+module Test.Extrapolate.Core+  ( module Test.LeanCheck+  , module Test.LeanCheck.Utils.TypeBinding+  , module Test.Extrapolate.Exprs++  , Generalizable (..)+  , this+  , these+  , usefuns+  , (+++)+  , nameOf++  , Option (..)+  , options+  , WithOption (..)+  , maxTests+  , extraInstances+  , maxConditionSize++  , counterExampleGen+  , counterExampleGens++  , generalizationsCE+  , generalizationsCEC+  , generalizationsCounts++  , conditionalGeneralization+  , matchList+  , newMatches++  , Testable+  , results++  , areInstancesOf++  , expressionsT+  )+where++import Test.Extrapolate.Utils+import Test.LeanCheck.Utils+import Test.LeanCheck.Utils.TypeBinding+import Data.Typeable+import Data.Dynamic+import Test.LeanCheck hiding+  ( Testable (..)+  , results+  , counterExamples+  , counterExample+  , productWith+  , check+  , checkFor+  , checkResult+  , checkResultFor+  )+import Test.Extrapolate.Exprs (fold, unfold)+import Data.Maybe (listToMaybe, fromJust, isJust)+import Data.Either (isRight)+import Data.List (insert)+import Test.Extrapolate.Exprs+import Test.LeanCheck.Error (errorToFalse)++class (Listable a, Typeable a, Show a) => Generalizable a where+  expr :: a -> Expr+  useful :: a -> [Expr]+  useful _ = []+  instances :: a -> Instances -> Instances+  instances _ = id++instance Generalizable () where+  expr = showConstant+  instances u = this "u" u id++instance Generalizable Bool where+  expr = showConstant+  instances p = these "p" p+              [ constant "not" not ]+              $ id++instance Generalizable Int where+  expr = showConstant+  instances x = these "x" x+              [ constant "==" ((==) -:> x)+              , constant "/=" ((/=) -:> x)+              , constant "<"  ((<)  -:> x)+              , constant "<=" ((<=) -:> x)+              ]+              $ id++instance Generalizable Integer where+  expr = showConstant+  instances x = these "x" x+              [ constant "==" ((==) -:> x)+              , constant "/=" ((/=) -:> x)+              , constant "<"  ((<)  -:> x)+              , constant "<=" ((<=) -:> x) ]+              $ id++instance Generalizable Char where+  expr = showConstant+  instances c = these "c" c+              [ constant "==" ((==) -:> c)+              , constant "/=" ((/=) -:> c)+              , constant "<"  ((<)  -:> c)+              , constant "<=" ((<=) -:> c) ]+              $ id++instance (Generalizable a) => Generalizable (Maybe a) where+  expr mx@Nothing   =  constant "Nothing" (Nothing -: mx)+  expr mx@(Just x)  =  constant "Just"    (Just   ->: mx) :$ expr x+  instances mx  = these "mx" mx+                [ constant "Just"    (Just   ->: mx) ]+                $ instances (fromJust mx)++instance (Generalizable a, Generalizable b) => Generalizable (a,b) where+  expr (x,y)  =  constant "," ((,) ->>: (x,y))+              :$ expr x :$ expr y+  instances xy  =  this "xy" xy $ instances (fst xy)+                                . instances (snd xy)++instance (Generalizable a, Generalizable b, Generalizable c) => Generalizable (a,b,c) where+  expr (x,y,z)  =  constant ",," ((,,) ->>>: (x,y,z))+                :$ expr x :$ expr y :$ expr z+  instances xyz  =  this "xyz" xyz $ instances (fst xyz)+                                   . instances (snd xyz)+                                   . instances (trd xyz)+    where+    fst (x,_,_) = x+    snd (_,y,_) = y+    trd (_,_,z) = z++instance Generalizable a => Generalizable [a] where+  expr (xs@[])      =  showConstant  ([]    -: xs)+  expr (xs@(y:ys))  =  constant ":"  ((:) ->>: xs) :$ expr y :$ expr ys+  instances xs  = these (nameOf (head xs) ++ "s") xs+                [ constant "length" (length -:> xs)+                , constant "filter" (filter ->:> xs) ]+                $ instances (head xs)++nameOf :: Generalizable a => a -> String+nameOf x = head $ names (instances x []) (typeOf x)++-- | Usage: @ins "x" (undefined :: Type)@+ins :: (Typeable a, Listable a, Show a)+    => String -> a -> Instances+ins n x = listable x +++ name n x++this :: (Typeable a, Listable a, Show a)+     => String -> a -> (Instances -> Instances) -> Instances -> Instances+this n x f is =+  if isListable is (typeOf x)+    then is+    else f (ins n x +++ is)++-- bad function naming!+these :: (Typeable a, Listable a, Show a)+      => String -> a -> [Expr] -> (Instances -> Instances) -> Instances -> Instances+these n x es f is =+  if isListable is (typeOf x)+    then is+    else f (listable x +++ name n x +++ usefuns x es +++ is)++-- bad function naming!+usefuns :: Typeable a => a -> [Expr] -> Instances+usefuns x es = [ Instance "Background" (typeOf x) es ]++getBackground :: Instances -> [Expr]+getBackground is = concat [es | Instance "Background" _ es <- is]++-- |  generalizes an expression by making it less defined,+--    starting with smaller changes, then bigger changes:+--+--    1: change constant to variable+--    1.1: if a variable of the constant type exists, use it+--    1.2: if not, introduce new variable+--    2: change a variable to a new variable+--+-- The above is the ideal, but let's start with a simpler algorithm:+--+--    1: change constant to hole+generalizations1 :: Instances -> Expr -> [Expr]+generalizations1 is (Var _ _)        =  []+generalizations1 is (Constant _ dx)  =+  [holeOfTy t | let t = dynTypeRep dx, isListable is t]+generalizations1 is (e1 :$ e2) =+  [holeOfTy t | isRight (etyp (e1 :$ e2))+              , let t = typ (e1 :$ e2)+              , isListable is t]+  ++ productWith (:$) (generalizations1 is e1) (generalizations1 is e2)+  ++ map (:$ e2) (generalizations1 is e1)+  ++ map (e1 :$) (generalizations1 is e2)+-- note above, I should only generalize types that I know how to enumerate,+-- i.e.: types that I have TypeInfo of!++generalizations :: Instances -> [Expr] -> [ [Expr] ]+generalizations is = map unfold . generalizations1 is . fold++productWith :: (a -> b -> c) -> [a] -> [b] -> [c]+productWith f xs ys = [f x y | x <- xs, y <- ys]++-- I don't love Option/WithOption.  It is clever but it is not __clear__.+-- Maybe remove from future versions of the tool?+data Option = MaxTests Int+            | ExtraInstances Instances+            | MaxConditionSize Int+  deriving Show++data WithOption a = With+                  { property :: a+                  , option :: Option }++type Options = [Option]++maxTests :: Testable a => a -> Int+maxTests p = head $ [m | MaxTests m <- options p] ++ [360]++extraInstances :: Testable a => a -> Instances+extraInstances p = concat [is | ExtraInstances is <- options p]++maxConditionSize :: Testable a => a -> Int+maxConditionSize p = head $ [m | MaxConditionSize m <- options p] ++ [5]++class Testable a where+  resultiers :: a -> [[([Expr],Bool)]]+  ($-|) :: a -> [Expr] -> Bool+  tinstances :: a -> Instances+  options :: a -> Options+  options _ = []++instance Testable a => Testable (WithOption a) where+  resultiers (p `With` o) = resultiers p+  (p `With` o) $-| es     = p $-| es+  tinstances (p `With` o) = tinstances p ++ extraInstances (p `With` o)+  options    (p `With` o) = o : options p++instance Testable Bool where+  resultiers p = [[([],p)]]+  p $-| []  =  p+  p $-| _   =  error "($-|): too many arguments"+  tinstances _ = []++instance (Testable b, Generalizable a, Listable a) => Testable (a->b) where+  resultiers p = concatMapT resultiersFor tiers+    where resultiersFor x = mapFst (expr x:) `mapT` resultiers (p x)+          mapFst f (x,y) = (f x, y)+  p $-| []      =  error "($-|): too few arguments"+  p $-| (e:es)  =  p (eval (error "($-|): wrong type") e) $-| es+  tinstances p = instances (undefarg p) $ tinstances (p undefined)+    where+    undefarg :: (a -> b) -> a+    undefarg _ = undefined++results :: Testable a => a -> [([Expr],Bool)]+results = concat . resultiers++counterExamples :: Testable a => Int -> a -> [[Expr]]+counterExamples n p = [as | (as,False) <- take n (results p)]++counterExample :: Testable a => Int -> a -> Maybe [Expr]+counterExample n = listToMaybe . counterExamples n++counterExampleGens :: Testable a => Int -> a -> Maybe ([Expr],[[Expr]])+counterExampleGens n p = case counterExample n p of+  Nothing -> Nothing+  Just es -> Just (es,generalizationsCE n p es)++generalizationsCE :: Testable a => Int -> a -> [Expr] -> [[Expr]]+generalizationsCE n p es =+  [ canonicalizeWith is gs'+  | gs <- generalizations is es+  , gs' <- vassignments gs+  , isCounterExample n p gs'+  ]+  where+  is = tinstances p++generalizationsCEC :: Testable a => Int -> a -> [Expr] -> [(Expr,[Expr])]+generalizationsCEC n p es =+  [ (wc'', gs'')+  | gs <- generalizations is es+  , gs' <- vassignments gs+  , let wc = weakestCondition n p gs'+  , wc /= constant "False" False+  , wc /= constant "True"  True+  , let (wc'':gs'') = canonicalizeWith is (wc:gs')+  ]+  where+  is = tinstances p++isCounterExample :: Testable a => Int -> a -> [Expr] -> Bool+isCounterExample m p = all (not . errorToFalse . (p $-|))+                     . take m+                     . grounds (tinstances p)++generalizationsCounts :: Testable a => Int -> a -> [Expr] -> [([Expr],Int)]+generalizationsCounts n p es =+  [ (canonicalizeWith is gs', countPasses n p gs')+  | gs <- generalizations is es+  , gs' <- vassignments gs+  ]+  where+  is = tinstances p++countPasses :: Testable a => Int -> a -> [Expr] -> Int+countPasses m p = length . filter (p $-|) . take m . grounds (tinstances p)++counterExampleGen :: Testable a => Int -> a -> Maybe ([Expr],Maybe [Expr])+counterExampleGen n p = case counterExampleGens n p of+  Nothing          -> Nothing+  Just (es,[])     -> Just (es,Nothing)+  Just (es,(gs:_)) -> Just (es,Just gs)++areInstancesOf :: [Expr] -> [Expr] -> Bool+es1 `areInstancesOf` es2 = length es1 == length es2+                        && and [e1 `isInstanceOf` e2 | (e1,e2) <- zip es1 es2]+-- change the above to use fold+-- maybe create a module that deals with lists of expressions, called Exprs++-- | List matches of lists of expressions if possible+--+-- > [0,1]   `matchList` [x,y]   = Just [x=0, y=1]+-- > [0,1+2] `matchList` [x,y+y] = Nothing+matchList :: [Expr] -> [Expr] -> Maybe Binds+matchList = m []+  where+  m bs [] [] = Just bs+  m bs (e1:es1) (e2:es2) =+    case matchWith bs e1 e2 of+      Nothing -> Nothing+      Just bs -> m bs es1 es2++-- list only the matches that introduce new variables (not variable-to-variable+-- matches)+newMatches :: [Expr] -> [Expr] -> Maybe Binds+e1 `newMatches` e2 = filter (not . isVar . snd) <$> e1 `matchList` e2+++expressionsT :: [Expr] -> [[Expr]]+expressionsT ds = [ds] \/ productMaybeWith ($$) es es `addWeight` 1+  where+  es = expressionsT ds++expressionsTT :: [[Expr]] -> [[Expr]]+expressionsTT dss = dss \/ productMaybeWith ($$) ess ess `addWeight` 1+  where+  ess = expressionsTT dss++-- given a 100% generalization, >90% generalization, returns a conditional generalization+conditionalGeneralization :: Testable a => Int -> a -> [Expr] -> [Expr] -> Maybe ([Expr],[Expr])+conditionalGeneralization m p es0 es1 = listToMaybe+  [ ([c],es1)+  | isJust $ es0 `newMatches` es1+  , c <- candidates+  , typ c == boolTy+  , any (`elem` vars [c]) [(t,x) | Var x t <- vs]+  , isCounterExampleUnder m p c es1+  ]+  where+  Just esM = es0 `newMatches` es1+  candidates = concat . take (maxConditionSize p) . expressionsT $ vs ++ esU+  vs = reverse [Var x (typ e) | (x,e) <- esM]+  esU = concat [es | Instance "Background" _ es <- tinstances p]++weakestCondition :: Testable a => Int -> a -> [Expr] -> Expr+weakestCondition m p es = head $+  [ c+  | c <- constant "True" True : candidates+  , typ c == boolTy+  , not (isAssignment c)+  , not (isAssignmentTest is m c)+  , isCounterExampleUnder m p c es+  ] ++ [ constant "False" False ]+  where+  is = tinstances p+  candidates = concat . take (maxConditionSize p) . expressionsTT+             . foldr (\/) [vs ++ esU]+             $ [ eval (error msg :: [[Expr]]) ess+               | Instance "Listable" _ [ess] <- tinstances p ]+  vs = [Var n t | (t,n) <- vars es]+  esU = concat [es | Instance "Background" _ es <- tinstances p]+  msg = "weakestCondition: wrong type, not [[Expr]]"++isCounterExampleUnder :: Testable a => Int -> a -> Expr -> [Expr] -> Bool+isCounterExampleUnder m p c es = and'+  [ not . errorToFalse $ p $-| es'+  | (bs,es') <- take m $ groundsAndBinds (tinstances p) es+  , errorToFalse $ eval False (c `assigning` bs)+  ]+  where+  and' ps = and ps && length ps > m `div` 12 -- poor workaround++isVar :: Expr -> Bool+isVar (Var _ _) = True+isVar _         = False
+ src/Test/Extrapolate/Derive.hs view
@@ -0,0 +1,358 @@+{-# LANGUAGE TemplateHaskell, CPP #-}+-- |+-- Module      : Test.Extrapolate.Derive+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Extrapolate,+-- a library for generalization of counter-examples.+--+-- This is a module for deriving 'Generalizable' instances.+--+-- Needs GHC and Template Haskell (tested on GHC 8.0).+--+-- If Extrapolate does not compile under later GHCs, this module is the+-- probable culprit.+module Test.Extrapolate.Derive+  ( deriveGeneralizable+  , deriveGeneralizableIfNeeded+  , deriveGeneralizableCascading+  )+where++import Test.Extrapolate.Core (Generalizable(..), Expr ((:$)))+import Test.Extrapolate.TypeBinding+import Language.Haskell.TH+import Test.LeanCheck.Basic+import Test.LeanCheck.Utils.TypeBinding+import Control.Monad (unless, liftM, liftM2, filterM)+import Data.List (delete,nub,sort)+import Data.Char (toLower)+import Data.Typeable++-- | Derives a 'Generalizable' instance for a given type 'Name'.+--+-- Consider the following @Stack@ datatype:+--+-- > data Stack a = Stack a (Stack a) | Empty+--+-- Writing+--+-- > deriveGeneralizable ''Stack+--+-- will automatically derive the following 'Generalizable' instance:+--+-- > instance Generalizable a => Generalizable (Stack a) where+-- >   tiers = cons2 Stack \/ cons0 Empty+--+-- Needs the @TemplateHaskell@ extension.+deriveGeneralizable :: Name -> DecsQ+deriveGeneralizable = deriveGeneralizableX True False++-- | Same as 'deriveGeneralizable' but does not warn when instance already exists+--   ('deriveGeneralizable' is preferable).+deriveGeneralizableIfNeeded :: Name -> DecsQ+deriveGeneralizableIfNeeded = deriveGeneralizableX False False++-- | Derives a 'Generalizable' instance for a given type 'Name'+--   cascading derivation of type arguments as well.+deriveGeneralizableCascading :: Name -> DecsQ+deriveGeneralizableCascading = deriveGeneralizableX True True++deriveGeneralizableX :: Bool -> Bool -> Name -> DecsQ+deriveGeneralizableX warnExisting cascade t = do+  is <- t `isInstanceOf` ''Generalizable+  if is+    then do+      unless (not warnExisting)+        (reportWarning $ "Instance Generalizable " ++ show t+                      ++ " already exists, skipping derivation")+      return []+    else if cascade+           then reallyDeriveGeneralizableCascading t+           else reallyDeriveGeneralizable t++reallyDeriveGeneralizable :: Name -> DecsQ+reallyDeriveGeneralizable t = do+  isEq <- t `isInstanceOf` ''Eq+  isOrd <- t `isInstanceOf` ''Ord+  (nt,vs) <- normalizeType t+  cxt <- sequence [ [t| $(conT c) $(return v) |]+                  | c <- ''Generalizable:([''Eq | isEq] ++ [''Ord | isOrd])+                  , v <- vs]+  cs <- typeConstructorsArgNames t+  let generalizableExpr = mergeIFns $ foldr1 mergeI+        [ do argTypesN <- lookupValN $ "argTypes" ++ show (length ns)+             let exprs = [[| expr $(varE n) |] | n <- ns]+             let conex = foldl AppE (VarE argTypesN) $ (ConE c:map VarE ns)+             let root = [| constant $(stringE $ showJustName c) $(return conex) |]+             let rhs = foldl (\e1 e2 -> [| $e1 :$ $e2 |]) root exprs+             [d| instance Generalizable $(return nt) where+                   expr ($(conP c (map varP ns))) = $rhs |]+        | (c,ns) <- cs+        ]+  let generalizableInstances = do+        n <- newName "x"+        let rhs = foldr1 (\e1 e2 -> [| $e1 . $e2 |])+                         [letin n c ns | (c,ns) <- cs, not (null ns)]+        case (isEq, isOrd) of+          (True, True) ->+               [d| instance Generalizable $(return nt) where+                     instances $(varP n) = these $(stringE vname) $(varE n)+                                         [ constant "==" ((==) -:> $(varE n))+                                         , constant "/=" ((/=) -:> $(varE n))+                                         , constant "<"  ((<)  -:> $(varE n))+                                         , constant "<=" ((<=) -:> $(varE n)) ]+                                         $ $rhs |]+          (True, False) ->+               [d| instance Generalizable $(return nt) where+                     instances $(varP n) = these $(stringE vname) $(varE n)+                                         [ constant "==" ((==) -:> $(varE n))+                                         , constant "/=" ((/=) -:> $(varE n)) ]+                                         $ $rhs |]+          (False, False) ->+               [d| instance Generalizable $(return nt) where+                     instances $(varP n) = this $(stringE vname) $(varE n) $ $rhs |]+          _ -> error $ "reallyDeriveGeneralizable " ++ show t ++ ": the impossible happened"+  cxt |=>| (generalizableExpr `mergeI` generalizableInstances)+  where+  showJustName = reverse . takeWhile (/= '.') . reverse . show+  vname = map toLower . take 1 $ showJustName t++letin :: Name -> Name -> [Name] -> ExpQ+letin x c ns = do+  und <- VarE <$> lookupValN "undefined"+  let lhs = conP c (map varP ns)+  let rhs = return $ foldl AppE (ConE c) [und | _ <- ns]+  let bot = foldl1 (\e1 e2 -> [| $e1 . $e2 |])+                   [ [| instances $(varE n) |] | n <- ns ]+  [| let $lhs = $rhs `asTypeOf` $(varE x) in $bot |]++typeConstructorsArgNames :: Name -> Q [(Name,[Name])]+typeConstructorsArgNames t = do+  cs <- typeConstructors t+  sequence [ do ns <- sequence [newName "x" | _ <- ts]+                return (c,ns)+           | (c,ts) <- cs ]++lookupValN :: String -> Q Name+lookupValN s = do+  mn <- lookupValueName s+  case mn of+    Just n -> return n+    Nothing -> fail $ "lookupValN: cannot find " ++ s+++data Bla = Bla Int Int+         | Ble Char+  deriving (Eq, Ord, Show)++-- Not only really derive Generalizable instances,+-- but cascade through argument types.+reallyDeriveGeneralizableCascading :: Name -> DecsQ+reallyDeriveGeneralizableCascading t =+      return . concat+  =<< mapM reallyDeriveGeneralizable+  =<< filterM (liftM not . isTypeSynonym)+  =<< return . (t:) . delete t+  =<< t `typeConCascadingArgsThat` (`isntInstanceOf` ''Generalizable)++-- * Template haskell utilities++typeConArgs :: Name -> Q [Name]+typeConArgs t = do+  is <- isTypeSynonym t+  if is+    then liftM typeConTs $ typeSynonymType t+    else liftM (nubMerges . map typeConTs . concat . map snd) $ typeConstructors t+  where+  typeConTs :: Type -> [Name]+  typeConTs (AppT t1 t2) = typeConTs t1 `nubMerge` typeConTs t2+  typeConTs (SigT t _) = typeConTs t+  typeConTs (VarT _) = []+  typeConTs (ConT n) = [n]+#if __GLASGOW_HASKELL__ >= 800+  -- typeConTs (PromotedT n) = [n] ?+  typeConTs (InfixT  t1 n t2) = typeConTs t1 `nubMerge` typeConTs t2+  typeConTs (UInfixT t1 n t2) = typeConTs t1 `nubMerge` typeConTs t2+  typeConTs (ParensT t) = typeConTs t+#endif+  typeConTs _ = []++typeConArgsThat :: Name -> (Name -> Q Bool) -> Q [Name]+typeConArgsThat t p = do+  targs <- typeConArgs t+  tbs   <- mapM (\t' -> do is <- p t'; return (t',is)) targs+  return [t' | (t',p) <- tbs, p]++typeConCascadingArgsThat :: Name -> (Name -> Q Bool) -> Q [Name]+t `typeConCascadingArgsThat` p = do+  ts <- t `typeConArgsThat` p+  let p' t' = do is <- p t'; return $ t' `notElem` (t:ts) && is+  tss <- mapM (`typeConCascadingArgsThat` p') ts+  return $ nubMerges (ts:tss)++-- Normalizes a type by applying it to necessary type variables, making it+-- accept "zero" parameters.  The normalized type is tupled with a list of+-- necessary type variables.+--+-- Suppose:+--+-- > data DT a b c ... = ...+--+-- Then, in pseudo-TH:+--+-- > normalizeType [t|DT|] == Q (DT a b c ..., [a, b, c, ...])+normalizeType :: Name -> Q (Type, [Type])+normalizeType t = do+  ar <- typeArity t+  vs <- newVarTs ar+  return (foldl AppT (ConT t) vs, vs)+  where+    newNames :: [String] -> Q [Name]+    newNames = mapM newName+    newVarTs :: Int -> Q [Type]+    newVarTs n = liftM (map VarT)+               $ newNames (take n . map (:[]) $ cycle ['a'..'z'])++-- Normalizes a type by applying it to units (`()`) while possible.+--+-- > normalizeTypeUnits ''Int    === [t| Int |]+-- > normalizeTypeUnits ''Maybe  === [t| Maybe () |]+-- > normalizeTypeUnits ''Either === [t| Either () () |]+normalizeTypeUnits :: Name -> Q Type+normalizeTypeUnits t = do+  ar <- typeArity t+  return (foldl AppT (ConT t) (replicate ar (TupleT 0)))++-- Given a type name and a class name,+-- returns whether the type is an instance of that class.+isInstanceOf :: Name -> Name -> Q Bool+isInstanceOf tn cl = do+  ty <- normalizeTypeUnits tn+  isInstance cl [ty]++isntInstanceOf :: Name -> Name -> Q Bool+isntInstanceOf tn cl = liftM not (isInstanceOf tn cl)++-- | Given a type name, return the number of arguments taken by that type.+-- Examples in partially broken TH:+--+-- > arity ''Int        === Q 0+-- > arity ''Int->Int   === Q 0+-- > arity ''Maybe      === Q 1+-- > arity ''Either     === Q 2+-- > arity ''Int->      === Q 1+--+-- This works for Data's and Newtype's and it is useful when generating+-- typeclass instances.+typeArity :: Name -> Q Int+typeArity t = do+  ti <- reify t+  return . length $ case ti of+#if __GLASGOW_HASKELL__ < 800+    TyConI (DataD    _ _ ks _ _) -> ks+    TyConI (NewtypeD _ _ ks _ _) -> ks+#else+    TyConI (DataD    _ _ ks _ _ _) -> ks+    TyConI (NewtypeD _ _ ks _ _ _) -> ks+#endif+    TyConI (TySynD _ ks _) -> ks+    _ -> error $ "error (typeArity): symbol " ++ show t+              ++ " is not a newtype, data or type synonym"++-- Given a type name, returns a list of its type constructor names paired with+-- the type arguments they take.+--+-- > typeConstructors ''()    === Q [('(),[])]+--+-- > typeConstructors ''(,)   === Q [('(,),[VarT a, VarT b])]+--+-- > typeConstructors ''[]    === Q [('[],[]),('(:),[VarT a,AppT ListT (VarT a)])]+--+-- > data Pair a = P a a+-- > typeConstructors ''Pair  === Q [('P,[VarT a, VarT a])]+--+-- > data Point = Pt Int Int+-- > typeConstructors ''Point === Q [('Pt,[ConT Int, ConT Int])]+typeConstructors :: Name -> Q [(Name,[Type])]+typeConstructors t = do+  ti <- reify t+  return . map simplify $ case ti of+#if __GLASGOW_HASKELL__ < 800+    TyConI (DataD    _ _ _ cs _) -> cs+    TyConI (NewtypeD _ _ _ c  _) -> [c]+#else+    TyConI (DataD    _ _ _ _ cs _) -> cs+    TyConI (NewtypeD _ _ _ _ c  _) -> [c]+#endif+    _ -> error $ "error (typeConstructors): symbol " ++ show t+              ++ " is neither newtype nor data"+  where+  simplify (NormalC n ts)  = (n,map snd ts)+  simplify (RecC    n ts)  = (n,map trd ts)+  simplify (InfixC  t1 n t2) = (n,[snd t1,snd t2])+  trd (x,y,z) = z++isTypeSynonym :: Name -> Q Bool+isTypeSynonym t = do+  ti <- reify t+  return $ case ti of+    TyConI (TySynD _ _ _) -> True+    _                     -> False++typeSynonymType :: Name -> Q Type+typeSynonymType t = do+  ti <- reify t+  return $ case ti of+    TyConI (TySynD _ _ t') -> t'+    _ -> error $ "error (typeSynonymType): symbol " ++ show t+              ++ " is not a type synonym"++-- Append to instance contexts in a declaration.+--+-- > sequence [[|Eq b|],[|Eq c|]] |=>| [t|instance Eq a => Cl (Ty a) where f=g|]+-- > == [t| instance (Eq a, Eq b, Eq c) => Cl (Ty a) where f = g |]+(|=>|) :: Cxt -> DecsQ -> DecsQ+c |=>| qds = do ds <- qds+                return $ map (`ac` c) ds+#if __GLASGOW_HASKELL__ < 800+  where ac (InstanceD c ts ds) c' = InstanceD (c++c') ts ds+        ac d                   _  = d+#else+  where ac (InstanceD o c ts ds) c' = InstanceD o (c++c') ts ds+        ac d                     _  = d+#endif++mergeIFns :: DecsQ -> DecsQ+mergeIFns qds = do ds <- qds+                   return $ map m' ds+  where+  m' (InstanceD o c ts ds) = InstanceD o c ts [foldr1 m ds]+  FunD n cs1 `m` FunD _ cs2 = FunD n (cs1 ++ cs2)++mergeI :: DecsQ -> DecsQ -> DecsQ+qds1 `mergeI` qds2 = do ds1 <- qds1+                        ds2 <- qds2+                        return $ ds1 `m` ds2+  where+  [InstanceD o c ts ds1] `m` [InstanceD _ _ _ ds2] = [InstanceD o c ts (ds1 ++ ds2)]++whereI :: DecsQ -> [Dec] -> DecsQ+qds `whereI` w = do ds <- qds+                    return $ map (`aw` w) ds+  where aw (InstanceD o c ts ds) w' = InstanceD o c ts (ds++w')+        aw d                     _  = d++-- > nubMerge xs ys == nub (merge xs ys)+-- > nubMerge xs ys == nub (sort (xs ++ ys))+nubMerge :: Ord a => [a] -> [a] -> [a]+nubMerge [] ys = ys+nubMerge xs [] = xs+nubMerge (x:xs) (y:ys) | x < y     = x :    xs  `nubMerge` (y:ys)+                       | x > y     = y : (x:xs) `nubMerge`    ys+                       | otherwise = x :    xs  `nubMerge`    ys++nubMerges :: Ord a => [[a]] -> [a]+nubMerges = foldr nubMerge []
+ src/Test/Extrapolate/Exprs.hs view
@@ -0,0 +1,86 @@+-- |+-- Module      : Test.Extrapolate.IO+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Extrapolate,+-- a library for generalization of counter-examples.+--+-- This module re-exports some functionality from Test.Speculate.Expr, but+-- instead of working on single expressions it works in lists of expressions+-- (the choosen representation for counter-examples).+module Test.Extrapolate.Exprs+  ( canonicalizeWith+  , grounds+  , groundsAndBinds+  , vassignments+  , vars+  , fold+  , unfold+  , isAssignmentTest++  , module Test.Speculate.Expr+  )+where++import Test.Speculate.Expr hiding+  ( ins+  , canonicalizeWith+  , grounds+  , vassignments+  , vars+  )+import qualified Test.Speculate.Expr as E+import qualified Test.Speculate.Engine as E+import Test.LeanCheck.Error (errorToFalse)+import Data.Typeable (typeOf, TypeRep)+import Data.List ((\\))++canonicalizeWith :: Instances -> [Expr] -> [Expr]+canonicalizeWith is = unfold . canonicalizeWith1 is . unrepeatedToHole1 . fold++canonicalizeWith1 :: Instances -> Expr -> Expr+canonicalizeWith1 ti e = e `assigning` ((\(t,n,n') -> (n,Var n' t)) `map` cr [] e)+  where+  cr :: [(TypeRep,String,String)] -> Expr -> [(TypeRep,String,String)]+  cr bs (e1 :$ e2) = cr (cr bs e1) e2+  cr bs (Var n t)+    | n == "" = bs+    | any (\(t',n',_) -> t == t' && n == n') bs = bs+    | otherwise = (t,n,head $ names ti t \\ map (\(_,_,n) -> n) bs):bs+  cr bs _ = bs++unrepeatedToHole1 :: Expr -> Expr+unrepeatedToHole1 e = e `assigning` [(n,Var "" t) | (t,n,1) <- countVars e]++grounds :: Instances -> [Expr] -> [ [Expr] ]+grounds is = map unfold . E.grounds is . fold++groundsAndBinds :: Instances -> [Expr] -> [(Binds,[Expr])]+groundsAndBinds is = map (mapSnd unfold) . E.groundAndBinds is . fold+  where+  mapSnd f (x,y) = (x,f y)++vassignments :: [Expr] -> [[Expr]]+vassignments = map unfold . E.vassignments . fold++vars :: [Expr] -> [(TypeRep,String)]+vars = E.vars . fold++isAssignmentTest :: Instances -> Int -> Expr -> Bool+isAssignmentTest is m e | typ e /= boolTy = False+isAssignmentTest is m e = length rs > 1 && length (filter id rs) == 1+  where+  rs = [errorToFalse $ eval False e' | [e'] <- take m $ grounds is [e]]++data MarkerType = MarkerType++fold :: [Expr] -> Expr+fold []     = constant "[]" MarkerType+fold (e:es) = constant ":"  MarkerType :$ e :$ fold es++unfold :: Expr -> [Expr]+unfold   e'@(Constant "[]" _)              | typ e' == typeOf MarkerType  =  []+unfold ((e'@(Constant ":"  _) :$ e) :$ es) | typ e' == typeOf MarkerType  =  e : unfold es+unfold e  =  error $ "unfold: cannot unfold expression: " ++ showPrecExpr 0 e
+ src/Test/Extrapolate/IO.hs view
@@ -0,0 +1,155 @@+-- |+-- Module      : Test.Extrapolate.IO+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Extrapolate,+-- a library for generalization of counter-examples.+--+-- QuickCheck-like interface.+{-# LANGUAGE CPP #-}+module Test.Extrapolate.IO+  ( check+  , checkResult++  , for+  , withInstances+  , withBackground+  , withConditionSize+  )+where++#if __GLASGOW_HASKELL__ <= 704+import Prelude hiding (catch)+#endif++import Test.Extrapolate.Core+import Data.Maybe (listToMaybe, mapMaybe)+import Data.List (find, intercalate)+import Control.Exception as E (SomeException, catch, evaluate)++for :: Testable a => (WithOption a -> b) -> Int -> a -> b+check `for` m  =  \p -> check $ p `With` MaxTests m++withInstances :: Testable a => (WithOption a -> b) -> Instances -> a -> b+check `withInstances` is  =  \p -> check $ p `With` ExtraInstances is++withBackground :: Testable a => (WithOption a -> b) -> [Expr] -> a -> b+check `withBackground` ufs  =  check `withInstances` usefuns (undefined::Option) ufs++withConditionSize :: Testable a => (WithOption a -> b) -> Int -> a -> b+check `withConditionSize` s  =   \p -> check $ p `With` MaxConditionSize s++-- | Checks a property printing results on 'stdout'+--+-- > > check $ \xs -> sort (sort xs) == sort (xs::[Int])+-- > +++ OK, passed 360 tests.+-- > > check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])+-- > *** Failed! Falsifiable (after 4 tests):+-- > [] [0,0]+-- > Generalization:+-- > [] (x:x:xs)+check :: Testable a => a -> IO ()+check p = checkResult p >> return ()++-- | Check a property+--   printing results on 'stdout' and+--   returning 'True' on success.+--+-- There is no option to silence this function:+-- for silence, you should use 'TestLean.Check.holds'.+checkResult :: Testable a => a -> IO Bool+checkResult p = do+  (r,ces) <- resultIO m p+  putStr . showResult m p ces $ r+  return (isOK r)+  where+  m = maxTests p+  isOK (OK _) = True+  isOK _      = False++data Result = OK        Int+            | Falsified Int [Expr]+            | Exception Int [Expr] String+  deriving (Eq, Show)++resultsIO :: Testable a => Int -> a -> IO [Result]+resultsIO n = sequence . zipWith torio [1..] . take n . results+  where+    tor i (_,True) = OK i+    tor i (as,False) = Falsified i as+    torio i r@(as,_) = E.evaluate (tor i r)+       `catch` \e -> let _ = e :: SomeException+                     in return (Exception i as (show e))++resultIO :: Testable a => Int -> a -> IO (Result, [[Expr]])+resultIO n p = do+  rs <- resultsIO n p+  return ( maybe (last rs) id $ find isFailure rs+         , mapMaybe ce rs )+  where+  isFailure (OK _) = False+  isFailure _      = True+  ce (OK _)             = Nothing+  ce (Falsified _ es)   = Just es+  ce (Exception _ es _) = Just es++showResult :: Testable a => Int -> a -> [[Expr]] -> Result -> String+showResult m p ces (OK n)             = "+++ OK, passed " ++ show n ++ " tests"+                                     ++ takeWhile (\_ -> n < m) " (exhausted)" ++ ".\n\n"+showResult m p ces (Falsified i ce)   = "*** Failed! Falsifiable (after "+                                     ++ show i ++ " tests):\n" ++ showCEC m p ce+showResult m p ces (Exception i ce e) = "*** Failed! Exception '" ++ e ++ "' (after "+                                     ++ show i ++ " tests):\n" ++ showCEC m p ce++showCEC :: Testable a => Int -> a -> [Expr] -> String+showCEC m p es = showCE es ++ "\n\n"+  ++ case generalizationsCE m p es of+       []     -> ""+       (es:_) -> "Generalization:\n"+              ++ showCE es ++ "\n\n"+  ++ case generalizationsCEC m p es of+       []         -> ""+       ((c,es):_) -> "Conditional Generalization:\n"+                  ++ showCE es ++ "  when  "+                  ++ showPrecExpr 0 (prettify c) ++ "\n\n"++showCEG :: Testable a => Int -> a -> [[Expr]] -> [Expr] -> String+showCEG m p ces es = showCE es ++ "\n\n"+  ++ case mg00 of+       Nothing -> ""+       Just es -> "Generalization, 100% failure, "+               ++ show (count (`areInstancesOf` es) ces * 100 `div` m) ++ "% match:\n"+               ++ showCE es ++ "\n\n"+  ++ case (mg10 /= mg00, mg10) of+       (True, Just es) -> "Generalization, >90% failure, "+                       ++ show (count (`areInstancesOf` es) ces * 100 `div` m) ++ "% match:\n"+                       ++ showCE es ++ "\n\n"+       _               -> ""+  ++ case (mg10 /= mg00, mg00, mg10) of+       (True, Just es0, Just es1) -> showCGen es0 es1+       (True, Nothing,  Just es1) -> showCGen es  es1+       _ -> ""+  where+  gcs = generalizationsCounts m p es+  mg00 = listToMaybe [es | (es,0) <- gcs]+  mg10 = listToMaybe [es | (es,n) <- gcs, n <= m `div` 12]+  count p = length . filter p+  showCGen es0 es1 = case conditionalGeneralization m p es0 es1 of+                       Nothing -> ""+                       Just (cs,es) -> "Generalization, 100% failure:\n"+                                    ++ showCE es ++ "  when  "+                                    ++ intercalate ", " [showPrecExpr 0 c | c <- cs]+                                    ++ "\n\n"++showCE :: [Expr] -> String+showCE [e] = showPrecExpr 0 e+showCE es = unwords [showPrecExpr 11 e | e <- es]++-- WARNING: expressions are unevaluable after this, just good for printing+prettify :: Expr -> Expr+prettify (((Constant "<=" _) :$ e1) :$ e2) | lengthE e1 < lengthE e2 = (((Constant ">=" undefined) :$ e2) :$ e1)+prettify (((Constant "<"  _) :$ e1) :$ e2) | lengthE e1 < lengthE e2 = (((Constant ">"  undefined) :$ e2) :$ e1)+prettify (e1 :$ e2) = prettify e1 :$ prettify e2+prettify e = e
+ src/Test/Extrapolate/TypeBinding.hs view
@@ -0,0 +1,174 @@+-- |+-- Module      : Test.Extrapolate.TypeBinding+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Extrapolate,+-- a library for generalization of counter-examples.+--+-- 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+  , argTy1of2, argTy2of2+  , argTy1of3, argTy2of3, argTy3of3+  , argTy1of4, argTy2of4, argTy3of4, argTy4of4+  , argTy1of5, argTy2of5, argTy3of5, argTy4of5, argTy5of5+  , argTy1of6, argTy2of6, argTy3of6, argTy4of6, argTy5of6, argTy6of6+  )+where++argTypes0 :: a -> a+argTypes0 f = f++argTypes1 :: (a -> b) -> a -> (a -> b)+argTypes1 f _ = f++argTypes2 :: (a -> b -> c)+          ->  a -> b+          -> (a -> b -> c)+argTypes2 f _ _ = f++argTypes3 :: (a -> b -> c -> d)+          ->  a -> b -> c+          -> (a -> b -> c -> d)+argTypes3 f _ _ _ = f++argTypes4 :: (a -> b -> c -> d -> e)+          ->  a -> b -> c -> d+          -> (a -> b -> c -> d -> e)+argTypes4 f _ _ _ _ = f++argTypes5 :: (a -> b -> c -> d -> e -> f)+          ->  a -> b -> c -> d -> e+          -> (a -> b -> c -> d -> e -> f)+argTypes5 f _ _ _ _ _ = f++argTypes6 :: (a -> b -> c -> d -> e -> f -> g)+          ->  a -> b -> c -> d -> e -> f+          -> (a -> b -> c -> d -> e -> f -> g)+argTypes6 f _ _ _ _ _ _ = f++argTypes7 :: (a -> b -> c -> d -> e -> f -> g -> h)+          ->  a -> b -> c -> d -> e -> f -> g+          -> (a -> b -> c -> d -> e -> f -> g -> h)+argTypes7 f _ _ _ _ _ _ _ = f++argTypes8 :: (a -> b -> c -> d -> e -> f -> g -> h -> i)+          ->  a -> b -> c -> d -> e -> f -> g -> h+          -> (a -> b -> c -> d -> e -> f -> g -> h -> i)+argTypes8 f _ _ _ _ _ _ _ _ = f++argTypes9 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j)+          ->  a -> b -> c -> d -> e -> f -> g -> h -> i+          -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> j)+argTypes9 f _ _ _ _ _ _ _ _ _ = f++argTypes10 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k)+           ->  a -> b -> c -> d -> e -> f -> g -> h -> i -> j+           -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k)+argTypes10 f _ _ _ _ _ _ _ _ _ _ = f++argTypes11 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l)+           ->  a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k+           -> (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l)+argTypes11 f _ _ _ _ _ _ _ _ _ _ _ = f++argTypes12 :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m)+           ->  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+argTy1of1 _ = undefined+++argTy1of2 :: con a b -> a+argTy1of2 _ = undefined++argTy2of2 :: con a b -> b+argTy2of2 _ = undefined+++argTy1of3 :: con a b c -> a+argTy1of3 _ = undefined++argTy2of3 :: con a b c -> b+argTy2of3 _ = undefined++argTy3of3 :: con a b c -> c+argTy3of3 _ = undefined+++argTy1of4 :: con a b c d -> a+argTy1of4 _ = undefined++argTy2of4 :: con a b c d -> b+argTy2of4 _ = undefined++argTy3of4 :: con a b c d -> c+argTy3of4 _ = undefined++argTy4of4 :: con a b c d -> d+argTy4of4 _ = undefined+++argTy1of5 :: con a b c d e -> a+argTy1of5 _ = undefined++argTy2of5 :: con a b c d e -> b+argTy2of5 _ = undefined++argTy3of5 :: con a b c d e -> c+argTy3of5 _ = undefined++argTy4of5 :: con a b c d e -> d+argTy4of5 _ = undefined++argTy5of5 :: con a b c d e -> e+argTy5of5 _ = undefined+++argTy1of6 :: con a b c d e f -> a+argTy1of6 _ = undefined++argTy2of6 :: con a b c d e f -> b+argTy2of6 _ = undefined++argTy3of6 :: con a b c d e f -> c+argTy3of6 _ = undefined++argTy4of6 :: con a b c d e f -> d+argTy4of6 _ = undefined++argTy5of6 :: con a b c d e f -> e+argTy5of6 _ = undefined++argTy6of6 :: con a b c d e f -> f+argTy6of6 _ = undefined
+ src/Test/Extrapolate/Utils.hs view
@@ -0,0 +1,36 @@+-- |+-- Module      : Test.Extrapolate.Utils+-- Copyright   : (c) 2017 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of Extrapolate,+-- a library for generalization of counter-examples.+--+-- Misc. utilities.+module Test.Extrapolate.Utils+  ( (+++)+  , nubMerge+  , nubMergeOn+  , nubMergeBy+  )+where++import Data.Function (on)++nubMergeBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a]+nubMergeBy cmp (x:xs) (y:ys) = case x `cmp` y of+                                 LT -> x:nubMergeBy cmp xs (y:ys)+                                 GT -> y:nubMergeBy cmp (x:xs) ys+                                 EQ -> x:nubMergeBy cmp xs ys+nubMergeBy _ xs ys = xs ++ ys++nubMergeOn :: Ord b => (a -> b) -> [a] -> [a] -> [a]+nubMergeOn f = nubMergeBy (compare `on` f)++nubMerge :: Ord a => [a] -> [a] -> [a]+nubMerge = nubMergeBy compare++(+++) :: Ord a => [a] -> [a] -> [a]+(+++) = nubMerge+infixr 5 +++
+ tests/test-extrapolate.hs view
@@ -0,0 +1,11 @@+-- Copyright (c) 2017 Rudy Matela.+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Test++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+  [ True+  ]