0 | module Hedgehog.Internal.Property

  2 | import Control.Monad.Either

  3 | import Control.Monad.Identity

  4 | import Control.Monad.Trans

  5 | import Control.Monad.Writer

  6 | import Data.Lazy

  7 | import Data.List.Quantifiers

  8 | import public Data.Double.Bounded

  9 | import Data.DPair

 10 | import Derive.Prelude

 11 | import Hedgehog.Internal.Gen

 12 | import Hedgehog.Internal.Range

 13 | import Hedgehog.Internal.Util

 14 | import Statistics.Confidence

 15 | import Text.Show.Diff

 16 | import Text.Show.Pretty

 18 | %language ElabReflection

 20 | %default total

 26 | public export

 27 | data Tag =

 28 |     ConfidenceTag

 29 |   | CoverCountTag

 30 |   | GroupNameTag

 31 |   | LabelNameTag

 32 |   | PropertyCountTag

 33 |   | PropertyNameTag

 34 |   | ShrinkCountTag

 35 |   | ShrinkLimitTag

 36 |   | TestCountTag

 37 |   | TestLimitTag

 38 |   | EarlyTermLowerBoundTag

 40 | %runElab derive "Tag" [Show,Eq,Ord]

 42 | public export

 43 | record Tagged (tag : Tag) (t : Type) where

 44 |   constructor MkTagged

 45 |   unTag : t

 47 | %runElab derivePattern "Tagged" [I,P]

 48 |   [Show,Eq,Ord,Num,FromString,Semigroup,Monoid]

 50 | public export %inline

 51 | Semigroup (Tagged t Nat) where (<+>) = (+)

 53 | public export %inline

 54 | Monoid (Tagged t Nat) where neutral = 0

 56 | public export %inline

 57 | Show a => Interpolation (Tagged t a) where

 58 |   interpolate (MkTagged x) = show x

 63 | public export

 64 | 0 CoverCount : Type

 65 | CoverCount = Tagged CoverCountTag Nat

 68 | public export

 69 | 0 GroupName : Type

 70 | GroupName = Tagged GroupNameTag String

 73 | public export

 74 | 0 PropertyCount : Type

 75 | PropertyCount = Tagged PropertyCountTag Nat

 78 | public export

 79 | 0 ShrinkCount : Type

 80 | ShrinkCount = Tagged ShrinkCountTag Nat

 85 | public export

 86 | 0 ShrinkLimit : Type

 87 | ShrinkLimit = Tagged ShrinkLimitTag Nat

 90 | public export

 91 | 0 TestCount : Type

 92 | TestCount = Tagged TestCountTag Nat

 98 | public export

 99 | 0 TestLimit : Type

100 | TestLimit = Tagged TestLimitTag Nat

106 | public export

107 | 0 EarlyTermLowerBound : Type

108 | EarlyTermLowerBound = Tagged EarlyTermLowerBoundTag Nat

111 | public export

112 | 0 PropertyName : Type

113 | PropertyName = Tagged PropertyNameTag String

120 | public export

121 | record Confidence where

122 |   constructor MkConfidence

123 |   confidence : Bits64

124 |   0 inBound    : confidence >= 2 = True

126 | %runElab derive "Confidence" [Show,Eq,Ord]

128 | namespace Confidence

129 |   public export

130 |   fromInteger :

131 |        (n : Integer)

132 |     -> {auto 0 prf : the Bits64 (fromInteger n) >= 2 = True}

133 |     -> Confidence

134 |   fromInteger n = MkConfidence (fromInteger n) prf

136 |   export

137 |   toProbability : Confidence -> Probability

138 |   toProbability $ MkConfidence c _ =

139 |     -- we can do `ratio` because `c` is `>= 2` due to `prf`

140 |     ratio 1 (cast c) @{believe_me Oh} @{believe_me Oh}

143 | public export

144 | 0 CoverPercentage : Type

145 | CoverPercentage = DoubleBetween 0 100

148 | public export

149 | 0 LabelName : Type

150 | LabelName = Tagged LabelNameTag String

