0 | module Hedgehog.Internal.Report

  2 | import Data.Lazy

  3 | import Data.Nat

  4 | import Derive.Prelude

  5 | import Hedgehog.Internal.Config

  6 | import Hedgehog.Internal.Property

  7 | import Hedgehog.Internal.Range

  8 | import Hedgehog.Internal.Util

  9 | import System.Random.Pure.StdGen

 10 | import Text.Show.Diff

 11 | import Text.PrettyPrint.Bernardy.ANSI

 13 | %default total

 15 | %language ElabReflection

 21 | public export

 22 | record FailedAnnotation where

 23 |   constructor MkFailedAnnotation

 24 |   failedValue : String

 26 | %runElab derive "FailedAnnotation" [Show,Eq]

 28 | public export

 29 | record FailureReport where

 30 |   constructor MkFailureReport

 31 |   size        : Size

 32 |   seed        : StdGen

 33 |   shrinks     : ShrinkCount

 34 |   coverage    : Maybe (Coverage CoverCount)

 35 |   annotations : List (Lazy FailedAnnotation)

 36 |   message     : String

 37 |   diff        : Maybe Diff

 38 |   footnotes   : List (Lazy String)

 40 | %runElab derive "FailureReport" [Show,Eq]

 43 | public export

 44 | data Progress = Running | Shrinking FailureReport

 46 | %runElab derive "Progress" [Show,Eq]

 52 | public export

 53 | data Result = Failed FailureReport | OK

 55 | %runElab derive "Result" [Show,Eq]

 57 | public export

 58 | isFailure : Result -> Bool

 59 | isFailure (Failed _) = True

 60 | isFailure OK         = False

 62 | public export

 63 | isSuccess : Result -> Bool

 64 | isSuccess = not . isFailure

 67 | public export

 68 | record Report a where

 69 |   constructor MkReport

 70 |   tests    : TestCount

 71 |   coverage : Coverage CoverCount

 72 |   status   : a

 74 | %runElab derive "Report" [Show,Eq]

 77 | Functor Report where

 78 |   map f = {status $= f}

 81 | Foldable Report where

 82 |   foldl f acc   = f acc . status

 83 |   foldr f acc r = f r.status acc

 84 |   null _        = False

 87 | Traversable Report where

 88 |   traverse f (MkReport t c a) = MkReport t c <$> f a

 91 | public export

 92 | record Summary where

 93 |   constructor MkSummary

 94 |   waiting : PropertyCount

 95 |   running : PropertyCount

 96 |   failed  : PropertyCount

 97 |   ok      : PropertyCount

 99 | %runElab derive "Summary" [Show,Eq,Semigroup,Monoid]

101 | record ColumnWidth where

102 |   constructor MkColumnWidth

103 |   widthPercentage : Nat

104 |   widthMinimum    : Nat

105 |   widthName       : Nat

106 |   widthNameFail   : Nat

108 | Semigroup ColumnWidth where

109 |   MkColumnWidth p0 m0 n0 f0 <+> MkColumnWidth p1 m1 n1 f1 =

110 |     MkColumnWidth (max p0 p1) (max m0 m1) (max n0 n1) (max f0 f1)

112 | Monoid ColumnWidth where

113 |   neutral = MkColumnWidth 0 0 0 0

117 | fromResult : Result -> Summary

118 | fromResult (Failed _) = { failed := 1} neutral

119 | fromResult OK         = { ok := 1} neutral

122 | summaryCompleted : Summary -> PropertyCount

123 | summaryCompleted (MkSummary _ _ x3 x4) = x3 + x4

126 | summaryTotal : Summary -> PropertyCount

127 | summaryTotal (MkSummary x1 x2 x3 x4) = x1 + x2 + x3 + x4

130 | takeAnnotation : Lazy Log -> Maybe $ Lazy FailedAnnotation

131 | takeAnnotation (Annotation x) = Just $ MkFailedAnnotation x

132 | takeAnnotation (Footnote _  ) = Nothing

133 | takeAnnotation (LogLabel _  ) = Nothing

136 | takeFootnote : Lazy Log -> Maybe $ Lazy String

137 | takeFootnote (Footnote x)   = Just x

138 | takeFootnote (Annotation _) = Nothing

139 | takeFootnote (LogLabel _)   = Nothing

