0 | module Hedgehog.Internal.Runner
  1 |
  2 | import Data.Colist
  3 | import Data.Cotree
  4 | import Data.Maybe
  5 | import Hedgehog.Internal.Config
  6 | import Hedgehog.Internal.Gen
  7 | import Hedgehog.Internal.Options
  8 | import Hedgehog.Internal.Property
  9 | import Hedgehog.Internal.Range
 10 | import Hedgehog.Internal.Report
 11 | import Hedgehog.Internal.Terminal
 12 | import System
 13 | import System.Random.Pure.StdGen
 14 |
 15 | %default total
 16 |
 17 | public export
 18 | TestRes : Type
 19 | TestRes = (Either Failure (), Journal)
 20 |
 21 | --------------------------------------------------------------------------------
 22 | --          Shrinking
 23 | --------------------------------------------------------------------------------
 24 |
 25 | -- Shrinking
 26 | shrink : Monad m => Nat -> Coforest a -> b -> (Nat -> a -> m (Maybe b)) -> m b
 27 | shrink _     []        b _ = pure b
 28 | shrink 0 _             b _ = pure b
 29 | shrink (S k) (t :: ts) b f = do
 30 |   Just b2 <- f (S k) t.value | Nothing => shrink k ts b f
 31 |   shrink k t.forest b2 f
 32 |
 33 | takeSmallest :
 34 |      {auto _ : Monad m}
 35 |   -> Size
 36 |   -> StdGen
 37 |   -> ShrinkLimit
 38 |   -> (Progress -> m ())
 39 |   -> Cotree TestRes
 40 |   -> m Result
 41 | takeSmallest si se (MkTagged slimit) updateUI t = do
 42 |   res <- run 0 t.value
 43 |   if isFailure res
 44 |      then shrink slimit t.forest res runMaybe
 45 |      else pure res
 46 |
 47 |   where
 48 |     -- calc number of shrinks from the remaining
 49 |     -- allowed numer and the shrink limit
 50 |     calcShrinks : Nat -> ShrinkCount
 51 |     calcShrinks rem = MkTagged $ (slimit `minus` rem) + 1
 52 |
 53 |     run : ShrinkCount -> TestRes -> m Result
 54 |     run shrinks t =
 55 |       case t of
 56 |         (Left $ MkFailure err diff, MkJournal logs) =>
 57 |            let fail = mkFailure si se shrinks Nothing err diff (reverse logs)
 58 |             in updateUI (Shrinking fail) $> Failed fail
 59 |
 60 |         (Right x, _) => pure OK
 61 |
 62 |     runMaybe : Nat -> TestRes -> m (Maybe Result)
 63 |     runMaybe shrinksLeft testRes = do
 64 |       res <- run (calcShrinks shrinksLeft) testRes
 65 |       if isFailure res then pure (Just res) else pure Nothing
 66 |
 67 | --------------------------------------------------------------------------------
 68 | --          Test Runners
 69 | --------------------------------------------------------------------------------
 70 |
 71 | -- main test runner
 72 | checkReport :
 73 |      {auto _ : Monad m}
 74 |   -> PropertyConfig
 75 |   -> Maybe Size
 76 |   -> StdGen
 77 |   -> PropertyT ()
 78 |   -> (Report Progress -> m ())
 79 |   -> m (Report Result)
 80 | checkReport cfg si0 se0 test updateUI =
 81 |   let (conf, MkTagged numTests, initSz) := unCriteria cfg.terminationCriteria
 82 |    in loop numTests 0 (fromMaybe initSz si0) se0 neutral conf
 83 |
 84 |   where
 85 |     loop :
 86 |          Nat
 87 |       -> TestCount
 88 |       -> Size
 89 |       -> StdGen
 90 |       -> Coverage CoverCount
 91 |       -> Maybe Confidence
 92 |       -> m (Report Result)
 93 |     loop n tests si se cover conf = do
 94 |       updateUI (MkReport tests cover Running)
 95 |       case n of
 96 |         0   =>
 97 |           -- required number of tests run
 98 |           pure $ report False tests si se cover conf
 99 |         S k =>
