diff --git a/TODO.md b/TODO.md --- a/TODO.md +++ b/TODO.md @@ -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. diff --git a/extrapolate.cabal b/extrapolate.cabal --- a/extrapolate.cabal +++ b/extrapolate.cabal @@ -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 diff --git a/src/Test/Extrapolate.hs b/src/Test/Extrapolate.hs --- a/src/Test/Extrapolate.hs +++ b/src/Test/Extrapolate.hs @@ -40,6 +40,7 @@ , for , withBackground , withConditionSize + , minFailures -- * Generalizable types , Generalizable (..) diff --git a/src/Test/Extrapolate/Core.hs b/src/Test/Extrapolate/Core.hs --- a/src/Test/Extrapolate/Core.hs +++ b/src/Test/Extrapolate/Core.hs @@ -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 diff --git a/src/Test/Extrapolate/Derive.hs b/src/Test/Extrapolate/Derive.hs --- a/src/Test/Extrapolate/Derive.hs +++ b/src/Test/Extrapolate/Derive.hs @@ -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 diff --git a/src/Test/Extrapolate/IO.hs b/src/Test/Extrapolate/IO.hs --- a/src/Test/Extrapolate/IO.hs +++ b/src/Test/Extrapolate/IO.hs @@ -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" diff --git a/src/Test/Extrapolate/Utils.hs b/src/Test/Extrapolate/Utils.hs --- a/src/Test/Extrapolate/Utils.hs +++ b/src/Test/Extrapolate/Utils.hs @@ -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 diff --git a/tests/Test.hs b/tests/Test.hs --- a/tests/Test.hs +++ b/tests/Test.hs @@ -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 + + diff --git a/tests/test-derive.hs b/tests/test-derive.hs --- a/tests/test-derive.hs +++ b/tests/test-derive.hs @@ -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 diff --git a/tests/test-extrapolate.hs b/tests/test-extrapolate.hs --- a/tests/test-extrapolate.hs +++ b/tests/test-extrapolate.hs @@ -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] diff --git a/tests/test-step-by-step.hs b/tests/test-step-by-step.hs new file mode 100644 --- /dev/null +++ b/tests/test-step-by-step.hs @@ -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 diff --git a/tests/test-utils.hs b/tests/test-utils.hs --- a/tests/test-utils.hs +++ b/tests/test-utils.hs @@ -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) ]