142 | mkFailure :

143 |      Size

144 |   -> StdGen

145 |   -> ShrinkCount

146 |   -> Maybe (Coverage CoverCount)

147 |   -> String

148 |   -> Maybe Diff

149 |   -> List (Lazy Log)

150 |   -> FailureReport

151 | mkFailure size seed shrinks mcoverage message diff logs =

152 |   let inputs    := mapMaybe takeAnnotation logs

153 |       footnotes := mapMaybe takeFootnote logs

154 |    in MkFailureReport size seed shrinks mcoverage inputs message diff footnotes

160 | public export

161 | data MarkupStyle = StyleDefault | StyleAnnotation | StyleFailure

164 | Semigroup MarkupStyle where

165 |   StyleFailure    <+> _               = StyleFailure

166 |   _               <+> StyleFailure    = StyleFailure

167 |   StyleAnnotation <+> _               = StyleAnnotation

168 |   _               <+> StyleAnnotation = StyleAnnotation

169 |   StyleDefault    <+> _               = StyleDefault

171 | %runElab derive "MarkupStyle" [Show,Eq,Ord]

173 | public export

174 | data Markup =

175 |     WaitingIcon

176 |   | WaitingHeader

177 |   | RunningIcon

178 |   | RunningHeader

179 |   | ShrinkingIcon

180 |   | ShrinkingHeader

181 |   | FailedIcon

182 |   | FailedText

183 |   | SuccessIcon

184 |   | SuccessText

185 |   | CoverageIcon

186 |   | CoverageText

187 |   | CoverageFill

188 |   | StyledBorder MarkupStyle

189 |   | AnnotationValue

190 |   | DiffPrefix

191 |   | DiffInfix

192 |   | DiffSuffix

193 |   | DiffSame

194 |   | DiffRemoved

195 |   | DiffAdded

196 |   | ReproduceHeader

197 |   | ReproduceGutter

198 |   | ReproduceSource

200 | %runElab derive "Markup" [Show,Eq,Ord]

202 | color : Color -> List SGR

203 | color c = [SetForeground c]

205 | toAnsi : Markup -> List SGR

206 | toAnsi (StyledBorder StyleAnnotation) = []

207 | toAnsi (StyledBorder StyleDefault)    = []

208 | toAnsi (StyledBorder StyleFailure)    = []

209 | toAnsi AnnotationValue                = color Magenta

210 | toAnsi CoverageFill                   = color BrightBlack

211 | toAnsi CoverageIcon                   = color Yellow

212 | toAnsi CoverageText                   = color Yellow

213 | toAnsi DiffAdded                      = color Green

214 | toAnsi DiffInfix                      = []

215 | toAnsi DiffPrefix                     = []

216 | toAnsi DiffRemoved                    = color Red

217 | toAnsi DiffSame                       = []

218 | toAnsi DiffSuffix                     = []

219 | toAnsi FailedIcon                     = color BrightRed

220 | toAnsi FailedText                     = color BrightRed

221 | toAnsi ReproduceGutter                = []

222 | toAnsi ReproduceHeader                = []

223 | toAnsi ReproduceSource                = []

224 | toAnsi RunningHeader                  = []

225 | toAnsi RunningIcon                    = []

226 | toAnsi ShrinkingHeader                = color BrightRed

227 | toAnsi ShrinkingIcon                  = color BrightRed

228 | toAnsi SuccessIcon                    = color Green

229 | toAnsi SuccessText                    = color Green

230 | toAnsi WaitingHeader                  = []

231 | toAnsi WaitingIcon                    = []

233 | testCount : TestCount -> String

234 | testCount (MkTagged 1) = "1 test"

235 | testCount (MkTagged n) = show n ++ " tests"

237 | shrinkCount : ShrinkCount -> String

238 | shrinkCount (MkTagged 1) = "1 shrink"

239 | shrinkCount (MkTagged n) = show n ++ " shrinks"

241 | %inline propertyCount : PropertyCount -> String

242 | propertyCount (MkTagged n) = show n

244 | renderCoverPercentage : CoverPercentage -> String

245 | renderCoverPercentage p =

246 |   show (round {a = Double} (p.asDouble * 10.0) / 10.0) ++ "%"

248 | labelWidth : TestCount -> Label CoverCount -> ColumnWidth

