content: {-# LANGUAGE ScopedTypeVariables #-}
  
  module Test.SmartCheck.Reduce
    (smartRun
    ) where
  
  import Test.SmartCheck.Args
  import Test.SmartCheck.Types
  import Test.SmartCheck.SmartGen
  import Test.SmartCheck.DataToTree
  import Test.SmartCheck.Render
  
  import qualified Test.QuickCheck as Q
  
  import Data.Typeable
  import Data.Tree
  import Data.Maybe
  
  import Control.Monad (liftM)
  
  --------------------------------------------------------------------------------
  
  -- 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 args res prop = do
    putStrLn ""
    smartPrtLn "Smart Shrinking ..."
    new <- smartShrink args res prop
    smartPrtLn "Smart-shrunk value:"
    print new
    return new
  
  --------------------------------------------------------------------------------
  
  -- | 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 =
    liftM fst $ iter' d (mkForest d) (Idx 0 0)
    where
    mkForest x = mkSubstForest x True
    notProp = Q.expectFailure . prop
  
    iter' x forest_ idx' =
      iter x test next notProp (scMaxDepth args) 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
        -- Found an ex that fails prop.  We'll now test the ex, and start trying
        -- to reduce from the top!
        Just y  -> iter' y (mkForest y) (Idx 0 0)
        -- 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
      let vm = getAtIdx x idx (scMaxDepth args)
      case vm of
        Nothing -> errorMsg "smartShrink0"
        Just v  -> do
          hole <- testHole v
          if isJust hole then return hole
            else do (_, r) <- iterateArb x v idx (scMaxReduce args)
                                -- Maximum size of values to generate; the minimum
                                -- of the value at the current index and the
                                -- maxSize parameter.
                                (min (subValSize x idx) (scMaxSize args))
                                notProp
                    return $ resultToMaybe r
  
      where
      testHole :: SubT -> IO (Maybe a)
      testHole SubT { unSubT = v } =
        maybe (return Nothing) extractAndTest (cast v :: Maybe a)
        where
        extractAndTest :: a -> IO (Maybe a)
        extractAndTest y = do
          res <- resultify notProp y
          return $ resultToMaybe res
  
  resultToMaybe :: Result a -> Maybe a
  resultToMaybe res =
    case res of
      BaseType      -> Nothing
      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 subValSize v (Idx 0 0) == 0.
  -- At (Idx 0 1) in v, we're at (C : C : []), so subValSize v (Idx 0 1) == 2, since
  -- we have the constructors :, C (or :, []) in the longest path underneath.
  -- Base-types have subValSize 0.  So subValSize [1,2,3] idx == 0 for any idx.
  -- Note that if we have subValSize d idx == 0, then it is impossible to construct a
  -- *structurally* smaller value at hole idx.
  subValSize :: SubTypes a => a -> Idx -> Int
  subValSize d idx = maybe 0 depth forestIdx
    where
    forestIdx :: Maybe [Tree Bool]
    forestIdx = fmap subForest $ getIdxForest (mkSubstForest d True) idx
  
  --------------------------------------------------------------------------------
  