Reduce/extrapolate: major refactoring, simplification, bug fixes.

src/Test/SmartCheck/Reduce.hs

@@ -10,18 +10,18 @@ import Test.SmartCheck.DataToTree
 import Test.SmartCheck.Render
 
 import qualified Test.QuickCheck as Q
-import Data.Typeable
 
+import Data.Typeable
 import Data.Tree
+import Data.Maybe
 
 ---------------------------------------------------------------------------------
 
 -- Smarter than shrinks.  Does substitution.  m is a value that failed QC that's
 -- been shrunk.  We substitute successive children with strictly smaller (and
 -- increasingly larger) randomly-generated values until we find a failure, and
 -- return that result.  (We call smartShrink recursively.)
-smartRun :: SubTypes a
-         => ScArgs -> a -> (a -> Q.Property) -> IO a
+smartRun :: SubTypes a => ScArgs -> a -> (a -> Q.Property) -> IO a
 smartRun args res prop = do
   putStrLn ""
   smartPrtLn "Smart Shrinking ... "
@@ -35,64 +35,19 @@ smartRun args res prop = do
 -- | Breadth-first traversal of d, trying to shrink it with *strictly* smaller
 -- children.  We replace d whenever a successful shrink is found and try again.
 smartShrink :: forall a. SubTypes a => ScArgs -> a -> (a -> Q.Property) -> IO a
-smartShrink args d prop = iter' d (mkForest d) (Idx 0 0) >>= return . fst
+smartShrink args d prop = 
+  iter' d (mkForest d) (Idx 0 0) >>= return . fst
 
   where
-  notProp    = Q.expectFailure . prop
   mkForest x = mkSubstForest x True
-  iter' y forest_ idx' = 
-    iter y test next notProp forest_ idx' (errorMsg "next-idxs")
-
-  --------------------------------------
-  test :: a -> Idx -> IO (Maybe a)
-  test x idx = 
-    case maxSize of
-      -- We'll continue down the tree.
-      Nothing     -> return Nothing
-      Just maxVal -> go maxVal
+  notProp = Q.expectFailure . prop
 
-    where
-    maxSize :: Maybe Int
-    maxSize = let dep = fmap depth forestIdx in
-              case dep of 
-                Nothing -> Nothing
-                Just d'  -> if d' <= 1 then Nothing else Just (d' - 1)
-      where
-      forestIdx = fmap subForest $ getIdxForest (mkForest x) idx
-
-    go maxVal = do 
-      v <- case getAtIdx x idx of
-             Nothing  -> return Nothing
-             Just v'  -> testHole v'
-      case v of
-        -- This sees if some subterm directly fails the property.  If so, we'll
-        -- take it, if it's well-typed.
-        Just v' -> return (Just v')
-        -- Otherwise, we'll do maxFailure tests of max, trying to pass the
-        -- precondition to find a failure.  We claim to find a failure if some
-        -- test satisfies the precondition and satisfies
-        --
-        -- (Q.expectFailure . originalProp).
-        Nothing -> do r <- iterateArb x idx (maxFailure args) maxVal notProp
-                      return $ case r of
-                                 Result a -> Just a
-                                 _        -> Nothing
-
-    testHole :: SubT -> IO (Maybe a)
-    testHole SubT { unSubT = v } = 
-      case cast v :: Maybe a of
-        Nothing -> return Nothing
-        -- FailedPreCond is just seeding extractResult, a folding operator.
-        Just y  -> do res <- extractResult notProp FailedPreCond y
-                      case res of
-                        -- This is a failed value strictly smaller.  Let's test
-                        -- starting from here.
-                        Result z      -> return (Just z)
-                        FailedPreCond -> return Nothing
-                        FailedProp    -> return Nothing
+  iter' x forest_ idx' = 
+    iter x test next notProp forest_ idx' (errorMsg "next-idxs")
 
-  --------------------------------------
+  -------------------------------------- 
 
+  -- next tells the iter what to do after running a test.
   next :: a -> Maybe a -> Forest Bool -> Idx -> [Idx] -> IO (a, [Idx])
   next x res forest idx _ = 
     case res of