157 | public export

158 | record Diff where

159 |   constructor MkDiff

160 |   diffPrefix  : String

161 |   diffRemoved : String

162 |   diffInfix   : String

163 |   diffAdded   : String

164 |   diffSuffix  : String

165 |   diffValue   : ValueDiff

167 | %runElab derive "Hedgehog.Internal.Property.Diff" [Show,Eq]

171 | public export

172 | data Cover = NotCovered | Covered

174 | %runElab derive "Cover" [Show,Eq,Ord]

176 | public export

177 | Semigroup Cover where

178 |   NotCovered <+> NotCovered = NotCovered

179 |   _          <+> _          = Covered

181 | public export

182 | Monoid Cover where

183 |   neutral = NotCovered

185 | public export

186 | toCoverCount : Cover -> CoverCount

187 | toCoverCount NotCovered = 0

188 | toCoverCount Covered    = 1

194 | public export

195 | record Label a where

196 |   constructor MkLabel

197 |   labelName       : LabelName

198 |   labelMinimum    : CoverPercentage

199 |   labelAnnotation : a

201 | %runElab derive "Label" [Show,Eq]

203 | public export

204 | Functor Label where

205 |   map f = {labelAnnotation $= f}

207 | public export

208 | Foldable Label where

209 |   foldl f a l = f a l.labelAnnotation

210 |   foldr f a l = f l.labelAnnotation a

211 |   null _ = False

213 | public export

214 | Traversable Label where

215 |   traverse f l =

216 |     (\v => {labelAnnotation := v} l) <$> f l.labelAnnotation

222 | Semigroup a => Semigroup (Label a) where

223 |   ll <+> lr = { labelAnnotation $= (ll.labelAnnotation <+>) } lr

226 | public export

227 | data Log : Type where

228 |   Annotation : Lazy String -> Log

229 |   Footnote   : Lazy String -> Log

230 |   LogLabel   : Label Cover -> Log

232 | %runElab derive "Log" [Show,Eq]

235 | public export

236 | record Journal where

237 |   constructor MkJournal

238 |   journalLogs : List (Lazy Log)

240 | %runElab derive "Journal" [Show,Eq,Semigroup,Monoid]

243 | public export

244 | record Failure where

245 |   constructor MkFailure

246 |   message : String

247 |   diff    : Maybe Diff

249 | %runElab derive "Failure" [Show,Eq]

256 | record Coverage a where

257 |   constructor MkCoverage

258 |   coverageLabels : List (LabelName, Label a)

260 | %runElab derive "Coverage" [Show,Eq]

262 | export %inline

263 | names : Coverage a -> List LabelName

264 | names = map fst . coverageLabels

266 | export %inline

267 | labels : Coverage a -> List (Label a)

268 | labels = map snd . coverageLabels

270 | export %inline

271 | annotations : Coverage a -> List a

272 | annotations = map (labelAnnotation . snd) . coverageLabels

274 | mergeWith :

275 |      {auto _ : Ord k}

276 |   -> SnocList (k,v)

277 |   -> (v -> v -> v)

278 |   -> List (k,v)

279 |   -> List (k,v)

280 |   -> List (k,v)

281 | mergeWith sp _ [] ys               = sp <>> ys

282 | mergeWith sp _ xs []               = sp <>> xs

283 | mergeWith sp f (x :: xs) (y :: ys) = case compare (fst x) (fst y) of

284 |   LT => mergeWith (sp :< x) f xs (y :: ys)

285 |   EQ => mergeWith (sp :< (fst x, f (snd x) (snd y))) f xs ys

286 |   GT => mergeWith (sp :< y) f (x::xs) ys

288 | export %inline

289 | Semigroup a => Semigroup (Coverage a) where

290 |   MkCoverage x <+> MkCoverage y =

291 |     MkCoverage $ mergeWith [<] (<+>) x y

293 | export %inline

294 | Semigroup a => Monoid (Coverage a) where

295 |   neutral = MkCoverage []

298 | Functor Coverage where

