packages feed

extrapolate 0.2.4 → 0.3.0

raw patch · 12 files changed

+755/−163 lines, 12 filesdep ~leancheckdep ~speculatePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: leancheck, speculate

API changes (from Hackage documentation)

- Test.Extrapolate.Core: conditionalGeneralization :: Testable a => Int -> a -> [Expr] -> [Expr] -> Maybe ([Expr], [Expr])
- Test.Extrapolate.Core: expressionsT :: [Expr] -> [[Expr]]
+ Test.Extrapolate: minFailures :: Testable a => (WithOption a -> b) -> Ratio Int -> a -> b
+ Test.Extrapolate.Core: ConditionBound :: (Maybe Int) -> Option
+ Test.Extrapolate.Core: ConstantBound :: (Maybe Int) -> Option
+ Test.Extrapolate.Core: DepthBound :: (Maybe Int) -> Option
+ Test.Extrapolate.Core: MaxSpeculateSize :: (Maybe Int) -> Option
+ Test.Extrapolate.Core: MinFailures :: (Ratio Int) -> Option
+ Test.Extrapolate.Core: atoms :: Testable a => a -> [[Expr]]
+ Test.Extrapolate.Core: fullInstances :: Testable a => a -> Instances
+ Test.Extrapolate.Core: getBackground :: Instances -> [Expr]
+ Test.Extrapolate.Core: tBackground :: Testable a => a -> [Expr]
+ Test.Extrapolate.Core: theoryAndReprConds :: Testable a => a -> (Thy, [Expr])
+ Test.Extrapolate.Core: theoryAndReprExprs :: Testable a => a -> (Thy, [Expr])
+ Test.Extrapolate.Core: validConditions :: Testable a => (Thy, [Expr]) -> a -> [Expr] -> [(Expr, Int)]
+ Test.Extrapolate.IO: conditionBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b
+ Test.Extrapolate.IO: constantBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b
+ Test.Extrapolate.IO: depthBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b
+ Test.Extrapolate.IO: maxSpeculateSize :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b
+ Test.Extrapolate.IO: minFailures :: Testable a => (WithOption a -> b) -> Ratio Int -> a -> b
+ Test.Extrapolate.Utils: argumentTy :: TypeRep -> TypeRep
+ Test.Extrapolate.Utils: compareIndex :: Eq a => [a] -> a -> a -> Ordering
+ Test.Extrapolate.Utils: discard :: (a -> Bool) -> [a] -> [a]
+ Test.Extrapolate.Utils: maximumOn :: Ord b => (a -> b) -> [a] -> a
+ Test.Extrapolate.Utils: minimumOn :: Ord b => (a -> b) -> [a] -> a
+ Test.Extrapolate.Utils: nubMergeMap :: Ord b => (a -> [b]) -> [a] -> [b]
+ Test.Extrapolate.Utils: pairEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
+ Test.Extrapolate.Utils: pairOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
+ Test.Extrapolate.Utils: quadrupleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (a, b, c, d) -> (a, b, c, d) -> Bool
+ Test.Extrapolate.Utils: quadrupleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (a, b, c, d) -> (a, b, c, d) -> Bool
+ Test.Extrapolate.Utils: resultTy :: TypeRep -> TypeRep
+ Test.Extrapolate.Utils: takeBound :: Maybe Int -> [a] -> [a]
+ Test.Extrapolate.Utils: tripleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (a, b, c) -> (a, b, c) -> Bool
+ Test.Extrapolate.Utils: tripleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (a, b, c) -> (a, b, c) -> Bool
+ Test.Extrapolate.Utils: typesIn :: TypeRep -> [TypeRep]
- Test.Extrapolate.Core: candidateConditions :: Testable a => a -> [Expr] -> [Expr]
+ Test.Extrapolate.Core: candidateConditions :: Testable a => (Thy, [Expr]) -> a -> [Expr] -> [Expr]
- Test.Extrapolate.Core: generalizationsCEC :: Testable a => Int -> a -> [Expr] -> [(Expr, [Expr])]
+ Test.Extrapolate.Core: generalizationsCEC :: Testable a => a -> [Expr] -> [(Expr, [Expr])]
- Test.Extrapolate.Core: weakestCondition :: Testable a => Int -> a -> [Expr] -> Expr
+ Test.Extrapolate.Core: weakestCondition :: Testable a => (Thy, [Expr]) -> a -> [Expr] -> Expr

Files