249 | labelWidth tests x =

250 |   let percentage :=

251 |         length . renderCoverPercentage $

252 |         coverPercentage tests x.labelAnnotation

254 |       minimum :=

255 |         if x.labelMinimum == 0

256 |            then the Nat 0

257 |            else length . renderCoverPercentage $ x.labelMinimum

259 |       name := length . unTag $ x.labelName

261 |       nameFail = if labelCovered tests x then the Nat 0 else name

263 |   in MkColumnWidth percentage minimum name nameFail

265 | coverageWidth : TestCount -> Coverage CoverCount -> ColumnWidth

266 | coverageWidth tests = concatMap (labelWidth tests) . labels

268 | full : Char

269 | full = '█'

271 | parts : List Char

272 | parts = ['·', '▏','▎','▍','▌','▋','▊','▉']

274 | parameters {opts : LayoutOpts} (useColor : UseColor)

275 |   markup : Markup -> Doc opts -> Doc opts

276 |   markup m d = case useColor of

277 |     DisableColor => d

278 |     EnableColor  => decorate (toAnsi m) d

280 |   %inline markupLine : Markup -> String -> Doc opts

281 |   markupLine m = markup m . line

283 |   gutter : Markup -> Doc opts -> Doc opts

284 |   gutter m x = markup m rangle <++> x

286 |   icon : Markup -> Char -> Doc opts -> Doc opts

287 |   icon m i x = markup m (symbol i) <++> x

289 |   lineDiff : LineDiff -> Doc opts

290 |   lineDiff (LineSame x)    = markup DiffSame    $ "  " <+> pretty x

291 |   lineDiff (LineRemoved x) = markup DiffRemoved $ "- " <+> pretty x

292 |   lineDiff (LineAdded x)   = markup DiffAdded   $ "+ " <+> pretty x

294 |   diff : Diff -> List (Doc opts)

295 |   diff (MkDiff pre removed inf added suffix df) =

296 |     ( markup DiffPrefix (line pre)      <+>

297 |       markup DiffRemoved (line removed) <+>

298 |       markup DiffInfix (line inf)       <+>

299 |       markup DiffAdded (line added)     <+>

300 |       markup DiffSuffix (line suffix)

301 |     ) :: map lineDiff (toLineDiff df)

303 |   reproduce : Maybe PropertyName -> Size -> StdGen -> Doc opts

304 |   reproduce name size seed =

305 |     let prop  := line $ maybe "<property>" unTag name

306 |         instr := prettyCon Open "recheck" [prettyArg size, prettyArg seed, prop]

307 |      in vsep

308 |           [ markupLine ReproduceHeader "This failure can be reproduced by running:"

309 |           , gutter ReproduceGutter $ markup ReproduceSource instr

310 |           ]

312 |   textLines : String -> List (Doc opts)

313 |   textLines = map line . lines

315 |   failedInput : Nat -> FailedAnnotation -> Doc opts

316 |   failedInput ix (MkFailedAnnotation val) =

317 |     vsep

318 |       [ line "forAll \{show ix} ="

319 |       , indent 2 . vsep . map (markup AnnotationValue . line) $ lines val

320 |       ]

322 |   failureReport :

323 |        Maybe PropertyName

324 |     -> TestCount

325 |     -> FailureReport

326 |     -> List (Doc opts)

327 |   failureReport nm tests (MkFailureReport si se _ mcover inputs msg mdiff msgs0) =

328 |       whenSome (empty ::)

329 |     . whenSome (++ [empty])

330 |     . intersperse empty

331 |     . map (vsep . map (indent 2))

332 |     . filter (\xs => not $ null xs)

333 |     $ [intersperse empty args, coverage, docs, bottom]

335 |     where

336 |       whenSome : Foldable t => (t a -> t a) -> t a -> t a

337 |       whenSome f xs = if null xs then xs else f xs

339 |       bottom : List (Doc opts)

340 |       bottom = maybe [reproduce nm si se] (const Nil) mcover

342 |       docs : List (Doc opts)

343 |       docs =

344 |         concatMap

345 |           textLines

346 |           (map force msgs0 ++ if msg == "" then [] else [msg])

347 |         <+> maybe [] diff mdiff

349 |       args : List (Doc opts)