299 |   map f = {coverageLabels $= map (mapSnd $ map f) }

302 | Foldable Coverage where

303 |   foldl f acc = foldl f acc . annotations

304 |   foldr f acc = foldr f acc . annotations

305 |   null = null . coverageLabels

308 | Traversable Coverage where

309 |   traverse f (MkCoverage sm) =

310 |     MkCoverage <$> traverse ((traverse . traverse) f) sm

316 | public export

317 | data TerminationCriteria : Type where

318 |   EarlyTermination        : Confidence -> TestLimit -> EarlyTermLowerBound -> TerminationCriteria

319 |   NoEarlyTermination      : Confidence -> TestLimit -> TerminationCriteria

320 |   NoConfidenceTermination : TestLimit -> TerminationCriteria

322 | %runElab derive "TerminationCriteria" [Show,Eq]

329 | public export

330 | unCriteria : TerminationCriteria -> (Maybe Confidence, TestLimit, Size)

331 | unCriteria (EarlyTermination c t _)    = (Just c, t, maxSize)

332 | unCriteria (NoEarlyTermination c t)    = (Just c, t, maxSize)

333 | unCriteria (NoConfidenceTermination t) = (Nothing, t, minSize)

336 | public export

337 | record PropertyConfig where

338 |   constructor MkPropertyConfig

339 |   shrinkLimit         : ShrinkLimit

340 |   terminationCriteria : TerminationCriteria

342 | %runElab derive "PropertyConfig" [Show,Eq]

345 | public export

346 | defaultMinTests : TestLimit

347 | defaultMinTests = 100

349 | public export

350 | defaultLowerBound : EarlyTermLowerBound

351 | defaultLowerBound = MkTagged $ unTag defaultMinTests

354 | public export

355 | defaultConfidence : Confidence

356 | defaultConfidence = Confidence.fromInteger 1000000000

359 | public export

360 | defaultConfig : PropertyConfig

361 | defaultConfig =

362 |   MkPropertyConfig

363 |     { shrinkLimit = 1000

364 |     , terminationCriteria = NoConfidenceTermination defaultMinTests

365 |     }

372 | public export

373 | 0 TestT : (Type -> Type) -> Type -> Type

374 | TestT m = EitherT Failure (WriterT Journal m)

376 | public export

377 | 0 Test : Type -> Type

378 | Test = TestT Identity

381 | mkTestT : Functor m => m (Either Failure a, Journal) -> TestT m a

382 | mkTestT = MkEitherT . writerT

385 | mkTest : (Either Failure a, Journal) -> Test a

386 | mkTest = mkTestT . Id

389 | runTestT : TestT m a -> m (Either Failure a, Journal)

390 | runTestT = runWriterT . runEitherT

393 | runTest : Test a -> (Either Failure a, Journal)

394 | runTest = runIdentity . runTestT

398 | writeLog : Applicative m => Lazy Log -> TestT m ()

399 | writeLog x = mkTestT $ pure (Right (), MkJournal [x])

404 | failWith : Applicative m => Maybe Diff -> String -> TestT m a

405 | failWith diff msg = mkTestT $ pure (Left $ MkFailure msg diff, neutral)

409 | export %inline

410 | annotate : Applicative m => Lazy String -> TestT m ()

411 | annotate v = writeLog $ Annotation v

415 | export %inline

416 | annotateShow : Show a => Applicative m => a -> TestT m ()

417 | annotateShow v = annotate $ ppShow v

421 | annotateAllShow : All Show ts => Monad m => HList ts -> TestT m ()

422 | annotateAllShow         []      = pure ()

423 | annotateAllShow @{_::_} [x]     = annotateShow x

424 | annotateAllShow @{_::_} (x::xs) = annotateShow x >> annotateAllShow xs

428 | export %inline

429 | footnote : Applicative m => Lazy String -> TestT m ()

430 | footnote v = writeLog $ Footnote v

434 | export %inline

435 | footnoteShow : Show a => Applicative m => a -> TestT m ()