TODO.md view
@@ -3,10 +3,12 @@  A non-exhaustive list of things TO DO for Extrapolate. +* `deriveGeneralizable` should `deriveListableIfNeeded`.  examples -------- + * `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@@ -36,6 +38,9 @@ feature ------- +* `background-exclusion`:+  add a mechanism to exclude functions from the background.+ * `report-multiple-generalizations`:   when there is more than one generalization and they don't encompass   one-another, report both.@@ -129,7 +134,7 @@   maybe there should be a multi-lgg, or start with all vars different    After some tests, I see that this does not quite work as expected.  c.f.-  `union xs ys == union ys xs`. When incorporating a counterExampe, sometimes+  `union xs ys == union ys xs`. When incorporating a counterExample, sometimes   the generalization will temporarily match some passing tests, only to be   later weeded out by some other counter-example.  There are many many more   combinations of counterexamples 2^#nce then there are candidate@@ -163,3 +168,13 @@    Thinking again, maybe it is a good idea to use this.  It is a real library   with real bugs in the git history.++* `enlarge-default-background`:+  I tried enlarging the default background by including (&&) and (||).  Not+  only there is no effect in the output of the build-in examples, runtime+  increases for up to 33%.++  I also tried enlarging the default background by including functions over+  lists from the prelude, such as: (:), last, reverse, init.  Runtime increases+  by 10x, with no interesting effect on output (most changes are just+  rewritings of the unconditional generalization.
extrapolate.cabal view
@@ -1,5 +1,5 @@ name:                extrapolate-version:             0.2.4+version:             0.3.0 synopsis:            generalize counter-examples of test properties description:   Extrapolate is a tool able to provide generalized counter-examples of test@@ -22,7 +22,7 @@  extra-doc-files: README.md                , TODO.md-tested-with: GHC==8.0, GHC==7.10, GHC==7.8+tested-with: GHC==8.2, GHC==8.0, GHC==7.10, GHC==7.8  source-repository head   type:            git@@ -31,7 +31,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/speculate-  tag:             v0.2.4+  tag:             v0.3.0  library   exposed-modules: Test.Extrapolate@@ -45,9 +45,9 @@                  , Test.Extrapolate.New   other-extensions:    TemplateHaskell, CPP   build-depends: base >= 4 && < 5-               , leancheck >= 0.6.5+               , leancheck >= 0.7                , template-haskell-               , speculate >= 0.2.9+               , speculate >= 0.3.2   hs-source-dirs:      src   default-language:    Haskell2010 @@ -78,6 +78,14 @@ test-suite new   type:                exitcode-stdio-1.0   main-is:             test-new.hs+  other-modules:       Test+  hs-source-dirs:      tests+  build-depends:       base >= 4 && < 5, leancheck, speculate, extrapolate+  default-language:    Haskell2010++test-suite step-by-step+  type:                exitcode-stdio-1.0+  main-is:             test-step-by-step.hs   other-modules:       Test   hs-source-dirs:      tests   build-depends:       base >= 4 && < 5, leancheck, speculate, extrapolate
src/Test/Extrapolate.hs view
@@ -40,6 +40,7 @@   , for   , withBackground   , withConditionSize+  , minFailures  -- * Generalizable types   , Generalizable (..)
src/Test/Extrapolate/Core.hs view
@@ -34,6 +34,7 @@   , (*/=*)   , (*<=*)   , (*<*)+  , tBackground    , counterExamples   , counterExampleGen@@ -44,10 +45,15 @@   , generalizationsCEC   , generalizationsCounts -  , weakestCondition+  , atoms+  , theoryAndReprExprs+  , theoryAndReprConds   , candidateConditions+  , validConditions+  , weakestCondition+  , getBackground+  , fullInstances -  , conditionalGeneralization   , matchList   , newMatches @@ -55,8 +61,6 @@   , results    , areInstancesOf--  , expressionsT   ) where @@ -76,14 +80,17 @@   , checkResult   , checkResultFor   )-import Test.Extrapolate.Exprs (fold, unfold)-import Data.Maybe (listToMaybe, fromJust, fromMaybe, isJust, listToMaybe, catMaybes)+import Data.Maybe import Data.Either (isRight)-import Data.List (insert)+import Data.List (insert, nub, sort) import Data.Functor ((<$>)) -- for GHC <= 7.8 import Test.Extrapolate.Exprs import Test.LeanCheck.Error (errorToFalse)+import Data.Ratio (Ratio, numerator, denominator) import Test.Extrapolate.TypeBinding -- for Haddock+import Test.Speculate.Reason (Thy)+import Test.Speculate.Engine (theoryAndRepresentativesFromAtoms, classesFromSchemasAndVariables)+import Data.Monoid ((<>))  -- | Extrapolate can generalize counter-examples of any types that are --   'Generalizable'.@@ -133,7 +140,8 @@ instance Generalizable Bool where   expr = showConstant   name _ = "p"-  background _ = [ constant "not" not ]+  background p = bgEq p+              ++ [ constant "not" not ]   instances p = this p id  instance Generalizable Int where@@ -158,19 +166,19 @@   expr mx@Nothing   =  constant "Nothing" (Nothing -: mx)   expr mx@(Just x)  =  constant "Just"    (Just   ->: mx) :$ expr x   name mx = "m" ++ name (fromJust mx)-  background mx  =  [ constant "Just" (Just ->: mx) ]-                 ++ bgEqWith1  (maybeEq  ->:> mx)+  background mx  =  bgEqWith1  (maybeEq  ->:> mx)                  ++ bgOrdWith1 (maybeOrd ->:> mx)+                 ++ [ constant "Just" (Just ->: mx) ]   instances mx  =  this mx $ instances (fromJust mx)  instance (Generalizable a, Generalizable b) => Generalizable (Either a b) where   expr lx@(Left x)   =  constant "Left"  (Left  ->: lx) :$ expr x   expr ry@(Right y)  =  constant "Right" (Right ->: ry) :$ expr y   name exy = "e" ++ name (fromLeft exy) ++ name (fromRight exy)-  background exy  =  [ constant "Left"  (Left  ->: exy)-                     , constant "Right" (Right ->: exy) ]-                  ++ bgEqWith2  (eitherEq  ->>:> exy)+  background exy  =  bgEqWith2  (eitherEq  ->>:> exy)                   ++ bgOrdWith2 (eitherOrd ->>:> exy)+                  ++ [ constant "Left"  (Left  ->: exy)+                     , constant "Right" (Right ->: exy) ]   instances exy  =  this exy $ instances (fromLeft  exy)                              . instances (fromRight exy) @@ -178,6 +186,8 @@   name xy  =  name (fst xy) ++ name (snd xy)   expr (x,y)  =  constant "," ((,) ->>: (x,y))               :$ expr x :$ expr y+  background xy  =  bgEqWith2  (pairEq  ->>:> xy)+                 ++ bgOrdWith2 (pairOrd ->>:> xy)   instances xy  =  this xy $ instances (fst xy)                            . instances (snd xy) @@ -187,6 +197,8 @@                where  (x,y,z) = xyz   expr (x,y,z)  =  constant ",," ((,,) ->>>: (x,y,z))                 :$ expr x :$ expr y :$ expr z+  background xyz  =  bgEqWith3  (tripleEq  ->>>:> xyz)+                  ++ bgOrdWith3 (tripleOrd ->>>:> xyz)   instances xyz  =  this xyz $ instances x . instances y . instances z                     where (x,y,z) = xyz @@ -196,6 +208,8 @@                 where (x,y,z,w) = xyzw   expr (x,y,z,w)  =  constant ",,," ((,,,) ->>>>: (x,y,z,w))                   :$ expr x :$ expr y :$ expr z :$ expr w+  background xyzw  =  bgEqWith4  (quadrupleEq  ->>>>:> xyzw)+                   ++ bgOrdWith4 (quadrupleOrd ->>>>:> xyzw)   instances xyzw  =  this xyzw $ instances x                                . instances y                                . instances z@@ -206,10 +220,10 @@   name xs  =  name (head xs) ++ "s"   expr (xs@[])      =  showConstant  ([]    -: xs)   expr (xs@(y:ys))  =  constant ":"  ((:) ->>: xs) :$ expr y :$ expr ys-  background xs  =  [ constant "length" (length -:> xs) ]-                 ++ [ constant "elem"      (elemBy (*==*) ->:> xs) | hasEq $ head xs ]-                 ++ bgEqWith1  (listEq  ->:> xs)+  background xs  =  bgEqWith1  (listEq  ->:> xs)                  ++ bgOrdWith1 (listOrd ->:> xs)+                 ++ [ constant "length" (length -:> xs) ]+                 ++ [ constant "elem"      (elemBy (*==*) ->:> xs) | hasEq $ head xs ]   instances xs  =  this xs $ instances (head xs)  instance Generalizable Ordering where@@ -245,11 +259,34 @@   x = argTy1of2 $ argTy1of2 makeEq   y = argTy1of2 . argTy1of2 $ argTy2of2 makeEq +bgEqWith3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d)+          => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)+          -> [Expr]+bgEqWith3 makeEq = takeWhile (\_ -> hasEq x && hasEq y && hasEq z)+                 [ constant "=="        (makeEq (*==*) (*==*) (*==*))+                 , constant "/=" (not .: makeEq (*==*) (*==*) (*==*)) ]+  where+  x = argTy1of2 $ argTy1of2 makeEq+  y = argTy1of2 . argTy1of2 $ argTy2of2 makeEq+  z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeEq++bgEqWith4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e)+          => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)+          -> [Expr]+bgEqWith4 makeEq = takeWhile (\_ -> hasEq x && hasEq y && hasEq z && hasEq w)+                 [ constant "=="        (makeEq (*==*) (*==*) (*==*) (*==*))+                 , constant "/=" (not .: makeEq (*==*) (*==*) (*==*) (*==*)) ]+  where+  x = argTy1of2 $ argTy1of2 makeEq+  y = argTy1of2 . argTy1of2 $ argTy2of2 makeEq+  z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeEq+  w = argTy1of2 . argTy1of2 . argTy2of2 . argTy2of2 $ argTy2of2 makeEq+ bgOrdWith1 :: (Generalizable a, Generalizable b)           => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr] bgOrdWith1 makeOrd = takeWhile (\_ -> hasOrd x)                    [ constant "<=" (             makeOrd (*<=*))-                   , constant "<"  (not .: flip (makeOrd (*<*))) ]+                   , constant "<"  (not .: flip (makeOrd (*<=*))) ]   where   x = argTy1of2 $ argTy1of2 makeOrd @@ -262,16 +299,39 @@   x = argTy1of2 $ argTy1of2 makeOrd   y = argTy1of2 . argTy1of2 $ argTy2of2 makeOrd +bgOrdWith3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d)+          => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)+          -> [Expr]+bgOrdWith3 makeOrd = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z)+                   [ constant "<="              (makeOrd (*<=*) (*<=*) (*<=*))+                   , constant "<"  (not .: flip (makeOrd (*<=*) (*<=*) (*<=*))) ]+  where+  x = argTy1of2 $ argTy1of2 makeOrd+  y = argTy1of2 . argTy1of2 $ argTy2of2 makeOrd+  z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeOrd++bgOrdWith4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e)+          => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)+          -> [Expr]+bgOrdWith4 makeOrd = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z && hasOrd w)+                   [ constant "<="              (makeOrd (*<=*) (*<=*) (*<=*) (*<=*))+                   , constant "<"  (not .: flip (makeOrd (*<=*) (*<=*) (*<=*) (*<=*))) ]+  where+  x = argTy1of2 $ argTy1of2 makeOrd+  y = argTy1of2 . argTy1of2 $ argTy2of2 makeOrd+  z = argTy1of2 . argTy1of2 . argTy2of2 $ argTy2of2 makeOrd+  w = argTy1of2 . argTy1of2 . argTy2of2 . argTy2of2 $ argTy2of2 makeOrd+ -- | Usage: @ins "x" (undefined :: Type)@ ins :: Generalizable a => a -> Instances-ins x = listable x +++ nameWith (name x) x +++ backgroundWith (background x) x+ins x = listable x ++ nameWith (name x) x ++ backgroundWith (background x) x  this :: Generalizable a      => a -> (Instances -> Instances) -> Instances -> Instances this x f is =   if isListable is (typeOf x)     then is-    else f (ins x +++ is)+    else f (ins x ++ is) -- TODO: change type to a -> [Instances -> Instances] -> Instances -> Instances  backgroundWith :: Typeable a => [Expr] -> a -> Instances@@ -280,9 +340,20 @@ getBackground :: Instances -> [Expr] getBackground is = concat [es | Instance "Background" _ es <- is] +getEqInstancesFromBackground :: Instances -> Instances+getEqInstancesFromBackground is =+  [Instance "Eq" (argumentTy $ typ eq) [eq, iq] | eq <- eqs, iq <- iqs, typ eq == typ iq]+  where+  eqs = [Constant "==" e | Constant "==" e <- bg]+  iqs = [Constant "/=" e | Constant "/=" e <- bg]+  bg = getBackground is+ backgroundOf :: Generalizable a => a -> [Expr] backgroundOf x = getBackground $ instances x [] +tBackground :: Testable a => a -> [Expr]+tBackground = getBackground . tinstances+ -- |  generalizes an expression by making it less defined, --    starting with smaller changes, then bigger changes: --@@ -319,6 +390,11 @@ data Option = MaxTests Int             | ExtraInstances Instances             | MaxConditionSize Int+            | MinFailures (Ratio Int)+            | MaxSpeculateSize (Maybe Int)+            | ConditionBound (Maybe Int)+            | ConstantBound (Maybe Int)+            | DepthBound (Maybe Int)   deriving (Show, Typeable) -- Typeable needed for GHC <= 7.8  data WithOption a = With@@ -328,14 +404,33 @@ type Options = [Option]  maxTests :: Testable a => a -> Int-maxTests p = head $ [m | MaxTests m <- options p] ++ [360]+maxTests p = head $ [m | MaxTests m <- options p] ++ [500]  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]+maxConditionSize p = head $ [m | MaxConditionSize m <- options p] ++ [4] +-- minimum number of failures for a conditional generalization+computeMinFailures :: Testable a => a -> Int+computeMinFailures p = max 2 $ m * numerator r `div` denominator r+  where+  r = head $ [r | MinFailures r <- options p] ++ [0]+  m = maxTests p++computeMaxSpeculateSize :: Testable a => a -> Maybe Int+computeMaxSpeculateSize p = head $ [b | MaxSpeculateSize b <- options p] ++ [Just 4]++computeConditionBound :: Testable a => a -> Maybe Int+computeConditionBound p = head $ [b | ConditionBound b <- options p] ++ [Nothing]++computeConstantBound :: Testable a => a -> Maybe Int+computeConstantBound p = head $ [b | ConstantBound b <- options p] ++ [Nothing]++computeDepthBound :: Testable a => a -> Maybe Int+computeDepthBound p = head $ [b | DepthBound b <- options p] ++ [Nothing]+ class Testable a where   resultiers :: a -> [[([Expr],Bool)]]   ($-|) :: a -> [Expr] -> Bool@@ -353,7 +448,7 @@   resultiers p = [[([],p)]]   p $-| []  =  p   p $-| _   =  error "($-|): too many arguments"-  tinstances _ = []+  tinstances _ = instances bool . instances int $ []  instance (Testable b, Generalizable a, Listable a) => Testable (a->b) where   resultiers p = concatMapT resultiersFor tiers@@ -390,13 +485,14 @@   where   is = tinstances p -generalizationsCEC :: Testable a => Int -> a -> [Expr] -> [(Expr,[Expr])]-generalizationsCEC n p es | maxConditionSize p <= 0 = []-generalizationsCEC n p es =+generalizationsCEC :: Testable a => a -> [Expr] -> [(Expr,[Expr])]+generalizationsCEC p es | maxConditionSize p <= 0 = []+generalizationsCEC p es =   [ (wc'', gs'')   | gs <- generalizations is es   , gs' <- vassignments gs-  , let wc = weakestCondition n p gs'+  , let thycs = theoryAndReprConds p+  , let wc = weakestCondition thycs p gs'   , wc /= constant "False" False   , wc /= constant "True"  True   , let (wc'':gs'') = canonicalizeWith is (wc:gs')@@ -452,71 +548,109 @@ 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-+-- | Given tiers of atomic expressions, generates tiers of expressions combined+--   by function application.  This is done blindly so redundant expressions+--   are generated: like x + y and y + x. 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-  ]+-- Generates expression schemas and a theory+theoryAndReprsFromPropAndAtoms :: Testable a => a -> [[Expr]] -> (Thy,[[Expr]])+theoryAndReprsFromPropAndAtoms p ess =+  theoryAndRepresentativesFromAtoms+    (maxConditionSize p) compareExpr (const True) (===) ess   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]+  -- the following uses of keep make Speculate run faster by defaulting to+  -- "these things are not equal" even in cases that they are.  Despite+  -- failing to detect some equalities, Speculte will still be useful as a+  -- generator of quasi-canonical expressions.+  e1 === e2 = keep e1 && keep e2 && equal is m e1 e2+  keep e = maybe True (\b -> length (consts e) <= b) constBound+        && maybe True (\b ->         depthE e  <= b) depthBound+        && maybe True (\b ->        lengthE e  <= b) (computeMaxSpeculateSize p)+-- NOTE: MaxSpeculateSize here should not be confused with the size+-- considering sizes of atoms (as per tier enumeration), this regards only the+-- size in number of symbols+  constBound = computeConstantBound p+  depthBound = computeDepthBound p+  is = fullInstances p+  m  = maxTests p+  compareExpr :: Expr -> Expr -> Ordering+  compareExpr = compareComplexityThen (lexicompareBy cmp)+  e1 `cmp` e2 | arity e1 == 0 && arity e2 /= 0 = LT+  e1 `cmp` e2 | arity e1 /= 0 && arity e2 == 0 = GT+  e1 `cmp` e2 = compareIndex (concat ess) e1 e2 <> e1 `compare` e2+-- NOTE: "concat $ atoms args" may be an infinite list.  This function assumes+-- that the symbols will appear on the list eventually for termination.  If I+-- am correct this ivariant is assured by the rest of the code. -weakestCondition :: Testable a => Int -> a -> [Expr] -> Expr-weakestCondition m p es = head $-  [ c | c <- candidateConditions p es-      , isCounterExampleUnder m p c es-      ] ++ [expr False]+-- tinstances including auto generated Eq instances (based on background)+fullInstances :: Testable a => a -> Instances+fullInstances p = is ++ getEqInstancesFromBackground is   where+  is = tinstances p -candidateConditions :: Testable a => a -> [Expr] -> [Expr]-candidateConditions p es = expr True :-  [ c-  | c <- candidateExpressions p es-  , typ c == boolTy-  , hasVar c-  , not (isAssignment c)-  , not (isAssignmentTest is (maxTests p) c)-  ]+-- Given a property, returns the atoms to be passed to Speculate+atoms :: Testable a => a -> [[Expr]]+atoms p = ([vs] \/)+        . foldr (\/) [esU]+        $ [ eval (error msg :: [[Expr]]) ess+          | Instance "Listable" _ [ess] <- is ]   where+  vs = sort . map holeOfTy . filter (isListable is) . nubMergeMap (typesIn . typ) $ esU+  esU = getBackground is+  msg = "canditateConditions: wrong type, not [[Expr]]"   is = tinstances p --- | Canditate expressions to appear in conditions-candidateExpressions :: Testable a => a -> [Expr] -> [Expr]-candidateExpressions p es = concat . take (maxConditionSize p) . expressionsTT-                         . foldr (\/) [vs ++ esU]-                         $ [ eval (error msg :: [[Expr]]) ess-                           | Instance "Listable" _ [ess] <- is ]+theoryAndReprExprs :: Testable a => a -> (Thy,[Expr])+theoryAndReprExprs p =+    (\(thy,ess) -> (thy, concat $ take (maxConditionSize p) ess))+  . theoryAndReprsFromPropAndAtoms p+  $ atoms p++theoryAndReprConds :: Testable a => a -> (Thy, [Expr])+theoryAndReprConds p = (thy, filter (\c -> typ c == boolTy) es)   where-  vs = [Var n t | (t,n) <- vars es]-  esU = concat [es | Instance "Background" _ es <- is]-  msg = "canditateConditions: wrong type, not [[Expr]]"+  (thy,es) = theoryAndReprExprs p++candidateConditions :: Testable a => (Thy,[Expr]) -> a -> [Expr] -> [Expr]+candidateConditions (thy,cs) p es = expr True :+  [ c | (c,_) <- classesFromSchemasAndVariables thy (uncurry (flip Var) <$> vars es) cs+      , hasVar c+      , not (isAssignment c)+      , not (isAssignmentTest is (maxTests p) c)+      ]+  where   is = tinstances p+-- 'expr True' is expected by the functions that call candidateConditions.  It+-- is always useful to check if a generalization without any conditions still+-- passes (that means we should skip as there is an already reported+-- unconditional generalization). -isCounterExampleUnder :: Testable a => Int -> a -> Expr -> [Expr] -> Bool-isCounterExampleUnder m p c es = and'+validConditions :: Testable a => (Thy,[Expr]) -> a -> [Expr] -> [(Expr,Int)]+validConditions thyes p es =+  [ (c,n) | c <- candidateConditions thyes p es+          , let (is,n) = isCounterExampleUnder p c es+          , is+          ] ++ [(expr False,0)]++weakestCondition :: Testable a => (Thy,[Expr]) -> a -> [Expr] -> Expr+weakestCondition thyes p es = fst+                            . maximumOn snd+                            . takeBound (computeConditionBound p)+                            $ validConditions thyes p es++isCounterExampleUnder :: Testable a => a -> Expr -> [Expr] -> (Bool, Int)+isCounterExampleUnder p c es = and'   [ not . errorToFalse $ p $-| es'-  | (bs,es') <- take m $ groundsAndBinds (tinstances p) es+  | (bs,es') <- take (maxTests p) $ groundsAndBinds (tinstances p) es   , errorToFalse $ eval False (c `assigning` bs)   ]   where-  and' ps = and ps && length ps > m `div` 12 -- poor workaround+  and' ps = let len = length ps+            in  (and ps && len > computeMinFailures p && len > 0, len)  isVar :: Expr -> Bool isVar (Var _ _) = True@@ -524,8 +658,7 @@  fromBackgroundOf :: (Generalizable a, Typeable b) => String -> a -> Maybe b fromBackgroundOf nm = listToMaybe-                    . catMaybes-                    . map evaluate+                    . mapMaybe evaluate                     . filter (`isConstantNamed` nm)                     . background
src/Test/Extrapolate/Derive.hs view
@@ -26,6 +26,7 @@ import Language.Haskell.TH import Test.LeanCheck.Basic import Test.LeanCheck.Utils.TypeBinding+import Test.LeanCheck.Derive (deriveListableIfNeeded) import Control.Monad (unless, liftM, liftM2, filterM) import Data.List (delete,nub,sort) import Data.Char (toLower)@@ -76,9 +77,10 @@         (reportWarning $ "Instance Generalizable " ++ show t                       ++ " already exists, skipping derivation")       return []-    else if cascade-           then reallyDeriveGeneralizableCascading t-           else reallyDeriveGeneralizable t+    else+      if cascade+        then liftM2 (++) (deriveListableCascading t) (reallyDeriveGeneralizableCascading t)+        else liftM2 (++) (deriveListableIfNeeded t)  (reallyDeriveGeneralizable t)  reallyDeriveGeneralizable :: Name -> DecsQ reallyDeriveGeneralizable t = do
src/Test/Extrapolate/IO.hs view
@@ -17,6 +17,11 @@   , withInstances   , withBackground   , withConditionSize+  , minFailures+  , maxSpeculateSize+  , conditionBound+  , constantBound+  , depthBound   ) where @@ -25,8 +30,10 @@ #endif  import Test.Extrapolate.Core-import Data.Maybe (listToMaybe, mapMaybe)+import Data.Maybe (listToMaybe, mapMaybe, fromMaybe) import Data.List (find, intercalate)+import Data.Ratio (Ratio)+import Control.Monad import Control.Exception as E (SomeException, catch, evaluate)  -- | Use @`for`@ to configure the number of tests performed by @check@.@@ -61,6 +68,37 @@ withConditionSize :: Testable a => (WithOption a -> b) -> Int -> a -> b check `withConditionSize` s  =   \p -> check $ p `With` MaxConditionSize s +-- | Use @`minFailures`@ to configure the minimum number of failures for a+--   conditional generalization in function of the maximum number of tests.+--+-- To set that conditional generalizations should fail for 10% of cases:+-- > check `minFailures` (`div` 10) $ prop+--+-- To set that conditional generalizations should fail for 5% of cases:+-- > check `minFailures` (`div` 20) $ prop+minFailures :: Testable a => (WithOption a -> b) -> Ratio Int -> a -> b+check `minFailures` s =  \p -> check $ p `With` MinFailures s++conditionBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b+check `conditionBound` mi =  \p -> check $ p `With` ConditionBound mi++maxSpeculateSize :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b+check `maxSpeculateSize` mi =  \p -> check $ p `With` MaxSpeculateSize mi++-- | Configures a bound on the number of constants allowed in expressions that+--   are considered when testing for equality in Speculate.+--+-- Defaults to 2.+constantBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b+check `constantBound` mi =  \p -> check $ p `With` ConstantBound mi++-- | Configures a bound on the depth of expressions that are considered+--   when testing for equality in Speculate.+--+-- Default to 3.+depthBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b+check `depthBound` mi =  \p -> check $ p `With` DepthBound mi+ -- | Checks a property printing results on 'stdout' -- -- > > check $ \xs -> sort (sort xs) == sort (xs::[Int])@@ -73,7 +111,7 @@ -- > Generalization: -- > [] (x:x:_) check :: Testable a => a -> IO ()-check p = checkResult p >> return ()+check = void . checkResult  -- | Check a property --   printing results on 'stdout' and@@ -97,7 +135,7 @@   deriving (Eq, Show)  resultsIO :: Testable a => Int -> a -> IO [Result]-resultsIO n = sequence . zipWith torio [1..] . take n . results+resultsIO n = zipWithM torio [1..] . take n . results   where     tor i (_,True) = OK i     tor i (as,False) = Falsified i as@@ -108,7 +146,7 @@ resultIO :: Testable a => Int -> a -> IO (Result, [[Expr]]) resultIO n p = do   rs <- resultsIO n p-  return ( maybe (last rs) id $ find isFailure rs+  return ( fromMaybe (last rs) $ find isFailure rs          , mapMaybe ce rs )   where   isFailure (OK _) = False@@ -131,7 +169,7 @@        []     -> ""        (es:_) -> "Generalization:\n"               ++ showCE es ++ "\n\n"-  ++ case generalizationsCEC m p es of+  ++ case generalizationsCEC p es of        []         -> ""        (es:_) -> "Conditional Generalization:\n"               ++ showCCE es ++ "\n\n"
src/Test/Extrapolate/Utils.hs view
@@ -24,11 +24,25 @@   , listEq,   listOrd   , maybeEq,  maybeOrd   , eitherEq, eitherOrd+  , pairEq,   pairOrd+  , tripleEq, tripleOrd+  , quadrupleEq, quadrupleOrd+  , minimumOn+  , maximumOn+  , takeBound+  , nubMergeMap+  , typesIn+  , argumentTy+  , resultTy+  , discard+  , compareIndex   , (.:)   ) where  import Data.Function (on)+import Data.List (minimumBy, maximumBy, nub, elemIndex)+import Data.Typeable  nubMergeBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a] nubMergeBy cmp (x:xs) (y:ys) = case x `cmp` y of@@ -104,5 +118,113 @@ eitherOrd _    _ (Left  _) (Right _) = True eitherOrd _    _ (Right _) (Left  _) = False +pairEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a,b) -> (a,b) -> Bool+pairEq (==.) (.==) (x1,y1) (x2,y2) = x1 ==. x2 && y1 .== y2++pairOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a,b) -> (a,b) -> Bool+pairOrd (<=.) (.<=) (x1,y1) (x2,y2) = x1 <. x2+                                   || x1 ==. x2 && y1 .<= y2+  where+  x <.  y = x <=. y && not (y <=. x)+  x ==. y = x <=. y &&      y <=. x++tripleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool)+         -> (a,b,c) -> (a,b,c) -> Bool+tripleEq (==..) (.==.) (..==) (x1,y1,z1) (x2,y2,z2) =+  x1 ==.. x2 && y1 .==. y2 && z1 ..== z2++tripleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool)+          -> (a,b,c) -> (a,b,c) -> Bool+tripleOrd (<=..) (.<=.) (..<=) (x1,y1,z1) (x2,y2,z2) =+  x1 <.. x2 || x1 ==.. x2 && pairOrd (.<=.) (..<=) (y1,z1) (y2,z2)+  where+  x <..  y = x <=.. y && not (y <=.. x)+  x ==.. y = x <=.. y &&      y <=.. x++quadrupleEq :: (a->a->Bool) -> (b->b->Bool) -> (c->c->Bool) -> (d->d->Bool)+            -> (a,b,c,d) -> (a,b,c,d) -> Bool+quadrupleEq (==...) (.==..) (..==.) (...==) (x1,y1,z1,w1) (x2,y2,z2,w2) =+  x1 ==... x2 && y1 .==.. y2 && z1 ..==. z2 && w1 ...== w2++quadrupleOrd :: (a->a->Bool) -> (b->b->Bool) -> (c->c->Bool) -> (d->d->Bool)+             -> (a,b,c,d) -> (a,b,c,d) -> Bool+quadrupleOrd (<=...) (.<=..) (..<=.) (...<=) (x1,y1,z1,w1) (x2,y2,z2,w2) =+  x1 <... x2 || x1 ==... x2 && tripleOrd (.<=..) (..<=.) (...<=) (y1,z1,w1) (y2,z2,w2)+  where+  x <...  y = x <=... y && not (y <=... x)+  x ==... y = x <=... y &&      y <=... x++minimumOn :: Ord b => (a -> b) -> [a] -> a+minimumOn f = minimumBy (compare `on` f)++-- left/head-biased, which is different from Prelude's maximum+maximumOn :: Ord b => (a -> b) -> [a] -> a+maximumOn f []     = error "maximumOn: empty list"+maximumOn f [x]    = x+maximumOn f (x:xs) = let y = maximumOn f xs+                     in if f x < f y+                          then y+                          else x++takeBound :: Maybe Int -> [a] -> [a]+takeBound Nothing  xs  =  xs+takeBound (Just n) xs  =  take n xs++nubMerges :: Ord a => [[a]] -> [a]+nubMerges = nubMergesBy compare++nubMergesBy :: Ord a => (a -> a -> Ordering) -> [[a]] -> [a]+nubMergesBy cmp [] = []+nubMergesBy cmp [xs] = xs+nubMergesBy cmp xss = nubMergeBy cmp (nubMerges yss) (nubMerges zss)+  where+  (yss,zss) = splitHalf xss+  splitHalf xs = splitAt (length xs `div` 2) xs++nubMergeMap :: Ord b => (a -> [b]) -> [a] -> [b]+nubMergeMap f = nubMerges . map f++funTyCon :: TyCon+funTyCon = typeRepTyCon $ typeOf (undefined :: () -> ())++isFunTy :: TypeRep -> Bool+isFunTy t =+  case splitTyConApp t of+    (con,[_,_]) | con == funTyCon -> True+    _ -> False++-- | For a given type, return all *-kinded types.+--   (all non-function types)+--+-- > typesIn (typeOf (undefined :: (Int -> Int) -> Int -> Bool))+-- >   == [Bool,Int]+typesIn :: TypeRep -> [TypeRep]+typesIn t+  | isFunTy t = typesIn (argumentTy t)+            +++ typesIn (resultTy   t)+  | otherwise = [t]++unFunTy :: TypeRep -> (TypeRep,TypeRep)+unFunTy t+  | isFunTy t = let (f,[a,b]) = splitTyConApp t in (a,b)+  | otherwise = error $ "error (unFunTy): `" ++ show t ++ "` is not a function type"++argumentTy :: TypeRep -> TypeRep+argumentTy = fst . unFunTy++resultTy :: TypeRep -> TypeRep+resultTy = snd . unFunTy++discard :: (a -> Bool) -> [a] -> [a]+discard p = filter (not . p)+ (.:) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d) (.:) = (.) . (.)++compareIndex :: Eq a => [a] -> a -> a -> Ordering+compareIndex xs x y =+  case (elemIndex x xs, elemIndex y xs) of+    (Just  i, Just  j) -> i `compare` j+    (Nothing, Just  _) -> GT+    (Just  _, Nothing) -> LT+    _                  -> EQ
tests/Test.hs view
@@ -12,19 +12,27 @@    , (-:-), ll, llb, llmi +  , (-+-)+   , _i, xx, yy   , _is, xxs, yys+  , _b, pp, qq   , _mi, mxx   , zero, one    , false, true+  , not'+  , notE -  , elem'+  , elem', length'+  , elemE, lengthE    , nothing, nothingBool, just    , comma +  , operatorE+   , (-==-)   , (-/=-)   , (-<-)@@ -37,6 +45,7 @@   , instancesOK   , namesOK, sameNamesIn, namesIn   , tiersOK, sameTiersIn, tiersIn+  , bgEqOK, bgEqOrdOK    , subset, bgSubset @@ -52,10 +61,12 @@ import Data.Typeable (typeOf) import Data.List (isPrefixOf, sort) import Data.Maybe (fromMaybe)+import Test.Speculate.Reason+import Test.Speculate.Reason.Order  import Test.Extrapolate import Test.Extrapolate.Utils-import Test.Extrapolate.Core hiding (false, true)+import Test.Extrapolate.Core hiding (false, true, lengthE) import qualified Test.Extrapolate.Core as Core import Test.LeanCheck.Utils.Operators @@ -111,6 +122,11 @@ _mi  =  var ""   (mayb int) mxx  =  var "mx" (mayb int) +_b, pp, qq :: Expr+_b  =  var ""  bool+pp  =  var "p" bool+qq  =  var "q" bool+ zero :: Expr zero  =  expr (0 :: Int) @@ -137,9 +153,21 @@  elem' :: Expr -> Expr -> Expr elem' x xs  =  elemE :$ x :$ xs-  where-  elemE  =  constant "elem" (elem :: Int -> [Int] -> Bool) +elemE :: Expr+elemE  =  constant "elem" (elem :: Int -> [Int] -> Bool)++length' :: Expr -> Expr+length' xs  =  lengthE :$ xs++lengthE  =  constant "length" (length :: [Int] -> Int)++not' :: Expr -> Expr+not' p  =  notE :$ p++notE :: Expr+notE  =  constant "not" not+ just :: Expr -> Expr just x  =  justE :$ x   where@@ -164,6 +192,16 @@   commaEbi  =  constant "," ((,) ->>: (bool,int))   commaEbb  =  constant "," ((,) ->>: (bool,bool)) +(-+-) :: Expr -> Expr -> Expr+e1 -+- e2 = plusE :$ e1 :$ e2+infixl 6 -+-++plusE :: Expr+plusE = constant "+" ((+) :: Int -> Int -> Int)++operatorE :: Expr -> Expr+operatorE ((opE :$ _) :$ _) = opE+ (-==-) :: Expr -> Expr -> Expr e1 -==- e2 =   fromMaybe (error $ "(-==-): cannot equate " ++ show e1 ++ " and " ++ show e2)@@ -246,6 +284,14 @@           && x `sameTiersIn` ((),x,())           && x `sameTiersIn` ((),(),x) +bgEqOK :: (Eq a, Generalizable a) => a -> a -> Bool+bgEqOK = (*==*) ==== (==)+    &&&& (*/=*) ==== (/=)++bgEqOrdOK :: (Eq a, Ord a, Generalizable a) => a -> a -> Bool+bgEqOrdOK = bgEqOK &&&& (*<=*) ==== (<=)+                   &&&& (*<*)  ==== (<)+ sameTiersIn :: (Eq a, Generalizable a, Generalizable b) => a -> b -> Bool x `sameTiersIn` cx = isListable (instances cx []) (typeOf x)                   && (tiers -: [[x]]) =| 6 |= tiersIn cx@@ -274,3 +320,30 @@ isSubsequenceOf (x:xs) (y:ys)   | x == y    =    xs  `isSubsequenceOf` ys   | otherwise = (x:xs) `isSubsequenceOf` ys++-- Quick and Dirty!+instance Show Thy where+  show Thy { rules = rs+           , equations = eqs+           , canReduceTo = (->-)+           , closureLimit = cl+           , keepE = keep+           }+    = "Thy { rules = "+   ++ drop 14 (indent 14 . listLines $ map showEquation rs)+   ++ "    , equations = "+   ++ drop 18 (indent 18 . listLines $ map showEquation eqs)+   ++ "    , canReduceTo = " ++ showCanReduceTo (->-) ++ "\n"+   ++ "    , closureLimit = " ++ show cl ++ "\n"+   ++ "    , keepE = " ++ showKeepE keep ++ "\n"+   ++ "    }"+    where+    showEquation (e1,e2) = showExpr e1 ++ " == " ++ showExpr e2+    listLines [] = "[]"+    listLines ss = '[':(tail . unlines $ map (", " ++) ss) ++ "]"+    showCanReduceTo (->-) = "(??)"+    showKeepE keep = "\\e -> ??"+    indent :: Int -> String -> String+    indent n = unlines . map (replicate n ' ' ++) . lines++
tests/test-derive.hs view
@@ -98,25 +98,9 @@ dict = undefined  --- TODO: auto-derive Listable from deriveGeneralizable? deriveListable ''List deriveListable ''Perhaps deriveListable ''Ship-deriveListable ''Arrangement--deriveListable ''NonEmptyList--deriveListable ''Mutual-deriveListable ''Shared--deriveListable ''Tree-deriveListable ''Leafy--deriveListable ''Dict--deriveListable ''Data-deriveListable ''EqData-deriveListable ''OrdData   deriveGeneralizable ''List
tests/test-extrapolate.hs view
@@ -99,27 +99,27 @@                                 ]    , background (mayb int)-    == [ constant "Just" (Just ->: mayb int)-       , constant "=="   ((==) -:> mayb int)+    == [ constant "=="   ((==) -:> mayb int)        , constant "/="   ((/=) -:> mayb int)        , constant "<="   ((<=) -:> mayb int)-       , constant "<"    ((<)  -:> mayb int) ]+       , constant "<"    ((<)  -:> mayb int)+       , constant "Just" (Just ->: mayb int) ]    , background (eith int char)-    == [ constant "Left"  (Left  ->: eith int char)-       , constant "Right" (Right ->: eith int char)-       , constant "=="    ((==)  -:> eith int char)+    == [ constant "=="    ((==)  -:> eith int char)        , constant "/="    ((/=)  -:> eith int char)        , constant "<="    ((<=)  -:> eith int char)-       , constant "<"     ((<)   -:> eith int char) ]+       , constant "<"     ((<)   -:> eith int char)+       , constant "Left"  (Left  ->: eith int char)+       , constant "Right" (Right ->: eith int char) ]    , background [int]-    == [ constant "length" (length -:> [int])-       , constant "elem"   (elem  ->:> [int])-       , constant "=="     ((==)   -:> [int])+    == [ constant "=="     ((==)   -:> [int])        , constant "/="     ((/=)   -:> [int])        , constant "<="     ((<=)   -:> [int])-       , constant "<"      ((<)    -:> [int]) ]+       , constant "<"      ((<)    -:> [int])+       , constant "length" (length -:> [int])+       , constant "elem"   (elem  ->:> [int]) ]    , background (mayb nord)     == [ constant "Just" (Just ->: mayb nord) ]@@ -186,56 +186,77 @@        , zero -:- zero -:- _is        ] -  {- TODO: fix the following tests-  , candidateConditions (([int] >- bool) `With` MaxConditionSize 3) [xxs]-    == [ true, elem' zero xxs ]+--, holds n $ bgEqOrdOK -:> () -- no Eq or Ord instance on background+  , holds n $ bgEqOrdOK -:> int+  , holds n $ bgEqOK    -:> bool+  , holds n $ bgEqOrdOK -:> char+  , holds n $ bgEqOrdOK -:> integer+  , holds n $ bgEqOrdOK -:> ordering -  , candidateConditions (([int] >- bool) `With` MaxConditionSize 3) [xx -:- xxs]-    =$ sort-    $= [ true-       , elem' zero xxs-       , elem' xx ll-       , elem' xx xxs-       , zero -/=- xx-       , xx   -/=- zero-       , xx   -/=- xx-       , zero -<- xx-       , xx   -<- zero-       , xx   -<- xx-       , zero -<=- xx-       , xx   -<=- zero-       , xx   -<=- xx-       ]-  -}+  , holds n $ bgEqOrdOK -:> (int,int)+  , holds n $ bgEqOK    -:> (int,bool)+  , holds n $ bgEqOK    -:> (bool,int)+  , holds n $ bgEqOK    -:> (bool,bool)+  , holds n $ bgEqOrdOK -:> (char,ordering) -  , holds n $ (*==*) ==== (==) -:> int-  , holds n $ (*==*) ==== (==) -:> char-  , holds n $ (*==*) ==== (==) -:> [int]-  , holds n $ (*==*) ==== (==) -:> mayb int-  , holds n $ (*==*) ==== (==) -:> mayb char-  , holds n $ (*==*) ==== (==) -:> eith int char+  , holds n $ bgEqOrdOK -:> (int,int,int)+  , holds n $ bgEqOK    -:> (int,int,bool)+  , holds n $ bgEqOK    -:> (int,bool,int)+  , holds n $ bgEqOK    -:> (int,bool,bool)+  , holds n $ bgEqOK    -:> (bool,int,int)+  , holds n $ bgEqOK    -:> (bool,int,bool)+  , holds n $ bgEqOK    -:> (bool,bool,int)+  , holds n $ bgEqOK    -:> (bool,bool,bool)+  , holds n $ bgEqOrdOK -:> (integer,char,ordering) -  , holds n $ (*/=*) ==== (/=) -:> int-  , holds n $ (*/=*) ==== (/=) -:> char-  , holds n $ (*/=*) ==== (/=) -:> [int]-  , holds n $ (*/=*) ==== (/=) -:> mayb int-  , holds n $ (*/=*) ==== (/=) -:> mayb char-  , holds n $ (*/=*) ==== (/=) -:> eith int char+  , holds n $ bgEqOrdOK -:> (int,int,int,int)+  , holds n $ bgEqOrdOK -:> (integer,char,ordering,int)+  , holds n $ bgEqOK    -:> (bool,bool,bool,bool) -  , holds n $ (*<=*) ==== (<=) -:> int-  , holds n $ (*<=*) ==== (<=) -:> char---, holds n $ (*<=*) ==== (<=) -:> [int]---, holds n $ (*<=*) ==== (<=) -:> mayb int---, holds n $ (*<=*) ==== (<=) -:> mayb char---, holds n $ (*<=*) ==== (<=) -:> eith int char+  , holds n $ bgEqOrdOK -:> [int]+  , holds n $ bgEqOK    -:> [bool]+  , holds n $ bgEqOrdOK -:> [char]+  , holds n $ bgEqOrdOK -:> [integer] -  , holds n $ (*<*) ==== (<) -:> int-  , holds n $ (*<*) ==== (<) -:> char---, holds n $ (*<*) ==== (<) -:> [int]---, holds n $ (*<*) ==== (<) -:> mayb int---, holds n $ (*<*) ==== (<) -:> mayb char---, holds n $ (*<*) ==== (<) -:> eith int char+  , holds n $ bgEqOrdOK -:> mayb int+  , holds n $ bgEqOK    -:> mayb bool+  , holds n $ bgEqOrdOK -:> mayb char++  , holds n $ bgEqOrdOK -:> eith int int+  , holds n $ bgEqOK    -:> eith int bool+  , holds n $ bgEqOK    -:> eith bool int+  , holds n $ bgEqOK    -:> eith bool bool+  , holds n $ bgEqOrdOK -:> eith char ordering++  , tinstancesUnrepeated $ bool+  , tinstancesUnrepeated $ bool >- bool+  , tinstancesUnrepeated $ int  >- bool+  , tinstancesUnrepeated $ char >- bool+  , tinstancesUnrepeated $ bool >- bool >- bool+  , tinstancesUnrepeated $ int  >- int  >- bool+  , tinstancesUnrepeated $ char >- char >- bool+  , tinstancesUnrepeated $ [bool] >- bool+  , tinstancesUnrepeated $ [int]  >- bool+  , tinstancesUnrepeated $ [char] >- bool+  , tinstancesUnrepeated $ mayb bool >- bool+  , tinstancesUnrepeated $ mayb int  >- bool+  , tinstancesUnrepeated $ mayb char >- bool+  , tinstancesUnrepeated $ eith bool bool >- bool+  , tinstancesUnrepeated $ eith int  int  >- bool+  , tinstancesUnrepeated $ eith char char >- bool+  , tinstancesUnrepeated $ eith char ()   >- bool+  , tinstancesUnrepeated $ ([bool],[bool]) >- bool+  , tinstancesUnrepeated $ ([int], [int])  >- bool+  , tinstancesUnrepeated $ ([char],[char]) >- bool+  , tinstancesUnrepeated $ eith [bool] [bool] >- ([bool],[bool]) >- bool   ]++tinstancesUnrepeated :: Testable a => a -> Bool+tinstancesUnrepeated p = nub is == is+                      && nub is' == is'+  where+  is = tinstances p+  is' = fullInstances p  listBackgroundOK :: Generalizable a => a -> Bool listBackgroundOK x = backgroundListOf x `subset` backgroundOf [x]
+ tests/test-step-by-step.hs view
@@ -0,0 +1,121 @@+-- Copyright (c) 2017 Rudy Matela.+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Test+import Data.List (nub)++main :: IO ()+main = mainTest tests 10000++tests :: Int -> [Bool]+tests n =+  [ True++  , tBackground prop+    == [ operatorE (_is -==- _is)+       , operatorE (_is -/=- _is)+       , operatorE (_is -<=- _is)+       , operatorE (_is -<-  _is)+       , lengthE+       , elemE++       , operatorE (_b -==- _b)+       , operatorE (_b -/=- _b)+       , notE++       , operatorE (_i -==- _i)+       , operatorE (_i -/=- _i)+       , operatorE (_i -<-  _i)+       , operatorE (_i -<=- _i) ]++  , concat (take 2 $ atoms prop)+    == [ _b+       , _i+       , _is+       , ll+       , false+       , true+       , zero++       , operatorE (_is -==- _is)+       , operatorE (_is -/=- _is)+       , operatorE (_is -<=- _is)+       , operatorE (_is -<-  _is)+       , lengthE+       , elemE++       , operatorE (_b -==- _b)+       , operatorE (_b -/=- _b)+       , notE++       , operatorE (_i -==- _i)+       , operatorE (_i -/=- _i)+       , operatorE (_i -<-  _i)+       , operatorE (_i -<=- _i)++       , showConstant [0::Int]+       , one+       ]++  , snd thyes+    == [ _b+       , false+       , true+       , not' _b++       , _is  -==- _is+       , _is  -==- ll+       , _is  -/=- _is+       , _is  -/=- ll+       , _is  -<=- _is+       , _is  -<-  _is+       , elem' _i _is+       , elem' zero _is++       , _b   -==- _b+       , _b   -/=- _b++       , _i   -==- _i+       , _i   -==- zero+       , _i   -/=- _i+       , _i   -/=- zero+       , _i   -<-  _i+       , _i   -<-  zero+       , zero -<-  _i+       , _i   -<=- _i+       , _i   -<=- zero+       , zero -<=- _i+       ]++  , candidateConditions thyes prop [xxs]+    == [ true+       , xxs -/=- ll+       , elem' zero xxs+       ]++  , validConditions thyes prop [xxs]+    == [(false, 0)]++  , candidateConditions thyes prop [xx -:- xxs]+    == [ true+       , xxs -/=- ll+       , elem' xx xxs+       , elem' zero xxs+       , xx -/=- zero+       , xx -<- zero+       , zero -<- xx+       , xx -<=- zero+       , zero -<=- xx+       ]++  , validConditions thyes prop [xx -:- xxs]+    =$ map fst+    $= [ (elem' xx xxs, 323) -- TODO: why is this 317 on GHC 8.0?+       , (false, 0)+       ]+  ]++thyes  =  theoryAndReprConds prop+prop   =  prop_nubid `With` MaxConditionSize 3 `With` ConstantBound Nothing++prop_nubid :: [Int] -> Bool+prop_nubid xs  =  nub xs == xs
tests/test-utils.hs view
@@ -51,4 +51,78 @@   , holds n $ eitherOrd (<=) (<=) ==== (<=) -:> eith int bool   , holds n $ eitherOrd (<=) (<=) ==== (<=) -:> eith bool int   , holds n $ eitherOrd (<=) (<=) ==== (<=) -:> eith bool bool++  , holds n $ pairEq (==) (==) ==== (==) -:> ((),())+  , holds n $ pairEq (==) (==) ==== (==) -:> (int,int)+  , holds n $ pairEq (==) (==) ==== (==) -:> (int,bool)+  , holds n $ pairEq (==) (==) ==== (==) -:> (bool,int)+  , holds n $ pairEq (==) (==) ==== (==) -:> (bool,bool)++  , holds n $ pairOrd (<=) (<=) ==== (<=) -:> ((),())+  , holds n $ pairOrd (<=) (<=) ==== (<=) -:> (int,int)+  , holds n $ pairOrd (<=) (<=) ==== (<=) -:> (int,bool)+  , holds n $ pairOrd (<=) (<=) ==== (<=) -:> (bool,int)+  , holds n $ pairOrd (<=) (<=) ==== (<=) -:> (bool,bool)++  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> ((),(),())+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (int,int,int)+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (int,int,bool)+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (int,bool,int)+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (int,bool,bool)+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (bool,int,int)+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (bool,int,bool)+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (bool,bool,int)+  , holds n $ tripleEq (==) (==) (==) ==== (==) -:> (bool,bool,bool)++  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> ((),(),())+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (int,int,int)+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (int,int,bool)+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (int,bool,int)+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (int,bool,bool)+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (bool,int,int)+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (bool,int,bool)+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (bool,bool,int)+  , holds n $ tripleOrd (<=) (<=) (<=) ==== (<=) -:> (bool,bool,bool)++  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> ((),(),(),())+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,int,int,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,int,int,bool)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,int,bool,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,int,bool,bool)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,bool,int,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,bool,int,bool)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,bool,bool,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (int,bool,bool,bool)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,int,int,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,int,int,bool)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,int,bool,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,int,bool,bool)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,bool,int,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,bool,int,bool)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,bool,bool,int)+  , holds n $ quadrupleEq (==) (==) (==) (==) ==== (==) -:> (bool,bool,bool,bool)++  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> ((),(),(),())+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,int,int,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,int,int,bool)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,int,bool,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,int,bool,bool)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,bool,int,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,bool,int,bool)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,bool,bool,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (int,bool,bool,bool)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,int,int,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,int,int,bool)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,int,bool,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,int,bool,bool)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,bool,int,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,bool,int,bool)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,bool,bool,int)+  , holds n $ quadrupleOrd (<=) (<=) (<=) (<=) ==== (<=) -:> (bool,bool,bool,bool)++  , minimumOn fst [(1,6),(2,5),(3,4)] == (1,6)+  , minimumOn snd [(1,6),(2,5),(3,4)] == (3,4)+  , maximumOn fst [(1,6),(2,5),(3,4)] == (3,4)+  , maximumOn snd [(1,6),(2,5),(3,4)] == (1,6)+  , maximumOn fst [(1,6),(1,5),(1,4)] == (1,6)   ]