350 |       args = zipWith failedInput [0 .. length inputs] (reverse $ map force inputs)

352 |       coverage : List (Doc opts)

353 |       coverage =

354 |         case mcover of

355 |           Nothing => []

356 |           Just c  => do

357 |             MkLabel _ _ count <- coverageFailures tests c

358 |             pure $

359 |                   line "Failed ("

360 |               <+> markupLine CoverageText

361 |                     (renderCoverPercentage (coverPercentage tests count))

362 |               <+> " coverage)"

364 |   ppName : Maybe PropertyName -> Doc opts

365 |   ppName Nothing                = "<interactive>"

366 |   ppName (Just $ MkTagged name) = text name

368 |   leftPad : Nat -> Doc opts -> Doc opts

369 |   leftPad n doc = doc >>= \l => pure $ indent (n `minus` width l) l

371 |   coverBar : CoverPercentage -> CoverPercentage -> Doc opts

372 |   coverBar percentage minimum =

373 |     let barWidth         := the Nat 20

374 |         coverageRatio    := percentage.asDouble / 100.0

375 |         coverageWidth    := toNat . floor $ coverageRatio * cast barWidth

376 |         minimumRatio     := minimum.asDouble / 100.0

377 |         minimumWidth     := toNat . floor $ minimumRatio * cast barWidth

378 |         fillWidth        := barWidth `minus` S coverageWidth

379 |         fillErrorWidth   := minimumWidth `minus` S coverageWidth

380 |         fillSurplusWidth := fillWidth `minus` fillErrorWidth

382 |         ix :=

383 |           toNat . floor $

384 |           ((coverageRatio * cast barWidth) - cast coverageWidth) *

385 |           cast (length parts)

387 |         part :=

388 |           symbol $

389 |             case inBounds ix parts of

390 |               Yes ib => index ix parts

391 |               No  _  => head parts

393 |      in hcat [ line $ replicate coverageWidth full

394 |              , if coverageWidth < barWidth then

395 |                  if ix == 0 then

396 |                    if fillErrorWidth > 0 then markup FailedText part

397 |                    else markup CoverageFill part

398 |                  else part

399 |                else empty

400 |              , markupLine FailedText $ replicate fillErrorWidth (head parts)

401 |              , markupLine CoverageFill $ replicate fillSurplusWidth (head parts)

402 |              ]

404 |   label : TestCount -> ColumnWidth -> Label CoverCount -> Doc opts

405 |   label tests w x@(MkLabel name minimum count) =

406 |     let covered  := labelCovered tests x

407 |         ltext    := if not covered then markup CoverageText else id

408 |         lborder  := markup (StyledBorder StyleDefault)

409 |         licon    := if not covered then markup CoverageText "⚠ " else "  "

410 |         lname    := padRight (cast w.widthName) ' ' (unTag name)

411 |         wminimum := leftPad w.widthMinimum . line $ renderCoverPercentage minimum

412 |         lcover   := wcover

414 |         lminimum =

415 |           if w.widthMinimum == 0 then empty

416 |           else if not covered then " ✗ " <+> wminimum

417 |           else if minimum == 0 then "   " <+> leftPad w.widthMinimum ""

418 |           else " ✓ " <+> wminimum

421 |      in hcat

422 |           [ licon

423 |           , ltext (line lname)

424 |           , lborder " "

425 |           , ltext lcover

426 |           , lborder " "

427 |           , ltext $ coverBar (coverPercentage tests count) minimum

428 |           , lborder ""

429 |           , ltext lminimum

430 |           ]

433 |     where wcover : Doc opts

434 |           wcover =

435 |             leftPad w.widthPercentage . line $

436 |             renderCoverPercentage (coverPercentage tests count)

438 |   coverage : TestCount -> Coverage CoverCount -> List (Doc opts)

439 |   coverage tests x = map (label tests (coverageWidth tests x)) $ labels x

441 |   whenNonZero : Doc opts -> PropertyCount -> Maybe (Doc opts)

442 |   whenNonZero _      0 = Nothing

443 |   whenNonZero suffix n = Just $ line (propertyCount n) <++> suffix

445 |   export

446 |   ppProgress : Maybe PropertyName -> Report Progress -> Doc opts

447 |   ppProgress name (MkReport tests cov status) =

448 |     case status of

449 |        Running =>

