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 | ||| The low-level runner behind `check`, returning the full `Report Result`.
 72 | export
 73 | checkReport :
 74 |      {auto _ : Monad m}
 75 |   -> PropertyConfig
 76 |   -> Maybe Size
 77 |   -> StdGen
 78 |   -> PropertyT ()
 79 |   -> (Report Progress -> m ())
 80 |   -> m (Report Result)
 81 | checkReport cfg si0 se0 test updateUI =
 82 |   let (conf, MkTagged numTests, initSz) := unCriteria cfg.terminationCriteria
 83 |    in loop numTests 0 (fromMaybe initSz si0) se0 neutral conf
 84 |
 85 |   where
 86 |     loop :
 87 |          Nat
 88 |       -> TestCount
 89 |       -> Size
 90 |       -> StdGen
 91 |       -> Coverage CoverCount
 92 |       -> Maybe Confidence
 93 |       -> m (Report Result)
 94 |     loop n tests si se cover conf = do
 95 |       updateUI (MkReport tests cover Running)
 96 |       case n of
 97 |         0   =>
 98 |           -- required number of tests run
 99 |           pure $ report False tests si se cover conf
100 |         S k =>
101 |           if abortEarly cfg.terminationCriteria tests cover conf
102 |              then
103 |                -- at this point we know that enough
104 |                -- tests have been run due to early termination
105 |                pure $ report True tests si se cover conf
106 |              else
107 |               -- run another test
108 |               let (s0,s1) := split se
109 |                   tr      := runGen si s0 $ runTestT test
110 |                   nextSize = if si < maxSize then (si + 1) else 0
111 |                in case tr.value of
112 |                     -- the test failed, so we abort and shrink
113 |                     (Left x, _)  =>
114 |                       let upd := updateUI . MkReport (tests+1) cover
115 |                        in map (MkReport (tests+1) cover) $
116 |                             takeSmallest si se cfg.shrinkLimit upd tr
117 |
118 |                     -- the test succeeded, so we accumulate results
119 |                     -- and loop once more
120 |                     (Right x, journal) =>
121 |                       let cover1 := journalCoverage journal <+> cover
122 |                        in loop k (tests + 1) nextSize s1 cover1 conf
123 |
124 | checkTerm :
125 |      {auto _ : HasTerminal m}
126 |   -> {auto _ : Monad m}
127 |   -> Terminal m
128 |   -> UseColor
129 |   -> Maybe PropertyName
130 |   -> Maybe Size
131 |   -> StdGen
132 |   -> Property
133 |   -> m (Report Result)
134 | checkTerm term color name si se prop = do
135 |   result <- checkReport {m} prop.config si se prop.test $
136 |     \prog =>
137 |        when (multOf100 prog.tests) $
138 |          let ppprog := renderProgress color name prog
139 |           in case prog.status of
140 |                Running     => putTmp term ppprog
141 |                Shrinking _ => putTmp term ppprog
142 |
143 |   putOut term (renderResult color name result)
144 |   pure result
145 |
146 | checkWith :
147 |      {auto _ : CanInitSeed StdGen m}
148 |   -> {auto _ : HasTerminal m}
149 |   -> {auto _ : Monad m}
150 |   -> Terminal m
151 |   -> UseColor
152 |   -> Maybe PropertyName
153 |   -> Property
154 |   -> m (Report Result)
155 | checkWith term color name prop =
156 |   initSeed >>= \se => checkTerm term color name Nothing se prop
157 |
158 | ||| Check a property.
159 | export
160 | checkNamed :
161 |      {auto _ : CanInitSeed StdGen m}
162 |   -> {auto _ : HasConfig m}
163 |   -> {auto _ : HasTerminal m}
164 |   -> {auto _ : Monad m}
165 |   -> PropertyName
166 |   -> Property
167 |   -> m Bool
168 | checkNamed name prop = do
169 |   color <- detectColor
170 |   term  <- console
171 |   rep   <- checkWith term color (Just name) prop
172 |   pure $ rep.status == OK
173 |
174 | ||| Check a property.
175 | export
176 | check :
177 |      {auto _ : CanInitSeed StdGen m}
178 |   -> {auto _ : HasConfig m}
179 |   -> {auto _ : HasTerminal m}
180 |   -> {auto _ : Monad m}
181 |   -> Property
182 |   -> m Bool
183 | check prop = do
184 |   color <- detectColor
185 |   term  <- console
186 |   rep   <- checkWith term color Nothing prop
187 |   pure $ rep.status == OK
188 |
189 | ||| Check a property using a specific size and seed.
190 | export
191 | recheck :
192 |      {auto _ : HasConfig m}
193 |   -> {auto _ : HasTerminal m}
194 |   -> {auto _ : Monad m}
195 |   -> Size
196 |   -> StdGen
197 |   -> Property
198 |   -> m ()
199 | recheck si se prop = do
200 |   color <- detectColor
201 |   term  <- console
202 |   let prop = noVerifiedTermination $ withTests 1 prop
203 |   _     <- checkTerm term color Nothing (Just si) se prop
204 |   pure ()
205 |
206 | checkGroupWith :
207 |      {auto _ : CanInitSeed StdGen m}
208 |   -> {auto _ : HasTerminal m}
209 |   -> {auto _ : Monad m}
210 |   -> Terminal m
211 |   -> UseColor
212 |   -> List (PropertyName, Property)
213 |   -> m Summary
214 | checkGroupWith term color = run neutral
215 |
216 |   where
217 |     run : Summary -> List (PropertyName, Property) -> m Summary
218 |     run s [] = pure s
219 |     run s ((pn,p) :: ps) = do
220 |       rep  <- checkWith term color (Just pn) p
221 |       run (s <+> fromResult rep.status) ps
222 |
223 | export
224 | checkGroup :
225 |      {auto _ : CanInitSeed StdGen m}
226 |   -> {auto _ : HasConfig m}
227 |   -> {auto _ : HasTerminal m}
228 |   -> {auto _ : Monad m}
229 |   -> Group
230 |   -> m Bool
231 | checkGroup (MkGroup group props) = do
232 |   term    <- console
233 |   putOut term $ "━━━ " ++ unTag group ++ " ━━━\n"
234 |   color   <- detectColor
235 |   summary <- checkGroupWith term color props
236 |   putOut term (renderSummary color summary)
237 |   pure $ summary.failed == 0
238 |
239 | ||| Simple test runner.
240 | |||
241 | ||| Use this in a `main` function in order to test a list of
242 | ||| property groups. The runner will take into account several
243 | ||| command line arguments in order to adjust the number of
244 | ||| tests to be run for each property, the maximal number of
245 | ||| shrinks and the confidence value to use.
246 | |||
247 | ||| ```idris example
248 | ||| main : IO ()
249 | ||| main = test myGroups
250 | ||| ```
251 | |||
252 | ||| The resulting executable can then be run as follows:
253 | |||
254 | ||| ```sh
255 | ||| build/exec/runTests -n 1000
256 | ||| ```
257 | |||
258 | ||| It will fail with an exit code of 1 if at least one property
259 | ||| fails.
260 | export
261 | test : HasIO io => List Group -> io ()
262 | test gs = do
263 |   args    <- getArgs
264 |   Right c <- pure $ applyArgs args
265 |     | Left errs => do
266 |         putStrLn "Errors when parsing command line args:"
267 |         traverse_ putStrLn errs
268 |         exitFailure
269 |   if c.printHelp
270 |      then putStrLn info >> exitSuccess
271 |      else
272 |        let gs2 := map (applyConfig c) gs
273 |         in do
274 |              res <- foldlM (\b,g => map (b &&) (checkGroup g)) True gs2
275 |              if res
276 |                 then exitSuccess
277 |                 else putStrLn "\n\nSome tests failed" >> exitFailure
278 |