Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Trying to generalize from (a -> Bool) to QuickCheck.Property.

  • Loading branch information...
commit 840f7674c1af32393f2786c98df13978c42b0a45 1 parent cc518c4
@leepike authored
View
11 TODO.md
@@ -7,14 +7,15 @@ TODO
* Collect failed tests as preconditions until we reach a fixed point.
+ * Should be able to discover properties starting from the True?
+
* Use shrink instances as default for base types.
+* When I'm shrinking, if I find a hole that is of the same type (via cast) that
+ also fails the property, replace the original value with the hole.
-Not sure how to do
------------------------------------------------
-* Replace (a -> Bool) properties with Testable properties.
-
- * Not quite sure how to do this...
+* Replace (a -> Bool) properties with Properties. This is needed in case we
+ originally want to omit certain values from triggering a failure.
Done
View
159 examples/Div0.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+
+-- | Divide by 0 example in a simple arithmetic language.
+
+module Div0 where
+
+import Test.QuickCheck
+import Test.SmartCheck
+import Control.Monad
+import Data.Data
+
+data M = C Int
+ | A M M
+ | D M M
+ deriving (Read, Show, Data, Typeable, Eq)
+
+mkTypes :: M -> M -> Forest SubT
+mkTypes m0 m1 = [ Node (subT m0) (subTypes m0)
+ , Node (subT m1) (subTypes m1)
+ ]
+
+instance SubTypes M where
+ subTypes (C _) = []
+ subTypes (A m0 m1) = mkTypes m0 m1
+ subTypes (D m0 m1) = mkTypes m0 m1
+
+eval :: M -> Maybe Int
+eval (C i) = Just i
+eval (A a b) = do
+ i <- eval a
+ j <- eval b
+ return $ i + j
+eval (D a b) =
+ if eval b == Just 0 then Nothing
+ else do i <- eval a
+ j <- eval b
+ return $ i `div` j
+
+instance Arbitrary M where
+ arbitrary = sized mkM
+ where
+ mkM 0 = liftM C arbitrary
+ mkM n = oneof [ liftM2 A mkM' mkM'
+ , liftM2 D mkM' mkM' ]
+ where mkM' = mkM =<< choose (0,n-1)
+
+ shrink (C _) = []
+ shrink (A a b) = [a, b]
+ shrink (D a b) = [a, b]
+
+div0 :: M -> Bool
+div0 m = eval m /= Nothing
+
+div1 :: M -> Property
+div1 m =
+-- True ==>
+ 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
+ divSubTerms (C _) = []
+ divSubTerms (A m0 m1) = divSubTerms m0 ++ divSubTerms m1
+ divSubTerms (D m0 m1) = m1 : divSubTerms m0 ++ divSubTerms m1
+
+-- divProp :: Gen Prop
+-- divProp = forAllShrink arbitrary shrink div1
+
+
+main :: IO ()
+main = do result <- smartRun args div1
+ extrapolate args result div1
+ where args = stdSmartArgs { qcArgs = stdArgs { maxSuccess = 1000
+ , maxSize = 20 }
+
+ }
+
+---------------------------------------------------------------------------------
+-- XXX cruft
+
+-- Fails if some leaf in a complex m == (C 0)
+prop0 :: M -> Property
+prop0 m =
+ (complex m)
+-- False
+ ==> f m
+ where
+ f (C i) = i /= 0
+ f (A m0 m1) = f m0 && f m1
+ f (D m0 m1) = f m0 && f m1
+
+ complex (C _) = False
+ complex _ = True
+
+-- Negation of a property.
+propNot :: (M -> Property) -> (M -> Property)
+propNot prop = \m -> expectFailure (prop m)
+-- p <- prop
+
+
+-- props :: IO ()
+-- props = do
+-- -- 0 not valid, 1 succeed, 2 fail
+-- let xs = [(C 0), A (C 2) (C 1), A (C 0) (C 1)]
+-- let xs' = map prop0 xs :: [Gen Prop]
+-- let fs = map (\(MkGen {unGen = f}) -> unProp $ f undefined undefined) xs'
+-- :: [Rose Result]
+-- r <- mapM (protectRose . reduceRose) fs
+-- :: IO [Rose Result]
+-- let reses = map (\(MkRose res _) -> res) r
+-- putStrLn (show $ map ok reses)
+
+
+
+
+
+-- runATest :: State -> (StdGen -> Int -> Prop) -> IO Result
+-- runATest st f =
+-- do let size = computeSize st (numSuccessTests st) (numDiscardedTests st)
+-- MkRose res ts <- protectRose (reduceRose (unProp (f rnd1 size)))
+-- callbackPostTest st res
+
+-- case res of
+-- MkResult{ok = Just True, stamp = stamp, expect = expect} -> -- successful test
+-- do test st{ numSuccessTests = numSuccessTests st + 1
+-- , randomSeed = rnd2
+-- , collected = stamp : collected st
+-- , expectedFailure = expect
+-- } f
+
+-- MkResult{ok = Nothing, expect = expect} -> -- discarded test
+-- do test st{ numDiscardedTests = numDiscardedTests st + 1
+-- , randomSeed = rnd2
+-- , expectedFailure = expect
+-- } f
+
+-- MkResult{ok = Just False} -> -- failed test
+-- do if expect res
+-- then putPart (terminal st) (bold "*** Failed! ")
+-- else putPart (terminal st) "+++ OK, failed as expected. "
+-- numShrinks <- foundFailure st res ts
+-- theOutput <- terminalOutput (terminal st)
+-- if not (expect res) then
+-- return Success{ labels = summary st,
+-- numTests = numSuccessTests st+1,
+-- output = theOutput }
+-- else
+-- return Failure{ usedSeed = randomSeed st -- correct! (this will be split first)
+-- , usedSize = size
+-- , numTests = numSuccessTests st+1
+-- , numShrinks = numShrinks
+-- , output = theOutput
+-- , reason = P.reason res
+-- , labels = summary st
+-- }
+-- where
+-- (rnd1,rnd2) = split (randomSeed st)
+
+
View
4 src/Test/SmartCheck.hs
@@ -9,8 +9,12 @@ module Test.SmartCheck
, SubT(..)
, subT
, SubTypes(..)
+ , Tree(..)
+ , Forest
) where
import Test.SmartCheck.Reduce
import Test.SmartCheck.Extrapolate
import Test.SmartCheck.Types
+
+import Data.Tree
View
25 src/Test/SmartCheck/Common.hs
@@ -1,6 +1,7 @@
module Test.SmartCheck.Common
( samples
, iterateArb
+ , resultify
, smartPrefix
) where
@@ -8,7 +9,9 @@ import Test.SmartCheck.Types
import Test.SmartCheck.DataToTree
import qualified Test.QuickCheck.Gen as Q
-import qualified Test.QuickCheck as Q
+import qualified Test.QuickCheck as Q hiding (Result)
+import qualified Test.QuickCheck.Property as Q
+
import System.Random
import Data.List
import Data.Data
@@ -37,15 +40,17 @@ samples _ i maxSz = do
-- | 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 that succeeds.
iterateArb :: (Data a, SubTypes a)
- => a -> Idx -> Int -> Int -> (a -> Bool) -> IO (Maybe a)
-iterateArb d idx tries sz prop =
+ => a -> Idx -> Int -> Int
+ -> (a -> Q.Property) -> IO (Maybe a)
+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
-- Catch errors
when (length res /= length rnds) (error "iterateArb")
- return (find prop res)
+-- return (find prop res)
+ return (find undefined res)
where
mkVals SubT { unSubT = v } = do
rnds <- samples v tries sz
@@ -55,6 +60,18 @@ 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
+
+ where
+ err = error "in propify: should not evaluate."
+
+---------------------------------------------------------------------------------
+
smartPrefix :: String
smartPrefix = "*** "
View
4 src/Test/SmartCheck/Extrapolate.hs
@@ -8,6 +8,8 @@ import Test.SmartCheck.Types
import Test.SmartCheck.DataToTree
import Test.SmartCheck.Common
+import qualified Test.QuickCheck as Q
+
import Data.Data
import Data.Tree
import Data.List
@@ -19,7 +21,7 @@ import Data.Maybe
-- 100% failure for, we claim we can generalize it---any term in that hole
-- fails.
extrapolate :: (Data a, SubTypes a)
- => SmartArgs -> a -> (a -> Bool) -> IO ()
+ => SmartArgs -> a -> (a -> Q.Property) -> IO ()
extrapolate args d prop = do
putStrLn ""
putStrLn $ smartPrefix ++ "Extrapolating ..."
View
24 src/Test/SmartCheck/Reduce.hs
@@ -11,6 +11,7 @@ import qualified Test.QuickCheck as Q
import Control.Monad
import Data.Maybe
import Data.Tree
+--import Data.List
---------------------------------------------------------------------------------
@@ -19,7 +20,7 @@ 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 -> Bool) -> IO a
+ => SmartArgs -> (a -> Q.Property) -> IO a
smartRun args prop = do
let genProp = Q.forAllShrink Q.arbitrary Q.shrink prop
res <- runQC (qcArgs args) genProp
@@ -49,7 +50,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 -> Bool) -> IO a
+ => SmartArgs -> a -> (a -> Q.Property) -> IO a
smartShrink args d prop = iter d (Idx 0 0)
where
@@ -59,6 +60,13 @@ smartShrink args d prop = iter d (Idx 0 0)
then iter d' (idx { level = level idx + 1 })
else do if isNothing maxSize
then iter d' (idx { column = column idx + 1 })
+ -- XXX We could shrink base values, but I'm not sure if
+ -- it's worth it. Doesn't affect extrapolation or make
+ -- counter-examples more readable.
+
+ -- then case getAtIdx d' idx of
+ -- Nothing -> iter d' (idx { column = column idx + 1 })
+ -- Just v -> mkVals v
else mkTry
where
@@ -73,7 +81,11 @@ smartShrink args d prop = iter d (Idx 0 0)
else iter d' (idx { column = column idx + 1 })
forest = mkSubstForest d'
- notProp = not . prop
+-- notProp = not . prop
+ -- notProp = do p <- prop
+ -- return $ not p
+ notProp = undefined
+
-- XXX How do I know that the size of arbitrary relates to the depth of the
-- structure? However, things seem to work, but I'm not sure if it's
@@ -88,4 +100,10 @@ smartShrink args d prop = iter d (Idx 0 0)
done = length pts <= level idx
nextLevel = length (pts !! level idx) <= column idx
+ -- mkVals SubT { unSubT = v } =
+ -- let vs = map (replaceAtIdx d' idx) (Q.shrink v) in
+ -- case find notProp (catMaybes vs) of
+ -- Nothing -> iter d' (idx { column = column idx + 1 })
+ -- Just x -> iter x (idx { column = column idx + 1 })
+
---------------------------------------------------------------------------------
View
2  src/Test/SmartCheck/Types.hs
@@ -34,7 +34,7 @@ stdSmartArgs = SmartArgs Q.stdArgs 1000 1000
---------------------------------------------------------------------------------
data SubT = forall a. (Data a, Q.Arbitrary a, Show a)
- => SubT { unSubT :: a }
+ => SubT { unSubT :: a }
instance Show SubT where
show (SubT t) = show t
Please sign in to comment.
Something went wrong with that request. Please try again.