436 | footnoteShow v = writeLog (Footnote $ ppShow v)

439 | export %inline

440 | failDiff : Show a => Show b => Applicative m => a -> b -> TestT m ()

441 | failDiff x y =

442 |   case valueDiff <$> reify x <*> reify y of

443 |     Nothing =>

444 |       failWith Nothing $

445 |         unlines

446 |           [ "Failed"

447 |           , "━━ lhs ━━"

448 |           , ppShow x

449 |           , "━━ rhs ━━"

450 |           , ppShow y

451 |           ]

453 |     Just vdiff@(Same _) =>

454 |       failWith

455 |         (Just $ MkDiff "━━━ Failed ("  "" "no differences" "" ") ━━━" vdiff)

456 |         ""

458 |     Just vdiff =>

459 |       failWith

460 |         (Just $ MkDiff "━━━ Failed (" "- lhs" ") (" "+ rhs" ") ━━━" vdiff)

461 |         ""

464 | export %inline

465 | failure : Applicative m => TestT m a

466 | failure = failWith Nothing ""

469 | export %inline

470 | success : Monad m => TestT m ()

471 | success = pure ()

474 | export %inline

475 | assert : Monad m => Bool -> TestT m ()

476 | assert ok = if ok then success else failure

490 | export %inline

491 | diff :

492 |      {auto _ : Show a}

493 |   -> {auto _ : Show b}

494 |   -> {auto _ : Monad m}

495 |   -> a -> (a -> b -> Bool) -> b -> TestT m ()

496 | diff x op y = if x `op` y then success else failDiff x y

498 | export infix 6 ===

501 | export %inline

502 | (===) : Eq a => Show a => Monad m => a -> a -> TestT m ()

503 | (===) x y = diff x (==) y

505 | export infix 4 /==

508 | export %inline

509 | (/==) : Eq a => Show a => Monad m => a -> a -> TestT m ()

510 | (/==) x y = diff x (/=) y

516 | evalEither : Show x => Monad m => Either x a -> TestT m a

517 | evalEither (Left x)  = failWith Nothing (ppShow x)

518 | evalEither (Right x) = pure x

523 | evalMaybe : Monad m => Maybe a -> TestT m a

524 | evalMaybe Nothing = failWith Nothing "the value was Nothing"

525 | evalMaybe (Just x) = pure x

533 | public export

534 | 0 PropertyT : Type -> Type

535 | PropertyT = TestT Gen

543 | forAllWith : (a -> String) -> Gen a -> PropertyT a

544 | forAllWith render gen = do

545 |   x <- lift (lift gen)

546 |   annotate (render x)

547 |   pure x

550 | export %inline

551 | forAll : Show a => Gen a -> PropertyT a

552 | forAll = forAllWith ppShow

561 | forAlls : All Show ts => All Gen ts -> PropertyT (HList ts)

562 | forAlls gens = do

563 |   xs <- lift $ lift $ hlist gens

564 |   annotateAllShow xs

565 |   pure xs

569 | test : Test a -> PropertyT a

570 | test = mapEitherT $ mapWriterT (pure . runIdentity)

578 | public export

579 | record Property where

580 |   constructor MkProperty

581 |   config : PropertyConfig

582 |   test   : PropertyT ()

584 | namespace Property

585 |   ||| Map a config modification function over a property.

586 |   export

587 |   mapConfig : (PropertyConfig -> PropertyConfig) -> Property -> Property

588 |   mapConfig f p = { config $= f } p

590 |   export

591 |   verifiedTermination :

592 |        {default defaultLowerBound min : EarlyTermLowerBound}

593 |     -> Property -> Property

594 |   verifiedTermination = mapConfig { terminationCriteria $= setEarlyTermination }

596 |     where

597 |       setEarlyTermination : TerminationCriteria -> TerminationCriteria

598 |       setEarlyTermination (NoEarlyTermination c n)    = EarlyTermination c n min

599 |       setEarlyTermination (NoConfidenceTermination n) = EarlyTermination defaultConfidence n min

