-
Notifications
You must be signed in to change notification settings - Fork 2
/
Reduce.hs
120 lines (104 loc) · 4.61 KB
/
Reduce.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
{-# LANGUAGE ScopedTypeVariables #-}
module Test.SmartCheck.Reduce
(smartRun
) where
import Test.SmartCheck.Types
import Test.SmartCheck.Common
import Test.SmartCheck.DataToTree
import Test.SmartCheck.Render
import qualified Test.QuickCheck as Q
import Data.Tree
import Data.Typeable
---------------------------------------------------------------------------------
-- 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
=> Q.Args -> Maybe a -> (a -> Q.Property) -> IO (Maybe a)
smartRun args res prop =
case res of
Just res' -> runSmart res'
Nothing -> do putStrLn ""
smartPrtLn "No value to smart-shrink; done."
return Nothing
where
runSmart r = do
putStrLn ""
smartPrtLn "Smart Shrinking ... "
new <- smartShrink args r prop
smartPrtLn "Smart-shrunk value:"
print new
return (Just 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 :: SubTypes a => Q.Args -> a -> (a -> Q.Property) -> IO a
smartShrink args d prop = iterReduce args d (Idx 0 0) notProp
where
notProp = Q.expectFailure . prop
iterReduce :: SubTypes a => Q.Args -> a -> Idx -> (a -> Q.Property) -> IO a
iterReduce args d idx prop =
if done then return d
else if nextLevel
then iterReduce args d idx { column = 0
, level = level idx + 1 }
prop
else case maxSize of
Nothing -> iterReduce args d (idx { column = column idx + 1 })
prop
-- 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 -> iterReduce args d
-- (idx { column = column idx + 1 })
-- prop
-- Just v -> mkVals v
-- Invariant: ms should be => 1.
Just ms -> mkTry args d idx prop ms
where
-- Extract a tree from a forest and make sure it's big enough to test.
maxSize = case getIdxForest forest idx of
Nothing -> Nothing
Just t -> let dep = depth (subForest t) in
if dep <= 1 then Nothing
else Just (dep-1)
forest = mkSubstForest d
pts = breadthLevels forest
done = length pts <= level idx
nextLevel = length (pts !! level idx) <= column idx
---------------------------------------------------------------------------------
mkTry :: forall a. SubTypes a
=> Q.Args -> a -> Idx -> (a -> Q.Property) -> Int -> IO a
mkTry args d idx prop maxSize = do
v <- mv
case v of
-- This sees if some subterm directly fails the property. If so, we'll take
-- it, if it's well-typed.
Just v' -> iterReduce args v' (Idx 0 0) prop
Nothing -> do
try <- iterateArb d idx (Q.maxDiscard args) maxSize prop
case try of
-- Found a try that fails prop. We'll now test try, and start trying to
-- reduce from the top!
Result x -> iterReduce args x (Idx 0 0) prop
-- Either couldn't satisfy the precondition or nothing satisfied the
-- property. Either way, we can't shrink it.
_ -> iterReduce args d (idx { column = column idx + 1 }) prop
where
mv = case getAtIdx d idx of
Nothing -> error "unexpected failure: getAtIdx mkTry"
Just v -> testHole v
testHole :: SubT -> IO (Maybe a)
testHole SubT { unSubT = v } =
case cast v :: Maybe a of
Nothing -> return Nothing
-- FailedPreCond is just seeding extractResult, a folding operator.
Just x -> do res <- extractResult prop FailedPreCond x
case res of
-- This is a failed value strictly smaller. Let's test
-- starting from here.
Result y -> return (Just y)
_ -> return Nothing
---------------------------------------------------------------------------------