450 |          vsep $

451 |            [ icon RunningIcon '●' . markup RunningHeader $

452 |              ppName name <++> line "passed \{testCount tests} (running)"

453 |            ] ++ coverage tests cov

455 |        Shrinking failure =>

456 |          icon ShrinkingIcon '↯' . markup ShrinkingHeader $

457 |            ppName name <++> line "failed after \{testCount tests}"

459 |   annotateSummary : Summary -> Doc opts -> Doc opts

460 |   annotateSummary summary =

461 |     if summary.failed > 0 then

462 |       icon FailedIcon '✗' . markup FailedText

463 |     else if summary.waiting > 0 || summary.running > 0 then

464 |       icon WaitingIcon '○' . markup WaitingHeader

465 |     else

466 |       icon SuccessIcon '✓' . markup SuccessText

468 |   ppResult : Maybe PropertyName -> Report Result -> Doc opts

469 |   ppResult name (MkReport tests cov result) =

470 |     case result of

471 |       Failed failure =>

472 |         vsep $

473 |         [ icon FailedIcon '✗' . markup FailedText $

474 |           ppName name <++>

475 |           line "failed after \{testCount tests}."

476 |         ] ++

477 |         coverage tests cov ++

478 |         failureReport name tests failure

480 |       OK =>

481 |         vsep $

482 |           [ icon SuccessIcon '✓' . markup SuccessText $

483 |             ppName name <++> line "passed \{testCount tests}."

484 |           ] ++

485 |           coverage tests cov

487 |   export

488 |   ppSummary : Summary -> Doc opts

489 |   ppSummary summary =

490 |     let complete := summaryCompleted summary == summaryTotal summary

491 |         suffix   := if complete then line "." else line " (running)"

493 |      in annotateSummary summary .

494 |           (<+> suffix)

495 |         . hcat

496 |         . addPrefix complete

497 |         . intersperse (line ", ")

498 |         $ catMaybes [

499 |             whenNonZero "failed" summary.failed

500 |           , if complete then

501 |               whenNonZero "succeeded" summary.ok

502 |             else

503 |               Nothing

504 |         ]

506 |     where

507 |       doPrefix : Bool -> Doc opts -> Doc opts

508 |       doPrefix True _    = empty

509 |       doPrefix False end =

510 |         let pc1 := propertyCount (summaryCompleted summary)

511 |             pc2 := propertyCount (summaryTotal summary)

512 |          in line "\{pc1} / \{pc2} complete" <+> end

514 |       addPrefix : Bool -> List (Doc opts) -> List (Doc opts)

515 |       addPrefix complete [] = [doPrefix complete empty]

516 |       addPrefix complete xs = doPrefix complete ": " :: xs

518 | public export

519 | LL80 : LayoutOpts

520 | LL80 = Opts 80

523 | renderDoc : Doc LL80 -> String

524 | renderDoc = render LL80 . indent 2

527 | renderProgress : UseColor -> Maybe PropertyName -> Report Progress -> String

528 | renderProgress color name = renderDoc . ppProgress color name

531 | renderResult : UseColor -> Maybe PropertyName -> Report Result -> String

532 | renderResult color name = renderDoc . ppResult color name

535 | renderSummary : UseColor -> Summary -> String

536 | renderSummary color = renderDoc . ppSummary color

543 | report :

544 |      (aborted : Bool)

545 |   -> TestCount

546 |   -> Size

547 |   -> StdGen

548 |   -> Coverage CoverCount

549 |   -> Maybe Confidence

550 |   -> Report Result

551 | report aborted tests size seed cover conf =

552 |   let failureReport := \msg =>

553 |         MkReport tests cover . Failed $

554 |           mkFailure size seed 0 (Just cover) msg Nothing []

556 |       coverageReached := successVerified tests cover conf

558 |       labelsCovered := coverageSuccess tests cover

560 |       successReport := MkReport tests cover OK

562 |       confidenceReport =

563 |         if coverageReached && labelsCovered

564 |            then successReport

565 |            else

566 |              failureReport

567 |                "Test coverage cannot be reached after \{tests} tests"

569 |   in if aborted then confidenceReport

570 |      else if labelsCovered then successReport

571 |      else

572 |        failureReport $

573 |          "Labels not sufficently covered after \{tests} tests"