diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/TODO.md b/TODO.md new file mode 100644 --- /dev/null +++ b/TODO.md @@ -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. diff --git a/extrapolate.cabal b/extrapolate.cabal new file mode 100644 --- /dev/null +++ b/extrapolate.cabal @@ -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 +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 diff --git a/src/Test/Extrapolate.hs b/src/Test/Extrapolate.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate.hs @@ -0,0 +1,39 @@ +-- | +-- Module : Test.Extrapolate +-- Copyright : (c) 2017 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Test/Extrapolate/Basic.hs b/src/Test/Extrapolate/Basic.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate/Basic.hs @@ -0,0 +1,24 @@ +-- | +-- Module : Test.Extrapolate.Basic +-- Copyright : (c) 2017 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Test/Extrapolate/Core.hs b/src/Test/Extrapolate/Core.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate/Core.hs @@ -0,0 +1,404 @@ +-- | +-- Module : Test.Extrapolate.Core +-- Copyright : (c) 2017 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Test/Extrapolate/Derive.hs b/src/Test/Extrapolate/Derive.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate/Derive.hs @@ -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 +-- +-- 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 [] diff --git a/src/Test/Extrapolate/Exprs.hs b/src/Test/Extrapolate/Exprs.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate/Exprs.hs @@ -0,0 +1,86 @@ +-- | +-- Module : Test.Extrapolate.IO +-- Copyright : (c) 2017 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Test/Extrapolate/IO.hs b/src/Test/Extrapolate/IO.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate/IO.hs @@ -0,0 +1,155 @@ +-- | +-- Module : Test.Extrapolate.IO +-- Copyright : (c) 2017 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Test/Extrapolate/TypeBinding.hs b/src/Test/Extrapolate/TypeBinding.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate/TypeBinding.hs @@ -0,0 +1,174 @@ +-- | +-- Module : Test.Extrapolate.TypeBinding +-- Copyright : (c) 2017 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Test/Extrapolate/Utils.hs b/src/Test/Extrapolate/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Test/Extrapolate/Utils.hs @@ -0,0 +1,36 @@ +-- | +-- Module : Test.Extrapolate.Utils +-- Copyright : (c) 2017 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 +++ diff --git a/tests/test-extrapolate.hs b/tests/test-extrapolate.hs new file mode 100644 --- /dev/null +++ b/tests/test-extrapolate.hs @@ -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 + ]