From 3afbf3ee8272fa5475619a90cf25582a6e5e2139 Mon Sep 17 00:00:00 2001 From: Lee Pike Date: Fri, 20 Apr 2012 10:12:13 -0700 Subject: [PATCH] Implemented recursive generalization. Isn't so effective, as QC keeps generating new concrete terms for ungeneralized terms. --- TODO.md | 5 +++- examples/Div0.hs | 5 +++- src/Test/SmartCheck/Common.hs | 9 +++++-- src/Test/SmartCheck/DataToTree.hs | 5 ---- src/Test/SmartCheck/Extrapolate.hs | 41 ++++++++++++++++++++++++------ src/Test/SmartCheck/Types.hs | 21 ++------------- 6 files changed, 50 insertions(+), 36 deletions(-) diff --git a/TODO.md b/TODO.md index 3a2a73b..3fad001 100644 --- a/TODO.md +++ b/TODO.md @@ -15,10 +15,13 @@ TODO also fails the property, replace the original value with the hole. * Use instances so I can pass anything that can be turned into a property to - reduce. + reduce, like in QuickCheck. * Make sure I can use extrapolation on its own, without reduce. +* Testing with arguments to value constructors omitted in the SubTypes + instances. + Done ----------------------------------------------- * ~~Rename examples/Test to examples/MutRecData~~ diff --git a/examples/Div0.hs b/examples/Div0.hs index 8b780ab..1a6558d 100644 --- a/examples/Div0.hs +++ b/examples/Div0.hs @@ -59,11 +59,14 @@ div1 m = divSubTerms m ==> eval m /= Nothing divSubTerms (A m0 m1) = divSubTerms m0 && divSubTerms m1 divSubTerms (D m0 m1) = divSubTerms m0 && divSubTerms m1 +-- div0 (A _ _) = property False +-- div0 _ = property True + main :: IO () main = do result <- smartRun args div1 extrapolate args result div1 - where args = stdArgs { maxSuccess = 1000 + where args = stdArgs { maxSuccess = 100 , maxSize = 20 } --------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Common.hs b/src/Test/SmartCheck/Common.hs index f860d8c..8510aaa 100644 --- a/src/Test/SmartCheck/Common.hs +++ b/src/Test/SmartCheck/Common.hs @@ -3,6 +3,7 @@ module Test.SmartCheck.Common , iterateArb , resultify , smartPrtLn + , replace ) where import Test.SmartCheck.Types @@ -46,7 +47,7 @@ iterateArb d idx tries sz prop = case getAtIdx d idx of Nothing -> return Nothing Just v -> do rnds <- mkVals v - let res = catMaybes $ map repl rnds + let res = catMaybes $ map (replace d idx) rnds -- Catch errors when (length res /= length rnds) (error "iterateArb") findM goodResult res @@ -72,10 +73,14 @@ iterateArb d idx tries sz prop = rnds <- samples v tries sz return $ map subT rnds - repl SubT { unSubT = v } = replaceAtIdx d idx v +--------------------------------------------------------------------------------- + +replace :: SubTypes a => a -> Idx -> SubT -> Maybe a +replace d idx SubT { unSubT = v } = replaceAtIdx d idx v --------------------------------------------------------------------------------- +-- | Make a QuickCheck Result by applying a property function to a value. resultify :: (a -> Q.Property) -> a -> IO Q.Result resultify prop a = do Q.MkRose r _ <- res fs diff --git a/src/Test/SmartCheck/DataToTree.hs b/src/Test/SmartCheck/DataToTree.hs index b1b8b4a..5d08e55 100644 --- a/src/Test/SmartCheck/DataToTree.hs +++ b/src/Test/SmartCheck/DataToTree.hs @@ -120,11 +120,6 @@ sub forest idx a = -- | Make a substitution Forest (all proper children). Initially we don't -- replace anything. --- mkSubstForest :: Data a => a -> Forest Subst --- mkSubstForest = gmapQ f --- where --- f :: forall d. Data d => d -> Tree Subst --- f x = Node Keep (mkSubstForest x) mkSubstForest :: SubTypes a => a -> Forest Subst mkSubstForest a = map tMap (subTypes a) where tMap t = fmap (\_ -> Keep) t diff --git a/src/Test/SmartCheck/Extrapolate.hs b/src/Test/SmartCheck/Extrapolate.hs index 634e72d..1039c28 100644 --- a/src/Test/SmartCheck/Extrapolate.hs +++ b/src/Test/SmartCheck/Extrapolate.hs @@ -2,11 +2,14 @@ module Test.SmartCheck.Extrapolate ( extrapolate + -- YYY + , matchesShape ) where import Test.SmartCheck.Types import Test.SmartCheck.DataToTree import Test.SmartCheck.Common +import Test.SmartCheck.Reduce import qualified Test.QuickCheck as Q @@ -21,18 +24,22 @@ import Control.Monad -- | Test d with arbitrary values replacing its children. For anything we get -- 100% failure for, we claim we can generalize it---any term in that hole -- fails. -extrapolate :: (Data a, SubTypes a) +extrapolate :: (Data a, SubTypes a, Read a, Show a, Q.Arbitrary a) => Q.Args -> Maybe a -> (a -> Q.Property) -> IO () extrapolate args md prop = do putStrLn "" when (isNothing md) (smartPrtLn "No value to extrapolate.") - unless (isNothing md) $ do smartPrtLn "Extrapolating ..." - smartPrtLn "Extrapolated value:" - idxs <- iter (mkSubstForest d) (Idx 0 0) [] - renderWithVars d idxs + when (isJust md) $ do smartPrtLn "Extrapolating ..." + smartPrtLn "Extrapolated value:" + idxs <- iter (mkSubstForest d) (Idx 0 0) [] + renderWithVars d idxs + d' <- smartRun args (prop' idxs) + extrapolate args d' (prop' idxs) where - Just d = md -- depends on laziness + prop' idxs a = (not $ matchesShape d a idxs) Q.==> prop a + + Just d = md -- use depends on laziness! -- Do a breadth-first traversal of the data, trying to replace items. When we -- find an index we can replace, add it's index to the index list. Recurse @@ -63,6 +70,9 @@ extrapolate args md prop = do --------------------------------------------------------------------------------- +-- PrettyPrinting + +-- | At each index into d from idxs, replace the whole with a fresh value. replaceWithVars :: SubTypes a => a -> [Idx] -> [String] -> Tree String replaceWithVars d idxs vars = foldl' f (mkShowTree d) (zip vars idxs) @@ -71,8 +81,6 @@ replaceWithVars d idxs vars = f tree (var, idx) = let forest = sub (subForest tree) idx var in Node (rootLabel tree) forest ---------------------------------------------------------------------------------- - renderWithVars :: SubTypes a => a -> [Idx] -> IO () renderWithVars d idxs = do putStrLn $ "forall " ++ unwords (take (length idxs) vars) ++ ":" @@ -81,3 +89,20 @@ renderWithVars d idxs = do vars = map (\(x,i) -> x ++ show i) $ zip (repeat "x") [0::Int ..] --------------------------------------------------------------------------------- + +-- | Does a == b modulo the values located at the idxes? We compute this by +-- filling in the holes in a with values from b, and seeing if the result is +-- equal. +matchesShape :: (SubTypes a) => a -> a -> [Idx] -> Bool +matchesShape a b idxs = + case foldl' f (Just b) idxs of + Nothing -> False + Just b' -> a == b' + + where + f mb idx = do + b' <- mb + v <- getAtIdx a idx + replace b' idx v + +--------------------------------------------------------------------------------- diff --git a/src/Test/SmartCheck/Types.hs b/src/Test/SmartCheck/Types.hs index d86f37d..778f881 100644 --- a/src/Test/SmartCheck/Types.hs +++ b/src/Test/SmartCheck/Types.hs @@ -1,9 +1,7 @@ {-# LANGUAGE ExistentialQuantification #-} module Test.SmartCheck.Types - ( -- SmartArgs(..) - -- , stdSmartArgs - SubT(..) + ( SubT(..) , subT , SubTypes(..) , Idx(..) @@ -14,21 +12,6 @@ import Data.Tree import Data.Data import qualified Test.QuickCheck as Q ---------------------------------------------------------------------------------- --- Arguments ---------------------------------------------------------------------------------- - --- data SmartArgs = SmartArgs --- { qcArgs :: Q.Args --- , shrinks :: Int -- How many tries to smart shrink the failed value? --- , grows :: Int -- How many tries to generalize the smart-shrunk value? --- } - ---------------------------------------------------------------------------------- - --- stdSmartArgs :: SmartArgs --- stdSmartArgs = SmartArgs Q.stdArgs 1000 1000 - --------------------------------------------------------------------------------- -- User-defined subtypes of data --------------------------------------------------------------------------------- @@ -42,7 +25,7 @@ instance Show SubT where subT :: (Data a, Q.Arbitrary a, Show a) => a -> SubT subT = SubT -class Data a => SubTypes a where +class (Eq a, Data a) => SubTypes a where subTypes :: a -> Forest SubT ---------------------------------------------------------------------------------