Permalink
Browse files

Use Property rather than Bool.

  • Loading branch information...
1 parent 840f767 commit 384cba0691333fa5d086a8e82d0b6c35adc41886 @leepike committed Apr 19, 2012
View
@@ -53,12 +53,13 @@ div0 m = eval m /= Nothing
div1 :: M -> Property
div1 m =
--- True ==>
- pre ==> eval m /= Nothing
+ True ==> eval m /= Nothing
+-- pre ==> eval m /= Nothing
where
- -- precondition: no dividand in a subterm can evaluate to 0.
- pre = and $ map non0Divsors (divSubTerms m)
- non0Divsors m0 = eval m0 /= Just 0
+ -- precondition: no dividand in a subterm can be 0.
+ pre = null (divSubTerms m)
+-- non0Divsors m0 = eval m0 /= Just 0
+ divSubTerms (C 0) = [C 0]
divSubTerms (C _) = []
divSubTerms (A m0 m1) = divSubTerms m0 ++ divSubTerms m1
divSubTerms (D m0 m1) = m1 : divSubTerms m0 ++ divSubTerms m1
@@ -70,10 +71,9 @@ div1 m =
main :: IO ()
main = do result <- smartRun args div1
extrapolate args result div1
- where args = stdSmartArgs { qcArgs = stdArgs { maxSuccess = 1000
- , maxSize = 20 }
-
- }
+
+ where args = stdArgs { maxSuccess = 1000
+ , maxSize = 20 }
---------------------------------------------------------------------------------
-- XXX cruft
@@ -3,11 +3,10 @@
module MutualRecData where
import Test.SmartCheck
+import Test.QuickCheck hiding (Result)
-import Data.Tree
import Data.Data
import Control.Monad.State
-import Test.QuickCheck hiding (Result)
---------------------------------------------------------------------------------
@@ -65,10 +64,11 @@ prop0 (M _ _ a) = a < 100
prop0 _ = True
main :: IO ()
-main = do result <- smartRun args prop0
- extrapolate args result prop0
+main = do result <- smartRun args p
+ extrapolate args result p
where
- args = stdSmartArgs { qcArgs = stdArgs { maxSuccess = 1000 } }
+ p = \a -> property (prop0 a)
+ args = stdArgs { maxSuccess = 1000 }
---------------------------------------------------------------------------------
@@ -1,9 +1,9 @@
-- | Interface module.
module Test.SmartCheck
- ( SmartArgs (..)
- , stdSmartArgs
- , smartRun
+ ( -- SmartArgs (..)
+ -- , stdSmartArgs
+ smartRun
, extrapolate
-- SubTypes class
, SubT(..)
@@ -49,9 +49,25 @@ iterateArb d idx tries sz prop =
let res = catMaybes $ map repl rnds
-- Catch errors
when (length res /= length rnds) (error "iterateArb")
--- return (find prop res)
- return (find undefined res)
+ findM goodResult res
+
where
+ findM _ [] = return Nothing
+ findM f (x:xs) = do b <- f x
+ if b then return (Just x)
+ else findM f xs
+
+ goodResult a = do
+ res <- resultify prop a
+ let go = if Q.expect res
+ then case Q.ok res of
+ Just True -> True
+ _ -> False
+ else case Q.ok res of
+ Just False -> True
+ _ -> False
+ return go
+
mkVals SubT { unSubT = v } = do
rnds <- samples v tries sz
return $ map subT rnds
@@ -60,14 +76,22 @@ iterateArb d idx tries sz prop =
---------------------------------------------------------------------------------
-resultify :: (a -> Q.Property) -> a -> Q.Result
-resultify prop a =
- let Q.MkGen { Q.unGen = f } = prop a :: Q.Gen Q.Prop in
- let fs = Q.unProp $ f err err :: Q.Rose Q.Result in
- let (Q.MkRose res _) = fs in
- res
+-- XXX need to protect by calling (protectRose . reduceRose) ?
+resultify :: (a -> Q.Property) -> a -> IO Q.Result
+resultify prop a = do
+ Q.MkRose r _ <- res fs
+ return r
where
+ Q.MkGen { Q.unGen = f } = prop a :: Q.Gen Q.Prop
+ fs = Q.unProp $ f err err :: Q.Rose Q.Result
+ res = Q.protectRose . Q.reduceRose
+
+-- case fs' of
+-- (Q.MkRose res' _) -> res'
+-- io -> res (Q.ioRose io)
+
+
err = error "in propify: should not evaluate."
---------------------------------------------------------------------------------
@@ -81,6 +81,20 @@ getIdxForest forest idx =
---------------------------------------------------------------------------------
+-- | Returns the value at index idx. Returns nothing if the index is out of
+-- bounds.
+getAtIdx :: SubTypes a
+ => a -- ^ Parent value
+ -> Idx -- ^ Index of hole to replace
+ -> Maybe SubT
+getAtIdx d Idx { level = l
+ , column = c }
+ = if length lev > c then Just (lev !! c) else Nothing
+ where
+ lev = getLevel (subTypes d) l
+
+---------------------------------------------------------------------------------
+
-- | Replace a tree at index Idx in a Forest. Return the original if the index
-- is out of range. All subforests are removed.
sub :: Forest a -> Idx -> a -> Forest a
@@ -117,20 +131,6 @@ mkSubstForest a = map tMap (subTypes a)
---------------------------------------------------------------------------------
--- | Returns the value at index idx. Returns nothing if the index is out of
--- bounds.
-getAtIdx :: SubTypes a
- => a -- ^ Parent value
- -> Idx -- ^ Index of hole to replace
- -> Maybe SubT
-getAtIdx d Idx { level = l
- , column = c }
- = if length lev > c then Just (lev !! c) else Nothing
- where
- lev = getLevel (subTypes d) l
-
----------------------------------------------------------------------------------
-
-- | Replace a value at index idx generically in a Tree/Forest generically.
replaceAtIdx :: (SubTypes a, Data b)
=> a -- ^ Parent value
@@ -14,23 +14,26 @@ import Data.Data
import Data.Tree
import Data.List
import Data.Maybe
+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)
- => SmartArgs -> a -> (a -> Q.Property) -> IO ()
-extrapolate args d prop = do
+ => Q.Args -> Maybe a -> (a -> Q.Property) -> IO ()
+extrapolate args md prop = do
putStrLn ""
- putStrLn $ smartPrefix ++ "Extrapolating ..."
- putStrLn $ smartPrefix ++ "Extrapolated value:"
-
- idxs <- iter (mkSubstForest d) (Idx 0 0) []
- renderWithVars d idxs
+ when (isNothing md) (putStrLn $ smartPrefix ++ "No value to extrapolate.")
+ unless (isNothing md) $ do putStrLn $ smartPrefix ++ "Extrapolating ..."
+ putStrLn $ smartPrefix ++ "Extrapolated value:"
+ idxs <- iter (mkSubstForest d) (Idx 0 0) []
+ renderWithVars d idxs
where
+ Just d = md -- 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
-- down the structure, following subtrees that have *not* been replaced.
@@ -39,7 +42,7 @@ extrapolate args d prop = do
if done then return idxs
else if nextLevel
then iter forest (idx { level = level idx + 1 }) idxs
- else do tries <- iterateArb d idx (grows args) rate prop
+ else do tries <- iterateArb d idx (Q.maxDiscard args) rate prop
if isNothing tries
-- None of the tries satisfy prop. Prevent recurring down
-- this tree, since we can generalize.
@@ -53,7 +56,7 @@ extrapolate args d prop = do
where
-- XXX right ratio? Should I use a user-specified arg?
- rate = ceiling (sqrt $ fromIntegral (grows args) :: Float) :: Int
+ rate = ceiling (sqrt $ fromIntegral (Q.maxDiscard args) :: Float) :: Int
pts = breadthLevels forest
done = length pts <= level idx
nextLevel = length (pts !! level idx) <= column idx
@@ -8,10 +8,8 @@ import Test.SmartCheck.Common
import Test.SmartCheck.DataToTree
import qualified Test.QuickCheck as Q
-import Control.Monad
import Data.Maybe
import Data.Tree
---import Data.List
---------------------------------------------------------------------------------
@@ -20,17 +18,24 @@ import Data.Tree
-- increasingly larger) randomly-generated values until we find a failure, and
-- return that result. (We call smartShrink recursively.)
smartRun :: (Read a, Show a, Q.Arbitrary a, SubTypes a)
- => SmartArgs -> (a -> Q.Property) -> IO a
+ => Q.Args -> (a -> Q.Property) -> IO (Maybe a)
smartRun args prop = do
let genProp = Q.forAllShrink Q.arbitrary Q.shrink prop
- res <- runQC (qcArgs args) genProp
- unless (isJust res) (return ())
- new <- smartShrink args (fromJust res) prop
- putStrLn ""
- putStrLn $ smartPrefix ++ "Smart Shrinking ... "
- putStrLn $ smartPrefix ++ "Smart-shrunk value:"
- print new
- return new
+ res <- runQC args genProp
+ if (isJust res) then runSmart (fromJust res)
+ else do putStrLn ""
+ putStrLn $ smartPrefix ++ "No value to smart-shrink!"
+ return Nothing
+
+ where
+ runSmart r = do
+ putStrLn ""
+ putStrLn $ smartPrefix ++ "Smart Shrinking ... "
+ new <- smartShrink args r prop
+
+ putStrLn $ smartPrefix ++ "Smart-shrunk value:"
+ print new
+ return (Just new)
---------------------------------------------------------------------------------
@@ -50,7 +55,7 @@ runQC args propGen = 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 :: SubTypes a
- => SmartArgs -> a -> (a -> Q.Property) -> IO a
+ => Q.Args -> a -> (a -> Q.Property) -> IO a
smartShrink args d prop = iter d (Idx 0 0)
where
@@ -70,7 +75,7 @@ smartShrink args d prop = iter d (Idx 0 0)
else mkTry
where
- mkTry = do try <- iterateArb d' idx (shrinks args)
+ mkTry = do try <- iterateArb d' idx (Q.maxDiscard args)
(fromJust maxSize) notProp
-- first failing try
if isJust try
@@ -81,10 +86,7 @@ smartShrink args d prop = iter d (Idx 0 0)
else iter d' (idx { column = column idx + 1 })
forest = mkSubstForest d'
--- notProp = not . prop
- -- notProp = do p <- prop
- -- return $ not p
- notProp = undefined
+ notProp = Q.expectFailure . prop
-- XXX How do I know that the size of arbitrary relates to the depth of the
@@ -1,9 +1,9 @@
{-# LANGUAGE ExistentialQuantification #-}
module Test.SmartCheck.Types
- ( SmartArgs(..)
- , stdSmartArgs
- , SubT(..)
+ ( -- SmartArgs(..)
+ -- , stdSmartArgs
+ SubT(..)
, subT
, SubTypes(..)
, Idx(..)
@@ -18,16 +18,16 @@ 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?
- }
+-- 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
+-- stdSmartArgs :: SmartArgs
+-- stdSmartArgs = SmartArgs Q.stdArgs 1000 1000
---------------------------------------------------------------------------------
-- User-defined subtypes of data

0 comments on commit 384cba0

Please sign in to comment.