600 |       setEarlyTermination (EarlyTermination c n lb)   = EarlyTermination c n min

602 |   export

603 |   noVerifiedTermination : Property -> Property

604 |   noVerifiedTermination = mapConfig { terminationCriteria $= setNoConfidence }

606 |     where

607 |       setNoConfidence : TerminationCriteria -> TerminationCriteria

608 |       setNoConfidence (NoEarlyTermination _ n)    = NoConfidenceTermination n

609 |       setNoConfidence (NoConfidenceTermination n) = NoConfidenceTermination n

610 |       setNoConfidence (EarlyTermination _ n _)    = NoConfidenceTermination n

612 |   ||| Adjust the number of times a property should be executed before it is considered

614 |   export

615 |   mapTests : (TestLimit -> TestLimit) -> Property -> Property

616 |   mapTests f = mapConfig {terminationCriteria $= setLimit}

618 |     where

619 |       setLimit : TerminationCriteria -> TerminationCriteria

620 |       setLimit (NoEarlyTermination c n)    = NoEarlyTermination c (f n)

621 |       setLimit (NoConfidenceTermination n) = NoConfidenceTermination (f n)

622 |       setLimit (EarlyTermination c n lb)   = EarlyTermination c (f n) lb

624 |   ||| Set the number of times a property should be executed before it is considered

630 |   export

631 |   withTests : TestLimit -> Property -> Property

632 |   withTests = mapTests . const

634 |   ||| Set the number of times a property is allowed to shrink before the test

636 |   export

637 |   withShrinks : ShrinkLimit -> Property -> Property

638 |   withShrinks n = mapConfig { shrinkLimit := n }

640 |   ||| Make sure that the result is statistically significant in accordance to

642 |   export

643 |   withConfidence : Confidence -> Property -> Property

644 |   withConfidence c = mapConfig { terminationCriteria $= setConfidence }

646 |     where

647 |       setConfidence : TerminationCriteria -> TerminationCriteria

648 |       setConfidence (NoEarlyTermination _ n)    = NoEarlyTermination c n

649 |       setConfidence (NoConfidenceTermination n) = NoEarlyTermination c n

650 |       setConfidence (EarlyTermination _ n lb)   = EarlyTermination c n lb

654 | property : PropertyT () -> Property

655 | property = MkProperty defaultConfig

663 | export %inline

664 | property1 : PropertyT () -> Property

665 | property1 = withTests 1 . property

668 | public export

669 | record Group where

670 |   constructor MkGroup

671 |   name       : GroupName

672 |   properties : List (PropertyName, Property)

674 | namespace Group

675 |   export

676 |   mapProperty : (Property -> Property) -> Group -> Group

677 |   mapProperty f = { properties $= map (mapSnd f) }

679 |   ||| Map a config modification function over all

681 |   export

682 |   mapConfig : (PropertyConfig -> PropertyConfig) -> Group -> Group

683 |   mapConfig = mapProperty . mapConfig

685 |   ||| Set the number of times the properties in a `Group`

688 |   export

689 |   withTests : TestLimit -> Group -> Group

690 |   withTests = mapProperty . withTests

692 |   ||| Set the number of times the properties in a `Group`

695 |   export

696 |   withShrinks : ShrinkLimit -> Group -> Group

697 |   withShrinks = mapProperty . withShrinks

699 |   ||| Make sure that the results of a `Group` are statistically

701 |   export

702 |   withConfidence : Confidence -> Group -> Group

703 |   withConfidence = mapProperty . withConfidence

710 | coverPercentage : TestCount -> CoverCount -> CoverPercentage

711 | coverPercentage (MkTagged tests) (MkTagged count) =

712 |   roughlyFit $ (cast count / cast tests) * 100

715 | labelCovered : TestCount -> Label CoverCount -> Bool

716 | labelCovered tests (MkLabel _ min population) =

717 |   coverPercentage tests population >= min

720 | coverageFailures : TestCount -> Coverage CoverCount -> List $ Label CoverCount

721 | coverageFailures tests kvs =

