Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Refactoring, bug fixes.

  • Loading branch information...
commit 847ea384dc060ad63b0248ad9143bd22225c7856 1 parent 663df16
@leepike authored
View
22 refs/README.txt
@@ -0,0 +1,22 @@
+* The SYB paper:
+ http://research.microsoft.com/en-us/um/people/simonpj/Papers/hmap/index.htm
+ Has shrink example
+
+* The Scrap your zippers paper:
+ https://www.cs.indiana.edu/~adamsmd/papers/scrap_your_zippers/
+ (I could build on this)
+
+* TODO:
+ * Find disjunctive invariants---actually, just add as new preconditions to tests.
+ * Run smartcheck and quickcheck in parallel. Maybe?
+ * Run as many tests in parallel as possible. Maybe?
+
+* QuickSpec:
+ http://www.cse.chalmers.se/~nicsma/quickspec.pdf
+
+* http://blog.regehr.org/archives/697 --- check out C-reduce (Regehr) and Delta
+ debugging (http://www.st.cs.uni-saarland.de/dd/). C-reduce is in PLDI.
+
+* Also check out http://www.whyprogramsfail.com/
+
+* GenCheck https://github.com/JacquesCarette/GenCheck
View
3  smartcheck.cabal
@@ -21,8 +21,7 @@ Library
Test.SmartCheck.SmartGen,
Test.SmartCheck.DataToTree,
Test.SmartCheck.Render,
- Test.SmartCheck.ConstructorGen,
- Test.SmartCheck.Generalize
+ Test.SmartCheck.ConstructorGen
Build-depends: base >= 4.0,
QuickCheck >= 2.4.2,
View
26 src/Test/SmartCheck.hs
@@ -38,6 +38,10 @@ smartCheck args prop = smartCheck' prop []
-- Extrapolate with the original property to see if we get
-- a previously-visited value back.
Just d' -> do (idxs, prop_) <- extrapolate args d' prop ds
+
+ putStrLn $ "ex d: " ++ show d -- YYY
+ putStrLn $ "ex idx " ++ show idxs -- YYY
+
return $ Just (idxs, prop_, d' : ds)
--continue idx prop_ (d' : ds)
@@ -50,8 +54,7 @@ smartCheck args prop = smartCheck' prop []
Just d' -> constrsGen args d' >>= return . Just
else return Nothing
- -- If either extraopolation pass yielded fruit, prettyprint it. Otherwise,
- -- fail.
+ -- If either extraopolation pass yielded fruit, prettyprint it.
if (nonEmpty vs cs)
then case d of
-- We shouldn't have non-empty extrapolation if there was no
@@ -66,18 +69,21 @@ smartCheck args prop = smartCheck' prop []
++ " any character then 'Enter' to quit.)"
s <- getLine
if (s == "")
- then smartCheck' (f vs $ prop) (newds vs)
+ then smartCheck' (f vs $ prop) (newVals vs)
else smartPrtLn "Done."
where
- newds :: Maybe (Extrapolate a) -> [a]
- newds vs = case vs of
- Nothing -> ds
- Just (_, _, ds') -> ds'
+ newVals :: Maybe (Extrapolate a) -> [a]
+ newVals vs = case vs of
+ Nothing -> ds
+ Just (_, _, ds') -> ds'
output :: a -> Replace Idx -> IO ()
output d repl = do
+ putStrLn $ "d: " ++ show d -- YYY
+ putStrLn $ "idx " ++ show repl -- YYY
+
smartPrtLn "Extrapolated value:"
renderWithVars (treeShow args) d repl -- XXX
@@ -89,24 +95,20 @@ smartCheck args prop = smartCheck' prop []
v = case vs of
Nothing -> []
Just (idxs, _, _) -> idxs
-
c = case cs of
Nothing -> []
Just idxs -> idxs
-
f vs = case vs of
Nothing -> id
Just (_, prop_, _) -> prop_
- nonEmpty vs cs =
- vsIdxs || csIdxs
+ nonEmpty vs cs = vsIdxs || csIdxs
where
vsIdxs = case vs of
Just (idxs, _, _) -> not $ null idxs
Nothing -> False
-
csIdxs = case cs of
Just idxs -> not $ null idxs
Nothing -> False
View
11 src/Test/SmartCheck/DataToTree.hs
@@ -4,7 +4,7 @@
module Test.SmartCheck.DataToTree
( subForestPath
, forestReplaceChop
- , forestStop
+ , forestReplaceStop
, getAtIdx
, replaceAtIdx
, getIdxForest
@@ -115,12 +115,15 @@ forestReplaceChop = sub Chop
-- | Replace a tree at index Idx in a Forest. Return the original if the
-- index is out of range. Replace the subforest of Idx with the Substs.
-forestStop :: Forest Subst -> Idx -> Forest Subst
-forestStop f idx = sub ReplaceSubs f idx Subst
+forestReplaceStop :: Forest Subst -> Idx -> Forest Subst
+forestReplaceStop f idx = sub ReplaceSubs f idx Subst
---------------------------------------------------------------------------------
-data SubStrat = Path | ReplaceSubs | Chop
+data SubStrat = Path -- ^ Replace everything in the path from the root to
+ -- here.
+ | ReplaceSubs -- ^ Replace the subforest with a value.
+ | Chop -- ^ Replace a value and remove the subforest.
deriving (Show, Read, Eq)
sub :: SubStrat -> Forest a -> Idx -> a -> Forest a
View
78 src/Test/SmartCheck/Extrapolate.hs
@@ -7,7 +7,6 @@ module Test.SmartCheck.Extrapolate
import Test.SmartCheck.Types
import Test.SmartCheck.DataToTree
import Test.SmartCheck.SmartGen
-import Test.SmartCheck.Generalize
import Test.SmartCheck.Render
import qualified Test.QuickCheck as Q
@@ -20,13 +19,13 @@ import Data.List
-- | 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.
-
+--
-- We extrapolate w.r.t. the original property since extrapolation throws away
-- any values that fail the precondition of the property (i.e., before the
-- Q.==>).
-
+--
-- We extrapolate if there exists at least one test that satisfies the
--- precondition, and for all tests that asatisfy the precondition, they fail.
+-- precondition, and for all tests that satisfy the precondition, they fail.
extrapolate :: SubTypes a
=> ScArgs -- ^ Arguments
-> a -- ^ Current failed value
@@ -36,54 +35,41 @@ extrapolate :: SubTypes a
extrapolate args d origProp ds = do
putStrLn ""
smartPrtLn "Extrapolating values ..."
- idxs <- iter (qcArgs args) strategy forest d origProp (Idx 0 0) []
-
- if matchesShapes d ds idxs
- then return ([], id)
- else return (idxs, prop' idxs)
-
- -- renderWithVars (treeShow args) d (toVals idxs emptyRepl)
-
- -- extrapolateConstrs :: Replace Idx -> IO ()
- -- extrapolateConstrs idxs =
- -- if constrGen args
- -- then do putStrLn ""
- -- smartPrtLn "Extrapolating constructors ..."
- -- idxs' <- constrGen args d
- -- to
- -- else
+ idxs <- iter (qcArgs args) forest d origProp (Idx 0 0) []
+ putStrLn $ "extrap: " ++ show idxs -- YYY
+ return (idxs, prop' idxs)
where
-
forest = mkSubstForest d
prop' idxs newProp a =
- (not $ matchesShapes a (d:ds) idxs) Q.==> newProp a
-
- strategy :: Idx -- ^ Index to extrapolate
- -> [Idx] -- ^ List of generalized indices
- -> IO [Idx]
- strategy idx idxs = do
- -- In this call to iterateArb, we want to claim we can extrapolate iff at
- -- least one test passes a precondition, and for every test in which the
- -- precondition is passed, it fails. We test values of all possible sizes,
- -- up to Q.maxSize.
- tries <- iterateArb d idx (Q.maxSuccess qcargs) (Q.maxSize qcargs) origProp
+ (not $ matchesShapes a (d : ds) idxs) Q.==> newProp a
+
+ -- strategy :: Idx -- ^ Index to extrapolate
+ -- -> [Idx] -- ^ List of generalized indices
+ -- -> IO [Idx]
+ -- strategy idx idxs = do
+ -- -- In this call to iterateArb, we want to claim we can extrapolate iff at
+ -- -- least one test passes a precondition, and for every test in which the
+ -- -- precondition is passed, it fails. We test values of all possible sizes,
+ -- -- up to Q.maxSize.
+ -- tries <- iterateArb d idx (Q.maxSuccess qcargs) (Q.maxSize qcargs) origProp
- case tries of
- -- None of the tries satisfy prop. Prevent recurring down this tree,
- -- since we can generalize (we do this with sub, which replaces the
- -- subForest with []).
- FailedProp -> iter qcargs strategy (forestStop forest idx) d origProp
- idx { column = column idx + 1 }
- (idx : idxs)
- -- Either something satisfied it or the precondition couldn't be
- -- satisfied. Recurse down.
- _ -> iter qcargs strategy forest d origProp
- idx { column = column idx + 1 }
- idxs
-
- qcargs = qcArgs args
+ -- case tries of
+ -- -- None of the tries satisfy prop. Prevent recurring down this tree,
+ -- -- since we can generalize (we do this with sub, which replaces the
+ -- -- subForest with []).
+ -- FailedProp -> iter qcargs strategy (forestReplaceStop forest idx)
+ -- d origProp
+ -- idx { column = column idx + 1 }
+ -- (idx : idxs)
+ -- -- Either something satisfied it or the precondition couldn't be
+ -- -- satisfied. Recurse down.
+ -- _ -> iter qcargs strategy forest d origProp
+ -- idx { column = column idx + 1 }
+ -- idxs
+
+ -- qcargs = qcArgs args
---------------------------------------------------------------------------------
View
99 src/Test/SmartCheck/Generalize.hs
@@ -1,99 +0,0 @@
-{-# LANGUAGE Rank2Types #-}
-
-module Test.SmartCheck.Generalize
- ( iter
- ) where
-
-import Test.SmartCheck.Types
-import Test.SmartCheck.DataToTree
-import Test.SmartCheck.SmartGen
-import Test.SmartCheck.Render
-
-import qualified Test.QuickCheck as Q
-
-import Data.Tree
-
----------------------------------------------------------------------------------
-
-type Strategy = Idx -> [Idx] -> IO [Idx]
-
----------------------------------------------------------------------------------
-
--- Do a breadth-first traversal of the data, trying to replace holes. 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.
-iter :: SubTypes a
- => Q.Args -- ^ Arguments
- -> Strategy -- ^ Our generalization strategy
- -> Forest Subst -- ^ Tree representation of data
- -> a -- ^ Failed value
- -> (a -> Q.Property) -- ^ Property
- -> Idx -- ^ Starting index to extrapolate
- -> [Idx] -- ^ List of generalized indices
- -> IO [Idx]
-iter args strat forest d prop idx idxs =
- if done then return idxs
- else if nextLevel
- then iter' forest (idx { level = level idx + 1
- , column = 0 })
- idxs
- else case getIdxForest forest idx of
- Just (Node Keep _) -> strat idx idxs
- _ -> next
-
- where
- pts = breadthLevels forest
- done = length pts <= level idx
- nextLevel = length (pts !! level idx) <= column idx
-
- next = iter' forest
- idx { column = column idx + 1 }
- idxs
-
- iter' frst = iter args strat frst d prop
-
----------------------------------------------------------------------------------
-
-
----------------------------------------------------------------------------------
-
--- iter :: SubTypes a
--- => Q.Args -> Forest Subst -> a
--- -> (a -> Q.Property) -> Idx -> [Idx] -> IO [Idx]
--- iter args forest d prop idx idxs =
--- if done then return idxs
--- else if nextLevel
--- then iter' forest (idx { level = level idx + 1
--- , column = 0 })
--- idxs
--- else case getIdxForest forest idx of
--- Just (Node Keep _) -> runTest
--- _ -> next
-
--- where
--- pts = breadthLevels forest
--- done = length pts <= level idx
--- nextLevel = length (pts !! level idx) <= column idx
-
--- next = iter' forest
--- idx { column = column idx + 1 }
--- idxs
-
--- iter' frst = iter args frst d prop
-
--- runTest = do
--- -- In this call to iterateArb, we want to claim we can extrapolate iff at
--- -- least one test passes a precondition, and for every test in which the
--- -- precondition is passed, it fails. We test values of all possible sizes,
--- -- up to Q.maxSize.
--- tries <- iterateArb d idx (Q.maxSuccess args) (Q.maxSize args) prop
--- case tries of
--- -- None of the tries satisfy prop. Prevent recurring down this tree,
--- -- since we can generalize (we do this with sub, which replaces the
--- -- subForest with []).
--- FailedProp -> iter' (forestStop forest idx)
--- idx { column = column idx + 1 }
--- (idx : idxs)
--- -- Either something satisfied it or the precondition couldn't be
--- -- satisfied. Recurse down.
--- _ -> next
View
4 src/Test/SmartCheck/Render.hs
@@ -32,6 +32,7 @@ smartPrtLn = putStrLn . (smartPrefix ++)
-- | We track indicies/strings, etc. for values (subterms) and constructors
-- separately.
data Replace a = Replace { unVals :: [a], unConstrs :: [a] }
+ deriving (Show, Read, Eq)
-- emptyRepl :: Replace a
-- emptyRepl = Replace [] []
@@ -96,7 +97,8 @@ replaceWithVars format d idxs vars =
Node (rootLabel tree) (forestReplaceChop (subForest tree) idx var)
zipRepl :: [(String, Idx)]
- zipRepl = zip (unVals vars) (unVals idxs) ++ zip (unVals vars) (unVals idxs)
+ zipRepl = zip (unVals vars) (unVals idxs)
+ ++ zip (unConstrs vars) (unConstrs idxs)
---------------------------------------------------------------------------------
View
103 src/Test/SmartCheck/SmartGen.hs
@@ -5,6 +5,7 @@ module Test.SmartCheck.SmartGen
, resultify
, replace
, samples -- YYY
+ , iter
) where
import Test.SmartCheck.Types
@@ -17,6 +18,7 @@ import qualified Test.QuickCheck.Property as Q
import System.Random
import Data.List
import Data.Maybe
+import Data.Tree
import Control.Monad
---------------------------------------------------------------------------------
@@ -76,7 +78,7 @@ iterateArb d idx tries sz prop =
---------------------------------------------------------------------------------
--- | Must pass at the precondition at least once to return either FailedProp or
+-- | 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
@@ -107,6 +109,103 @@ resultify prop a = do
fs = Q.unProp $ f err err :: Q.Rose Q.Result
res = Q.protectRose . Q.reduceRose
- err = errorMsg "propify: should not evaluate."
+ err = errorMsg "resultify: should not evaluate."
+
+---------------------------------------------------------------------------------
+
+-- Do a breadth-first traversal of the data, trying to replace holes. 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.
+iter :: SubTypes a
+ => Q.Args -- ^ Arguments
+-- -> Strategy -- ^ Our generalization strategy
+ -> Forest Subst -- ^ Tree representation of data
+ -> a -- ^ Failed value
+ -> (a -> Q.Property) -- ^ Property
+ -> Idx -- ^ Starting index to extrapolate
+ -> [Idx] -- ^ List of generalized indices
+ -> IO [Idx]
+iter args forest d prop idx idxs = do -- YYY
+ putStrLn $ "iter-idx " ++ show idx
+ putStrLn $ "iter-idxs " ++ show idxs
+ if done then return idxs
+ else if nextLevel
+ then iter' forest (idx { level = level idx + 1
+ , column = 0 })
+ idxs
+ else case getIdxForest forest idx of
+ Just (Node Keep _) -> runTest
+ _ -> next
+
+ where
+ pts = breadthLevels forest
+ done = length pts <= level idx
+ nextLevel = length (pts !! level idx) <= column idx
+
+ next = iter' forest
+ idx { column = column idx + 1 }
+ idxs
+
+ iter' frst = iter args frst d prop
+
+ runTest = do
+ -- In this call to iterateArb, we want to claim we can extrapolate iff at
+ -- least one test passes a precondition, and for every test in which the
+ -- precondition is passed, it fails. We test values of all possible sizes,
+ -- up to Q.maxSize.
+ tries <- iterateArb d idx (Q.maxSuccess args) (Q.maxSize args) prop
+ case tries of
+ -- None of the tries satisfy prop. Prevent recurring down this tree,
+ -- since we can generalize (we do this with sub, which replaces the
+ -- subForest with []).
+ FailedProp -> iter' (forestReplaceStop forest idx)
+ idx { column = column idx + 1 }
+ (idx : idxs)
+ -- Either something satisfied it or the precondition couldn't be
+ -- satisfied. Recurse down.
+ _ -> next
+
+---------------------------------------------------------------------------------
+
+-- iter :: SubTypes a
+-- => Q.Args -> Forest Subst -> a
+-- -> (a -> Q.Property) -> Idx -> [Idx] -> IO [Idx]
+-- iter args forest d prop idx idxs =
+-- if done then return idxs
+-- else if nextLevel
+-- then iter' forest (idx { level = level idx + 1
+-- , column = 0 })
+-- idxs
+-- else case getIdxForest forest idx of
+-- Just (Node Keep _) -> runTest
+-- _ -> next
+
+-- where
+-- pts = breadthLevels forest
+-- done = length pts <= level idx
+-- nextLevel = length (pts !! level idx) <= column idx
+
+-- next = iter' forest
+-- idx { column = column idx + 1 }
+-- idxs
+
+-- iter' frst = iter args frst d prop
+
+-- runTest = do
+-- -- In this call to iterateArb, we want to claim we can extrapolate iff at
+-- -- least one test passes a precondition, and for every test in which the
+-- -- precondition is passed, it fails. We test values of all possible sizes,
+-- -- up to Q.maxSize.
+-- tries <- iterateArb d idx (Q.maxSuccess args) (Q.maxSize args) prop
+-- case tries of
+-- -- None of the tries satisfy prop. Prevent recurring down this tree,
+-- -- since we can generalize (we do this with sub, which replaces the
+-- -- subForest with []).
+-- FailedProp -> iter' (forestStop forest idx)
+-- idx { column = column idx + 1 }
+-- (idx : idxs)
+-- -- Either something satisfied it or the precondition couldn't be
+-- -- satisfied. Recurse down.
+-- _ -> next
---------------------------------------------------------------------------------
Please sign in to comment.
Something went wrong with that request. Please try again.