@@ -102,5 +57,63 @@ smartShrink args d prop = iter' d (mkForest d) (Idx 0 0) >>= return . fst
       -- Either couldn't satisfy the precondition or nothing satisfied the
       -- property.  Either way, we can't shrink it.
       Nothing -> iter' x forest idx { column = column idx + 1 }
-
+
+  -------------------------------------- 
+
+  -- Our test function.  First, we'll see if we can just return the hole at idx,
+  -- assuming it's (1) well-typed and (2), fails the test.  Otherwise, we'll
+  -- test x by replacing values at idx against (Q.expectFailure . prop).  Make
+  -- sure that values generated are strictly smaller than the value at
+  -- idx.
+  test :: a -> Idx -> IO (Maybe a)
+  test x idx = do
+    hole <- testHole (getAtIdx x idx)
+    if isJust hole then return hole
+      else do r <- iterateArb x idx (maxFailure args) (maxSize x idx) notProp
+              return $ case r of
+                         Result a -> Just a
+                         FailedPreCond -> Nothing
+                         FailedProp    -> Nothing
+
+    where
+    -- -- XXX debuging
+    -- sh (Just SubT { unSubT = v }) = show v
+
+    testHole :: Maybe SubT -> IO (Maybe a)
+    testHole Nothing = return Nothing
+    testHole (Just SubT { unSubT = v }) = 
+      case cast v :: Maybe a of
+        Just v' -> extractAndTest v'
+        Nothing -> return Nothing
+      where
+      extractAndTest :: a -> IO (Maybe a)
+      extractAndTest y = do 
+        res <- resultify notProp y
+        return $ case res of
+                   FailedPreCond -> Nothing
+                   FailedProp    -> Nothing
+                   Result n      -> Just n
+
+---------------------------------------------------------------------------------
+
+-- | Get the maximum depth of d's subforest at idx.  Intuitively, it's the
+-- maximum number of constructors you have *below* the constructor at idx.  So
+-- for a unary constructor C, the value [C, C, C]
+
+-- (:) C 
+--   (:) C
+--     (:) C []
+
+-- At (Idx 0 0) in v, we're at C, so maxSize v (Idx 0 0) == 0.
+-- At (Idx 0 1) in v, we're at (C : C : []), so maxSize v (Idx 0 1) == 2, since
+-- we have the constructors :, C (or :, []) in the longest path underneath.
+-- Base-types have maxSize 0.  So maxSize [1,2,3] idx == 0 for any idx.
+-- Note that if we have maxSize d idx == 0, then it is impossible to construct a
+-- *structurally* smaller value at hole idx.
+maxSize :: SubTypes a => a -> Idx -> Int
+maxSize d idx = maybe 0 id (fmap depth forestIdx)
+  where
+  forestIdx :: Maybe [Tree Bool]
+  forestIdx = fmap subForest $ getIdxForest (mkSubstForest d True) idx
+
 ---------------------------------------------------------------------------------

src/Test/SmartCheck/SmartGen.hs

@@ -1,7 +1,7 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
 module Test.SmartCheck.SmartGen