722 |   filter (not . labelCovered tests) (labels kvs)

726 | coverageSuccess : TestCount -> Coverage CoverCount -> Bool

727 | coverageSuccess tests c = null $ coverageFailures tests c

744 | cover : Monad m => CoverPercentage -> LabelName -> Bool -> TestT m ()

745 | cover min name covered =

746 |   let cover := if covered then Covered else NotCovered

747 |    in writeLog $ LogLabel (MkLabel name min cover)

762 | classify : Monad m => LabelName -> Bool -> TestT m ()

763 | classify name covered = cover 0 name covered

768 | label : Monad m => LabelName -> TestT m ()

769 | label name = cover 0 name True

773 | collect : Show a => Monad m => a -> TestT m ()

774 | collect x = cover 0 (MkTagged $ show x) True

777 | fromLabel : Label a -> Coverage a

778 | fromLabel x = MkCoverage $ [(labelName x, x)]

780 | unionsCoverage : Semigroup a => List (Coverage a) -> Coverage a

781 | unionsCoverage = MkCoverage . concatMap coverageLabels

784 | journalCoverage : Journal -> Coverage CoverCount

785 | journalCoverage =

786 |     map toCoverCount

787 |   . unionsCoverage

788 |   . (>>= fromLog)

789 |   . journalLogs

791 |   where

792 |     fromLog : Lazy Log -> List (Coverage Cover)

793 |     fromLog (LogLabel x)   = [fromLabel x]

794 |     fromLog (Footnote _)   = []

795 |     fromLog (Annotation _) = []

801 | boundsForLabel :

802 |      TestCount

803 |   -> Confidence

804 |   -> Label CoverCount

805 |   -> (Probability, Probability)

806 | boundsForLabel (MkTagged tests) c lbl = do

807 |   let (tests ** _) : (k ** IsSucc k) = case tests of

808 |                                          Z       => (1 ** ItIsSucc)

809 |                                          k@(S n) => (k ** ItIsSucc)

810 |   let succ = P $ roughlyFit $ cast (unTag lbl.labelAnnotation) / cast tests

811 |   wilsonBounds (toProbability c) tests succ

816 | confidenceSuccess : TestCount -> Confidence -> Coverage CoverCount -> Bool

817 | confidenceSuccess tests confidence =

818 |   all assertLow . labels

820 |   where

821 |     assertLow : Label CoverCount -> Bool

822 |     assertLow cc =

823 |       fst (boundsForLabel tests confidence cc) >= cc.labelMinimum.percent

828 | confidenceFailure : TestCount -> Confidence -> Coverage CoverCount -> Bool

829 | confidenceFailure tests confidence =

830 |   any assertHigh . labels

832 |   where

833 |     assertHigh : Label CoverCount -> Bool

834 |     assertHigh cc =

835 |       snd (boundsForLabel tests confidence cc) < cc.labelMinimum.percent

838 | multOf100 : TestCount -> Bool

839 | multOf100 (MkTagged n) = natToInteger n `mod` 100 == 0

842 | failureVerified : TestCount -> Coverage CoverCount -> Maybe Confidence -> Bool

843 | failureVerified count cover conf =

844 |   multOf100 count &&

845 |   maybe False (\c => confidenceFailure count c cover) conf

848 | successVerified : TestCount -> Coverage CoverCount -> Maybe Confidence -> Bool

849 | successVerified count cover conf =

850 |   multOf100 count &&

851 |   maybe False (\c => confidenceSuccess count c cover) conf

854 | abortEarly :

855 |      TerminationCriteria

856 |   -> TestCount

857 |   -> Coverage CoverCount

858 |   -> Maybe Confidence

859 |   -> Bool

860 | abortEarly (EarlyTermination _ _ etMinTests) tests cover conf =

861 |   let coverageReached     := successVerified tests cover conf

862 |       coverageUnreachable := failureVerified tests cover conf

863 |    in unTag tests >= unTag etMinTests &&

864 |       (coverageReached || coverageUnreachable)

866 | abortEarly _ _ _ _ = False