Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

interface update.

  • Loading branch information...
commit 1d2dee3996f03499b3a054b847fc9b6725e59ec8 1 parent 68de1c4
@leepike authored
View
4 examples/Div0.hs
@@ -44,8 +44,8 @@ instance Arbitrary Exp where
-- property: so long as 0 isn't in the divisor, we won't try to divide by 0.
-- It's false: something might evaluate to 0 still.
-prop_div :: Exp -> Property
-prop_div e = divSubTerms e ==> eval e /= Nothing
+prop_div :: Exp -> ScProp
+prop_div e = divSubTerms e --> eval e /= Nothing
-- prop_div e = property $ case x of
-- Nothing -> True
-- Just True -> True
View
2  examples/Heap_Program.hs
@@ -36,7 +36,7 @@ deriving instance Typeable OrdA
deriving instance Generic OrdA
heapProgramTest :: IO ()
-heapProgramTest = SC.smartCheck SC.scStdArgs (\h -> property (prop_ToSortedList h))
+heapProgramTest = SC.smartCheck SC.scStdArgs (\h -> (prop_ToSortedList h))
instance SC.SubTypes OrdA
instance (SC.SubTypes a, Ord a, Arbitrary a, Generic a)
View
20 examples/LambdaCalc.hs
@@ -113,16 +113,16 @@ instance Arbitrary Pr where
-- prop0 (Pr (e0, e1)) = alphaEq e0 e1 ==> betaEq e0 e1
-- if you do a beta reduction to nf
-prop1 :: Pr -> Property
-prop1 (Pr e0 e1) = -- Timeout due to possible non-termination
- within 1000 $ alphaEq e0 e1 ==> betaEq e0 (substVar "x" "y" e1)
-
-lambdaTest :: IO ()
-lambdaTest = smartCheck args prop1
- where args = scStdArgs { qcArgs = stdArgs { maxSuccess = 100
- , maxSize = 100
- }
- }
+-- prop1 :: Pr -> ScProp
+-- prop1 (Pr e0 e1) = -- Timeout due to possible non-termination
+-- within 1000 $ alphaEq e0 e1 --> betaEq e0 (substVar "x" "y" e1)
+
+-- lambdaTest :: IO ()
+-- lambdaTest = smartCheck args prop1
+-- where args = scStdArgs { qcArgs = stdArgs { maxSuccess = 100
+-- , maxSize = 100
+-- }
+-- }
---------------------------------------------------------------------------------
-- Cruft
View
2  examples/MutualRecData.hs
@@ -46,7 +46,7 @@ prop0 (M _ _ a) = a < 100
prop0 _ = True
mutRecTest :: IO ()
-mutRecTest = smartCheck args (property . prop0)
+mutRecTest = smartCheck args prop0
where
args = scStdArgs { qcArgs = stdArgs {maxSuccess = 1000} }
View
4 examples/Tests.hs
@@ -3,7 +3,7 @@ module Main where
import Div0
import MutualRecData
import Heap_Program
-import LambdaCalc
+--import LambdaCalc
--import Protocol
main :: IO ()
@@ -11,5 +11,5 @@ main = do
divTest
mutRecTest
heapProgramTest
- lambdaTest
+-- lambdaTest
-- protocolTest
View
108 src/Test/SmartCheck.hs
@@ -5,10 +5,23 @@
-- | Interface module.
module Test.SmartCheck
- ( smartCheck
- , runQC
- , SubTypes(..)
+ ( -- ** Main interface function.
+ smartCheck
+
+ -- ** Type of SmartCheck properties.
+ , ScProp()
+ -- ** Implication for SmartCheck properties.
+ , (-->)
+
+ -- ** Run QuickCheck and get a result.
+ , runQCInit
+
+ -- ** Arguments
, module Test.SmartCheck.Args
+
+ -- ** Main type class based on Generics.
+ , SubTypes(..)
+
-- ** For constructing new instances of `SubTypes`
, gst
, grc
@@ -133,41 +146,73 @@ runAgainMsg = putStrLn $
--------------------------------------------------------------------------------
+-- XXX I have to parse a string from QC to get the counterexamples.
+
+-- | Run QuickCheck initially, to get counterexamples for each argument,
+-- includding the one we want to focus on for SmartCheck, plus a `Property`.
runQCInit :: (Show a, Read a, Q.Arbitrary a, ScProperty prop, Q.Testable prop)
=> Q.Args -> (a -> prop) -> IO (Maybe a, a -> Q.Property)
runQCInit args scProp = do
- let prop = propify scProp
- let genProp = Q.forAllShrink Q.arbitrary Q.shrink prop
- res <- Q.quickCheckWithResult args genProp
- case res of
- -- XXX C'mon, QuickCheck, let me grab the result in a sane way rather than
- -- parsing a string!
- Q.Failure _ _ _ _ _ _ out -> do
- let outs = lines out
- if length outs < 2 then errorMsg "No value to SmartCheck!"
- else do let cexs = tail outs
- let prop' = propifyWithArgs (tail cexs) scProp
- return (Just $ read $ head cexs, prop')
+ res <- Q.quickCheckWithResult args (genProp $ propify scProp)
+ return $ maybe
-- 2nd arg should never be evaluated if the first arg is Nothing.
- _ -> return (Nothing, errorMsg "Bug in runQCInit")
+ (Nothing, errorMsg "Bug in runQCInit")
+ ((\(cex, p) -> (Just cex, p)) . parse)
+ (getOut res)
+ where
+ parse outs = (read $ head cexs, prop')
+ where cexs = lenChk ((< 2) . length) outs
+ prop' = propifyWithArgs (tail cexs) scProp
+-- | Run QuickCheck only analyzing the SmartCheck value, holding the other
+-- values constant.
runQC :: (Show a, Read a, Q.Arbitrary a)
=> Q.Args -> (a -> Q.Property) -> IO (Maybe a)
runQC args prop = do
- let genProp = Q.forAllShrink Q.arbitrary Q.shrink prop
- res <- Q.quickCheckWithResult args genProp
+ res <- Q.quickCheckWithResult args (genProp prop)
+ return $ fmap parse (getOut res)
+ where
+ parse outs = read $ head cexs
+ where cexs = lenChk ((/= 2) . length) outs
+
+lenChk :: ([String] -> Bool) -> [String] -> [String]
+lenChk chk ls = if chk ls then errorMsg "No value to SmartCheck!"
+ else tail ls
+
+getOut :: Q.Result -> Maybe [String]
+getOut res =
case res of
- -- XXX C'mon, QuickCheck, let me grab the result in a sane way rather than
- -- parsing a string!
- Q.Failure _ _ _ _ _ _ out -> do
- let outs = lines out
- if length outs /= 2 then errorMsg "No value to SmartCheck!"
- else do let cexs = tail outs
- return $ Just (read $ head cexs)
- _ -> return Nothing
+ Q.Failure _ _ _ _ _ _ out -> Just $ lines out
+ _ -> Nothing
+
+genProp :: (Show a, Q.Testable prop, Q.Arbitrary a)
+ => (a -> prop) -> Q.Property
+genProp prop = Q.forAllShrink Q.arbitrary Q.shrink prop
--------------------------------------------------------------------------------
+-- | Type for SmartCheck properties. Moral equivalent of QuickCheck's
+-- `Property` type.
+data ScProp = Implies (Bool, Bool)
+ | Simple Bool
+ deriving (Show, Read, Eq)
+
+instance Q.Testable ScProp where
+ property (Simple prop) = Q.property prop
+ property (Implies prop) = Q.property (toQCImp prop)
+ exhaustive (Simple prop) = Q.exhaustive prop
+ exhaustive (Implies prop) = Q.exhaustive (toQCImp prop)
+
+-- same as ==>
+infixr 0 -->
+-- | Moral equivalent of QuickCheck's `==>` operator.
+(-->) :: Bool -> Bool -> ScProp
+pre --> post = Implies (pre, post)
+
+-- Helper function.
+toQCImp :: (Bool, Bool) -> Q.Property
+toQCImp (pre, post) = pre Q.==> post
+
-- | Turn a function that returns a `Bool` into a QuickCheck `Property`.
class ScProperty prop where
scProperty :: [String] -> prop -> Q.Property
@@ -178,10 +223,13 @@ instance ScProperty Bool where
scProperty _ res = Q.property res
qcProperty = Q.property
--- | Instance with a precondition and a postcondition.
-instance ScProperty (Bool,Bool) where
- scProperty _ (pre,post) = Q.property $ pre Q.==> post
- qcProperty (pre,post) = Q.property $ pre Q.==> post
+-- | Wrapped properties.
+instance ScProperty ScProp where
+ scProperty _ (Simple res) = Q.property res
+ scProperty _ (Implies prop) = Q.property $ toQCImp prop
+
+ qcProperty (Simple res) = Q.property res
+ qcProperty (Implies prop) = Q.property $ toQCImp prop
-- | Beta-reduction.
instance (Q.Arbitrary a, Q.Testable prop, Show a, Read a, ScProperty prop)
Please sign in to comment.
Something went wrong with that request. Please try again.