100 |           if abortEarly cfg.terminationCriteria tests cover conf
101 |              then
102 |                -- at this point we know that enough
103 |                -- tests have been run due to early termination
104 |                pure $ report True tests si se cover conf
105 |              else
106 |               -- run another test
107 |               let (s0,s1) := split se
108 |                   tr      := runGen si s0 $ runTestT test
109 |                   nextSize = if si < maxSize then (si + 1) else 0
110 |                in case tr.value of
111 |                     -- the test failed, so we abort and shrink
112 |                     (Left x, _)  =>
113 |                       let upd := updateUI . MkReport (tests+1) cover
114 |                        in map (MkReport (tests+1) cover) $
115 |                             takeSmallest si se cfg.shrinkLimit upd tr
116 |
117 |                     -- the test succeeded, so we accumulate results
118 |                     -- and loop once more
119 |                     (Right x, journal) =>
120 |                       let cover1 := journalCoverage journal <+> cover
121 |                        in loop k (tests + 1) nextSize s1 cover1 conf
122 |
123 | checkTerm :
124 |      {auto _ : HasTerminal m}
125 |   -> {auto _ : Monad m}
126 |   -> Terminal m
127 |   -> UseColor
128 |   -> Maybe PropertyName
129 |   -> Maybe Size
130 |   -> StdGen
131 |   -> Property
132 |   -> m (Report Result)
133 | checkTerm term color name si se prop = do
134 |   result <- checkReport {m} prop.config si se prop.test $
135 |     \prog =>
136 |        when (multOf100 prog.tests) $
137 |          let ppprog := renderProgress color name prog
138 |           in case prog.status of
139 |                Running     => putTmp term ppprog
140 |                Shrinking _ => putTmp term ppprog
141 |
142 |   putOut term (renderResult color name result)
143 |   pure result
144 |
145 | checkWith :
146 |      {auto _ : CanInitSeed StdGen m}
147 |   -> {auto _ : HasTerminal m}
148 |   -> {auto _ : Monad m}
149 |   -> Terminal m
150 |   -> UseColor
151 |   -> Maybe PropertyName
152 |   -> Property
153 |   -> m (Report Result)
154 | checkWith term color name prop =
155 |   initSeed >>= \se => checkTerm term color name Nothing se prop
156 |
157 | ||| Check a property.
158 | export
159 | checkNamed :
160 |      {auto _ : CanInitSeed StdGen m}
161 |   -> {auto _ : HasConfig m}
162 |   -> {auto _ : HasTerminal m}
163 |   -> {auto _ : Monad m}
164 |   -> PropertyName
165 |   -> Property
166 |   -> m Bool
167 | checkNamed name prop = do
168 |   color <- detectColor
169 |   term  <- console
170 |   rep   <- checkWith term color (Just name) prop
171 |   pure $ rep.status == OK
172 |
173 | ||| Check a property.
174 | export
175 | check :
176 |      {auto _ : CanInitSeed StdGen m}
177 |   -> {auto _ : HasConfig m}
178 |   -> {auto _ : HasTerminal m}
179 |   -> {auto _ : Monad m}
180 |   -> Property
181 |   -> m Bool
182 | check prop = do
183 |   color <- detectColor
184 |   term  <- console
185 |   rep   <- checkWith term color Nothing prop
186 |   pure $ rep.status == OK
187 |
188 | ||| Check a property using a specific size and seed.
189 | export
190 | recheck :
191 |      {auto _ : HasConfig m}
192 |   -> {auto _ : HasTerminal m}
193 |   -> {auto _ : Monad m}
194 |   -> Size
195 |   -> StdGen
196 |   -> Property
197 |   -> m ()
198 | recheck si se prop = do
199 |   color <- detectColor
200 |   term  <- console
201 |   let prop = noVerifiedTermination $ withTests 1 prop
202 |   _     <- checkTerm term color Nothing (Just si) se prop
203 |   pure ()
204 |
205 | checkGroupWith :
206 |      {auto _ : CanInitSeed StdGen m}
207 |   -> {auto _ : HasTerminal m}
208 |   -> {auto _ : Monad m}
209 |   -> Terminal m
210 |   -> UseColor
211 |   -> List (PropertyName, Property)
212 |   -> m Summary
213 | checkGroupWith term color = run neutral
214 |
215 |   where
216 |     run : Summary -> List (PropertyName, Property) -> m Summary
217 |     run s [] = pure s
218 |     run s ((pn,p) :: ps) = do
219 |       rep  <- checkWith term color (Just pn) p
220 |       run (s <+> fromResult rep.status) ps
221 |
222 | export
223 | checkGroup :
224 |      {auto _ : CanInitSeed StdGen m}
225 |   -> {auto _ : HasConfig m}
226 |   -> {auto _ : HasTerminal m}
227 |   -> {auto _ : Monad m}
228 |   -> Group
229 |   -> m Bool
230 | checkGroup (MkGroup group props) = do
231 |   term    <- console
232 |   putOut term $ "━━━ " ++ unTag group ++ " ━━━\n"
233 |   color   <- detectColor
234 |   summary <- checkGroupWith term color props
235 |   putOut term (renderSummary color summary)
236 |   pure $ summary.failed == 0
237 |
238 | ||| Simple test runner.
239 | |||
240 | ||| Use this in a `main` function in order to test a list of
241 | ||| property groups. The runner will take into account several
242 | ||| command line arguments in order to adjust the number of
243 | ||| tests to be run for each property, the maximal number of
244 | ||| shrinks and the confidence value to use.
245 | |||
246 | ||| ```idris example
247 | ||| main : IO ()
248 | ||| main = test myGroups
249 | ||| ```
250 | |||
251 | ||| The resulting executable can then be run as follows:
252 | |||
253 | ||| ```sh
254 | ||| build/exec/runTests -n 1000
255 | ||| ```
256 | |||
257 | ||| It will fail with an exit code of 1 if at least one property
258 | ||| fails.
259 | export
260 | test : HasIO io => List Group -> io ()
261 | test gs = do
262 |   args    <- getArgs
263 |   Right c <- pure $ applyArgs args
264 |     | Left errs => do
265 |         putStrLn "Errors when parsing command line args:"
266 |         traverse_ putStrLn errs
267 |         exitFailure
268 |   if c.printHelp
269 |      then putStrLn info >> exitSuccess
270 |      else
271 |        let gs2 := map (applyConfig c) gs
272 |         in do
273 |              res <- foldlM (\b,g => map (b &&) (checkGroup g)) True gs2
274 |              if res
275 |                 then exitSuccess
276 |                 else putStrLn "\n\nSome tests failed" >> exitFailure
277 |