-  ( Result(..)
-  , iterateArb
-  , extractResult
+  ( iterateArb
   , resultify
   , replace
   , iter
@@ -14,95 +14,95 @@ import qualified Test.QuickCheck.Gen as Q
 import qualified Test.QuickCheck as Q hiding (Result)
 import qualified Test.QuickCheck.Property as Q
 
-import System.Random hiding (next)
-import Data.List
-import Data.Maybe
+import System.Random 
 import Data.Tree hiding (levels)
-import Control.Monad
-
----------------------------------------------------------------------------------
-
--- | Possible results of iterateArb.
-data Result a = FailedPreCond -- ^ Couldn't satisfy the precondition of a
-                              -- QuickCheck property
-              | FailedProp    -- ^ Failed the property
-              | Result a      -- ^ Satisfied it, with the satisfying value
-  deriving (Show, Read, Eq)
-
----------------------------------------------------------------------------------
-
--- | Make some samples no larger than maxSz of the same type as value a.
-samples :: Q.Arbitrary a 
-        => a   -- ^ unused; just to type arbitrary.
-        -> Int -- ^ Number of tries.
-        -> Int -- ^ Maximum size of the structure generated.
-        -> IO [a]
-samples _ i maxSz = do
-  rnd0 <- newStdGen
-  when (maxSz < 0) (errorMsg "samples: maxSize less than 0.")
-  let ls = sort . take i $ randomRs (0, maxSz) rnd0 -- XXX better distribution?
-  let rnds rnd = rnd1 : rnds rnd2 where (rnd1,rnd2) = split rnd
-  let Q.MkGen m = Q.arbitrary
-  -- Remember, m is a *function*, that takes a random generator (r) and a
-  -- maxSize parameter (n).  We control size using the n parameter.  This is
-  -- morally equivalent to using the resize function in QuickCheck.Gen.
-  return [ (m r n) | (r,n) <- rnds rnd0 `zip` ls ]
 
 ---------------------------------------------------------------------------------
 
 -- | Replace the hole in d indexed by idx with a bunch of random values, and
 -- test the new d against the property.  Returns the first new d (the full d but
--- with the hole replaced) that succeeds.
-iterateArb :: SubTypes a
-           => a -> Idx -> Int -> Int
-           -> (a -> Q.Property) -> IO (Result a)
-iterateArb d idx tries sz prop = 
-  case getAtIdx d idx of
-    Nothing -> errorMsg "iterateArb 0"
-    Just v  -> do rnds <- mkVals v
-                  forM_ rnds (\a -> if isNothing $ replace d idx a
-                                      then errorMsg "iterateArb 1"
-                                      else return ())
-
-                  let res = catMaybes $ map (replace d idx) rnds
-                  -- Catch errors that shouldn't ever happen: this means that
-                  -- there is probably a bad idx passed in.
-                  when (length res /= length rnds) (errorMsg "iterateArb 1")
-                  foldM (extractResult prop) FailedPreCond res
+-- with the hole replaced) that succeeds.  "Succeeds" is determined by the call
+-- to resultify---if we're expecting failure, then we succeed by getting a value
+-- that passes the precondition but fails the property; otherwise we succeed by
+-- getting a value that passes the precondition and satisfies the property.  If
+-- no value ever satisfies the precondition, then we return FailedPreCond.
+-- (Thus, there's an implied linear order on the Result type: FailedPreCond <
+-- FailedProp < Result a.)
+iterateArb :: forall a. SubTypes a
+           => a -> Idx -> Int -> Int -> (a -> Q.Property) -> IO (Result a)
+iterateArb d idx tries maxSize prop = do
+  g <- newStdGen
+  iterateArb' FailedPreCond g 0 0
+
   where
-
-  mkVals SubT { unSubT = v } = do
-    rnds <- samples v tries sz
-    return $ map subT rnds
+  ext :: SubT
+  ext = case getAtIdx d idx of
+          Just v  -> v
+          Nothing -> errorMsg "iterateArb 0"
+
+  newMax SubT { unSubT = v } = maxDepth v
+
+  -- Main loop.  We break out if we ever satisfy the property.  Otherwise, we
+  -- return the latest value.
+  iterateArb' :: Result a -> StdGen -> Int -> Int -> IO (Result a)
+  iterateArb' res g try currMax
+    -- We've exhausted the number of iterations.
+    | try >= tries = return res
+    -- Values are now too big.  Start again with size at 0.
+    | newMax s >= maxSize = iterateArb' res g0 (try + 1) 0
+    | otherwise = 
+        case replace d idx s of
+          Nothing -> errorMsg "iterateArb 1"
+          Just d' -> do 
+            res' <- resultify prop d'
+            case res' of
+              FailedPreCond -> rec FailedPreCond
+              FailedProp    -> rec FailedProp
+              Result x      -> return (Result x)
+
+    where 
+    (size, g0) = randomR (0, currMax) g
+    s = sample ext g size
+    sample SubT { unSubT = v } = newVal v 
+    rec res' = iterateArb' res' g0 (try + 1) 
+                 (currMax * 2) -- XXX what ratio is right to increase size of
+                               -- values?  This gives us exponentail growth, but
+                               -- remember we're randomly chosing within the
+                               -- range of [0, max], so many values are
+                               -- significantly smaller than the max.  Plus we
+                               -- reset the size whenever we get a value that's
+                               -- too big.
 
 ---------------------------------------------------------------------------------
 
--- | Must pass the precondition at least once to return either FailedProp or
--- Result.
-extractResult :: (a -> Q.Property) -> Result a -> a -> IO (Result a)
-extractResult _    r@(Result _) _ = return r
-extractResult prop r            a = do
-  res <- resultify prop a 
-  let go = case Q.ok res of
-             Nothing -> r -- Failed the precondition
-             Just b  -> if Q.expect res 
-                          then if b then Result a else FailedProp
-                          else if b then FailedProp else Result a
-  return go
+-- | Make a new random value given a generator and a max size.  Based on the
+-- value's type's arbitrary instance.
+newVal :: forall a. (SubTypes a, Q.Arbitrary a) 
+       => a -> StdGen -> Int -> SubT
+newVal _ g size = 
+  let Q.MkGen m = Q.resize size (Q.arbitrary :: Q.Gen a) in
+  let v = m g size in
+  subT v
 
 ---------------------------------------------------------------------------------
 
+-- | Put a value v into a another value d at a hole idx, if v is well-typed.
+-- Return Nothing if dynamic typing fails.
 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
+-- | Make a QuickCheck Result by applying a property function to a value and
+-- then get out the Result using our result type.
+resultify :: (a -> Q.Property) -> a -> IO (Result a)
 resultify prop a = do 
   Q.MkRose r _ <- res fs
-  return r
-
+  return $ case Q.ok r of -- result of test case (True ==> passed)
+             Nothing -> FailedPreCond -- Failed precondition (discard)
+             Just b  -> if b && Q.expect r then Result a
+                          else if not b && not (Q.expect r) then Result a
+                                 else FailedProp
   where
   Q.MkGen { Q.unGen = f } = prop a :: Q.Gen Q.Prop
   fs  = Q.unProp $ f err err       :: Q.Rose Q.Result
@@ -115,9 +115,9 @@ resultify prop a = do
 type Next a b = a -> b -> Forest Bool -> Idx -> [Idx] -> IO (a, [Idx])
 type Test a b = a -> Idx -> IO b
 
--- Do a breadth-first traversal of the data, trying to replace holes.  When we
--- find an index we can replace, add its index to the index list.  Recurse down
--- the structure, following subtrees that have *not* been replaced.
+-- Do a breadth-first traversal of the data.  First, we find the next valid
+-- index we can use.  Then we apply our test function, passing the result to our
+-- next function.
 iter :: SubTypes a 
      => a                 -- ^ Failed value
      -> Test a b          -- ^ Test to use
@@ -127,21 +127,29 @@ iter :: SubTypes a
      -> Idx               -- ^ Starting index to extrapolate
      -> [Idx]             -- ^ List of generalized indices
      -> IO (a, [Idx])
-iter d test next prop forest idx idxs 
+iter d test nxt prop forest idx idxs 
   | done      = return (d, idxs)
   | nextLevel = iter'
   | atFalse   = iter' -- Must be last check or !! index below may be out of
                       -- bounds!
   | otherwise = do tries <- test d idx
-                   next d tries forest idx idxs
+                   nxt d tries forest idx idxs
 
   where
   -- Location is w.r.t. the forest, not the original data value.
   levels     = breadthLevels forest
   done       = length levels <= level idx
   nextLevel  = length (levels !! level idx) <= column idx
   atFalse    = not $ (levels !! level idx) !! column idx
-  iter'      = iter d test next prop forest 
+  iter'      = iter d test nxt prop forest 
                  idx { level = level idx + 1, column = 0 } idxs
 
 ---------------------------------------------------------------------------------
+
+-- | Get the maximum depth of a value, where depth is measured in the maximum
+-- depth of the tree representation, not counting base types (defined in
+-- Types.hs).
+maxDepth :: SubTypes a => a -> Int
+maxDepth d = depth (mkSubstForest d True) 
+
+---------------------------------------------------------------------------------