Implemented recursive generalization. Isn't so effective, as QC keeps…

… generating new concrete terms for ungeneralized terms.

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~~

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 }
 
 ---------------------------------------------------------------------------------

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

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

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
+
+---------------------------------------------------------------------------------

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
 
 ---------------------------------------------------------------------------------