Hedgehog.Internal.Property

(source)

Reexports

import public Data.Double.Bounded

Definitions

data Tag : Type

Totality: total
Visibility: public export
Constructors:

ConfidenceTag : Tag
CoverCountTag : Tag
GroupNameTag : Tag
LabelNameTag : Tag
PropertyCountTag : Tag
PropertyNameTag : Tag
ShrinkCountTag : Tag
ShrinkLimitTag : Tag
TestCountTag : Tag
TestLimitTag : Tag
EarlyTermLowerBoundTag : Tag

Hints:

Eq Tag
Eq t => Eq (Tagged tag t)
FromString t => FromString (Tagged tag t)
Show a => Interpolation (Tagged t a)
Monoid t => Monoid (Tagged tag t)
Monoid (Tagged t Nat)
Num t => Num (Tagged tag t)
Ord Tag
Ord t => Ord (Tagged tag t)
Semigroup t => Semigroup (Tagged tag t)
Semigroup (Tagged t Nat)
Show Tag
Show t => Show (Tagged tag t)

record Tagged : Tag -> Type -> Type

Totality: total
Visibility: public export
Constructor:

MkTagged : t -> Tagged tag t

Projection:

.unTag : Tagged tag t -> t

Hints:

Eq t => Eq (Tagged tag t)
FromString t => FromString (Tagged tag t)
Show a => Interpolation (Tagged t a)
Monoid t => Monoid (Tagged tag t)
Monoid (Tagged t Nat)
Num t => Num (Tagged tag t)
Ord t => Ord (Tagged tag t)
Semigroup t => Semigroup (Tagged tag t)
Semigroup (Tagged t Nat)
Show t => Show (Tagged tag t)

.unTag : Tagged tag t -> t

Totality: total
Visibility: public export

unTag : Tagged tag t -> t

Totality: total
Visibility: public export

0 CoverCount : Type

  The total number of tests which are covered by a classifier.
  
  Can be constructed using numeric literals.

Totality: total
Visibility: public export

0 GroupName : Type

  The name of a group of properties.

Totality: total
Visibility: public export

0 PropertyCount : Type

  The number of properties in a group.

Totality: total
Visibility: public export

0 ShrinkCount : Type

  The numbers of times a property was able to shrink after a failing test.

Totality: total
Visibility: public export

0 ShrinkLimit : Type

  The number of shrinks to try before giving up on shrinking.
  
  Can be constructed using numeric literals:

Totality: total
Visibility: public export

0 TestCount : Type

  The number of tests a property ran successfully.

Totality: total
Visibility: public export

0 TestLimit : Type

  The number of successful tests that need to be run before a property test
  is considered successful.
  
  Can be constructed using numeric literals.

Totality: total
Visibility: public export

0 EarlyTermLowerBound : Type

  The number of successful tests that need to be run before the first check
  of a confidence interval at the early termination mode.
  
  Can be constructed using numeric literals.

Totality: total
Visibility: public export

0 PropertyName : Type

  The name of a property.

Totality: total
Visibility: public export

record Confidence : Type

  The acceptable occurrence of false positives
  
  Example, `the Confidence 1000000000` would mean that
  you'd accept a false positive
  for 1 in 10^9 tests.

Totality: total
Visibility: public export
Constructor:

MkConfidence : (confidence : Bits64) -> (0 _ : confidence >= 2 = True) -> Confidence

Projections:

.confidence : Confidence -> Bits64
0 .inBound : ({rec:0} : Confidence) -> confidence {rec:0} >= 2 = True

Hints:

Eq Confidence
Ord Confidence
Show Confidence

.confidence : Confidence -> Bits64

Totality: total
Visibility: public export

confidence : Confidence -> Bits64

Totality: total
Visibility: public export

0 .inBound : ({rec:0} : Confidence) -> confidence {rec:0} >= 2 = True

Totality: total
Visibility: public export

0 inBound : ({rec:0} : Confidence) -> confidence {rec:0} >= 2 = True

Totality: total
Visibility: public export

fromInteger : (n : Integer) -> {auto 0 _ : the Bits64 (fromInteger n) >= 2 = True} -> Confidence

Totality: total
Visibility: public export

toProbability : Confidence -> Probability

Totality: total
Visibility: export

0 CoverPercentage : Type

  The relative number of tests which are covered by a classifier.

Totality: total
Visibility: public export

0 LabelName : Type

  The name of a classifier.

Totality: total
Visibility: public export

record Diff : Type

  The difference between some expected and actual value.

Totality: total
Visibility: public export
Constructor:

MkDiff : String -> String -> String -> String -> String -> ValueDiff -> Diff

Projections:

.diffAdded : Diff -> String
.diffInfix : Diff -> String
.diffPrefix : Diff -> String
.diffRemoved : Diff -> String
.diffSuffix : Diff -> String
.diffValue : Diff -> ValueDiff

Hints:

Eq Diff
Show Diff

.diffPrefix : Diff -> String

Totality: total
Visibility: public export

diffPrefix : Diff -> String

Totality: total
Visibility: public export

.diffRemoved : Diff -> String

Totality: total
Visibility: public export

diffRemoved : Diff -> String

Totality: total
Visibility: public export

.diffInfix : Diff -> String

Totality: total
Visibility: public export

diffInfix : Diff -> String

Totality: total
Visibility: public export

.diffAdded : Diff -> String

Totality: total
Visibility: public export

diffAdded : Diff -> String

Totality: total
Visibility: public export

.diffSuffix : Diff -> String

Totality: total
Visibility: public export

diffSuffix : Diff -> String

Totality: total
Visibility: public export

.diffValue : Diff -> ValueDiff

Totality: total
Visibility: public export

diffValue : Diff -> ValueDiff

Totality: total
Visibility: public export

data Cover : Type

  Whether a test is covered by a classifier, and therefore belongs to a
  'Class'.

Totality: total
Visibility: public export
Constructors:

NotCovered : Cover
Covered : Cover

Hints:

Eq Cover
Monoid Cover
Ord Cover
Semigroup Cover
Show Cover

toCoverCount : Cover -> CoverCount

Totality: total
Visibility: public export

record Label : Type -> Type

  The extent to which a test is covered by a classifier.
  
  When a classifier's coverage does not exceed the required minimum, the
  test will be failed.

Totality: total
Visibility: public export
Constructor:

MkLabel : LabelName -> CoverPercentage -> a -> Label a

Projections:

.labelAnnotation : Label a -> a
.labelMinimum : Label a -> CoverPercentage
.labelName : Label a -> LabelName

Hints:

Eq a => Eq (Label a)
Foldable Label
Functor Label
Semigroup a => Semigroup (Label a)
Show a => Show (Label a)
Traversable Label

.labelName : Label a -> LabelName

Totality: total
Visibility: public export

labelName : Label a -> LabelName

Totality: total
Visibility: public export

.labelMinimum : Label a -> CoverPercentage

Totality: total
Visibility: public export

labelMinimum : Label a -> CoverPercentage

Totality: total
Visibility: public export

.labelAnnotation : Label a -> a

Totality: total
Visibility: public export

labelAnnotation : Label a -> a

Totality: total
Visibility: public export

data Log : Type

  Log messages which are recorded during a test run.

Totality: total
Visibility: public export
Constructors:

Annotation : Lazy String -> Log
Footnote : Lazy String -> Log
LogLabel : Label Cover -> Log

Hints:

Eq Log
Show Log

record Journal : Type

  A record containing the details of a test run.

Totality: total
Visibility: public export
Constructor:

MkJournal : List (Lazy Log) -> Journal

Projection:

.journalLogs : Journal -> List (Lazy Log)

Hints:

Eq Journal
Monoid Journal
Semigroup Journal
Show Journal

.journalLogs : Journal -> List (Lazy Log)

Totality: total
Visibility: public export

journalLogs : Journal -> List (Lazy Log)

Totality: total
Visibility: public export

record Failure : Type

  Details on where and why a test failed.

Totality: total
Visibility: public export
Constructor:

MkFailure : String -> Maybe Diff -> Failure

Projections:

.diff : Failure -> Maybe Diff
.message : Failure -> String

Hints:

Eq Failure
Show Failure

.message : Failure -> String

Totality: total
Visibility: public export

message : Failure -> String

Totality: total
Visibility: public export

.diff : Failure -> Maybe Diff

Totality: total
Visibility: public export

diff : Failure -> Maybe Diff

Totality: total
Visibility: public export

record Coverage : Type -> Type

  The extent to which all classifiers cover a test.
  
  When a given classification's coverage does not exceed the required/
  minimum, the test will be failed.

Totality: total
Visibility: export
Constructor:

MkCoverage : List (LabelName, Label a) -> Coverage a

Projection:

.coverageLabels : Coverage a -> List (LabelName, Label a)

Hints:

Eq a => Eq (Coverage a)
Foldable Coverage
Functor Coverage
Semigroup a => Monoid (Coverage a)
Semigroup a => Semigroup (Coverage a)
Show a => Show (Coverage a)
Traversable Coverage

names : Coverage a -> List LabelName

Totality: total
Visibility: export

labels : Coverage a -> List (Label a)

Totality: total
Visibility: export

annotations : Coverage a -> List a

Totality: total
Visibility: export

data TerminationCriteria : Type

Totality: total
Visibility: public export
Constructors:

EarlyTermination : Confidence -> TestLimit -> EarlyTermLowerBound -> TerminationCriteria
NoEarlyTermination : Confidence -> TestLimit -> TerminationCriteria
NoConfidenceTermination : TestLimit -> TerminationCriteria

Hints:

Eq TerminationCriteria
Show TerminationCriteria

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

  Returns main paramters of the termination criteria
  
  Returned size is the minimal starting size according to the criteria.
  For confidence-checking criteria it is important to start with maximal size
  to achieve correct distribution.

Totality: total
Visibility: public export

record PropertyConfig : Type

  Configuration for a property test.

Totality: total
Visibility: public export
Constructor:

MkPropertyConfig : ShrinkLimit -> TerminationCriteria -> PropertyConfig

Projections:

.shrinkLimit : PropertyConfig -> ShrinkLimit
.terminationCriteria : PropertyConfig -> TerminationCriteria

Hints:

Eq PropertyConfig
Show PropertyConfig

.shrinkLimit : PropertyConfig -> ShrinkLimit

Totality: total
Visibility: public export

shrinkLimit : PropertyConfig -> ShrinkLimit

Totality: total
Visibility: public export

.terminationCriteria : PropertyConfig -> TerminationCriteria

Totality: total
Visibility: public export

terminationCriteria : PropertyConfig -> TerminationCriteria

Totality: total
Visibility: public export

defaultMinTests : TestLimit

  The minimum amount of tests to run for a 'Property'

Totality: total
Visibility: public export

defaultLowerBound : EarlyTermLowerBound

Totality: total
Visibility: public export

defaultConfidence : Confidence

  The default confidence allows one false positive in 10^9 tests

Totality: total
Visibility: public export

defaultConfig : PropertyConfig

  The default configuration for a property test.

Totality: total
Visibility: public export

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

  A test monad transformer allows the assertion of expectations.

Totality: total
Visibility: public export

0 Test : Type -> Type

Totality: total
Visibility: public export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

  Log some information which might be relevant to a potential test failure.

Totality: total
Visibility: export

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

  Fail the test with an error message, useful for building other failure
  combinators.

Totality: total
Visibility: export

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

  Annotates the source code with a message that might be useful for
  debugging a test failure.

Totality: total
Visibility: export

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

  Annotates the source code with a value that might be useful for
  debugging a test failure.

Totality: total
Visibility: export

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

  Annotates the source code with all values separately.

Totality: total
Visibility: export

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

  Logs a message to be displayed as additional information in the footer of
  the failure report.

Totality: total
Visibility: export

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

  Logs a value to be displayed as additional information in the footer of
  the failure report.

Totality: total
Visibility: export

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

  Fails with an error that shows the difference between two values.

Totality: total
Visibility: export

failure : Applicative m => TestT m a

  Causes a test to fail.

Totality: total
Visibility: export

success : Monad m => TestT m ()

  Another name for `pure ()`.

Totality: total
Visibility: export

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

  Fails the test if the condition provided is 'False'.

Totality: total
Visibility: export

diff : Show a => Show b => Monad m => a -> (a -> b -> Bool) -> b -> TestT m ()

  Fails the test and shows a git-like diff if the comparison operation
  evaluates to 'False' when applied to its arguments.
  
  The comparison function is the second argument, which may be
  counter-intuitive to Haskell programmers. However, it allows operators to
  be written infix for easy reading:
  
  This function behaves like the unix @diff@ tool, which gives a 0 exit
  code if the compared files are identical, or a 1 exit code code
  otherwise. Like unix @diff@, if the arguments fail the comparison, a
  /diff is shown.

Totality: total
Visibility: export

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

  Fails the test if the two arguments provided are not equal.

Totality: total
Visibility: export
Fixity Declarations:
infix operator, level 6
infix operator, level 6

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

  Fails the test if the two arguments provided are equal.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 4

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

  Fails the test if the 'Either' is 'Left', otherwise returns the value in
  the 'Right'.

Totality: total
Visibility: export

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

  Fails the test if the 'Maybe' is 'Nothing', otherwise returns the value in
  the 'Just'.

Totality: total
Visibility: export

0 PropertyT : Type -> Type

  The property monad allows both the generation of test inputs
   and the assertion of expectations.

Totality: total
Visibility: public export

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

  Generates a random input for the test by running the provided generator.
  
  This is a the same as 'forAll' but allows the user to provide a custom
  rendering function. This is useful for values which don't have a
  'Show' instance.

Totality: total
Visibility: export

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

  Generates a random input for the test by running the provided generator.

Totality: total
Visibility: export

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

  Generates a random input provided a bunch of generators.
  
  This function is an easy way to write several foralls in a row.
  `[a, b, c] <- forAlls [x, y, z]` prints error message like
  `(a, b, c) <- [| (forAll x, forAll y, forAll z) |]` but shrinks like
  `(a, b, c) <- forAll [| (x, y, z) |]`.

Totality: total
Visibility: export

test : Test a -> PropertyT a

  Lift a test in to a property.

Totality: total
Visibility: export

record Property : Type

  A property test, along with some configurable limits like how many times
  to run the test.

Totality: total
Visibility: public export
Constructor:

MkProperty : PropertyConfig -> PropertyT () -> Property

Projections:

.config : Property -> PropertyConfig
.test : Property -> PropertyT ()

.config : Property -> PropertyConfig

Totality: total
Visibility: public export

config : Property -> PropertyConfig

Totality: total
Visibility: public export

.test : Property -> PropertyT ()

Totality: total
Visibility: public export

test : Property -> PropertyT ()

Totality: total
Visibility: public export

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

  Map a config modification function over a property.

Totality: total
Visibility: export

verifiedTermination : {default defaultLowerBound _ : EarlyTermLowerBound} -> Property -> Property

Totality: total
Visibility: export

noVerifiedTermination : Property -> Property

Totality: total
Visibility: export

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

  Adjust the number of times a property should be executed before it is considered
  successful.

Totality: total
Visibility: export

withTests : TestLimit -> Property -> Property

  Set the number of times a property should be executed before it is considered
  successful.
  
  If you have a test that does not involve any generators and thus does not
  need to run repeatedly, you can use @withTests 1@ to define a property that
  will only be checked once.

Totality: total
Visibility: export

withShrinks : ShrinkLimit -> Property -> Property

  Set the number of times a property is allowed to shrink before the test
  runner gives up and prints the counterexample.

Totality: total
Visibility: export

withConfidence : Confidence -> Property -> Property

  Make sure that the result is statistically significant in accordance to
  the passed 'Confidence'

Totality: total
Visibility: export

property : PropertyT () -> Property

  Creates a property with the default configuration.

Totality: total
Visibility: export

property1 : PropertyT () -> Property

  Creates a property, that is tested exactly once.
  
  Use this for tests that are not based on randomly generated
  inputs.
  
  This is an alias for `withTests 1 . property`.

Totality: total
Visibility: export

record Group : Type

  A named collection of property tests.

Totality: total
Visibility: public export
Constructor:

MkGroup : GroupName -> List (PropertyName, Property) -> Group

Projections:

.name : Group -> GroupName
.properties : Group -> List (PropertyName, Property)

.name : Group -> GroupName

Totality: total
Visibility: public export

name : Group -> GroupName

Totality: total
Visibility: public export

.properties : Group -> List (PropertyName, Property)

Totality: total
Visibility: public export

properties : Group -> List (PropertyName, Property)

Totality: total
Visibility: public export

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

Totality: total
Visibility: export

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

  Map a config modification function over all
  properties in a `Group`.

Totality: total
Visibility: export

withTests : TestLimit -> Group -> Group

  Set the number of times the properties in a `Group`
  should be executed before they are considered
  successful.

Totality: total
Visibility: export

withShrinks : ShrinkLimit -> Group -> Group

  Set the number of times the properties in a `Group`
  are allowed to shrink before the test
  runner gives up and prints the counterexample.

Totality: total
Visibility: export

withConfidence : Confidence -> Group -> Group

  Make sure that the results of a `Group` are statistically
  significant in accordance to the passed 'Confidence'

Totality: total
Visibility: export

coverPercentage : TestCount -> CoverCount -> CoverPercentage

Totality: total
Visibility: export

labelCovered : TestCount -> Label CoverCount -> Bool

Totality: total
Visibility: export

coverageFailures : TestCount -> Coverage CoverCount -> List (Label CoverCount)

Totality: total
Visibility: export

coverageSuccess : TestCount -> Coverage CoverCount -> Bool

  All labels are covered

Totality: total
Visibility: export

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

  Require a certain percentage of the tests to be covered by the
  classifier.
  
  ```idris
     prop_with_coverage : Property
     prop_with_coverage =
       property $ do
         match <- forAll Gen.bool
         cover 30 "True" $ match
         cover 30 "False" $ not match
  ```
  
  The example above requires a minimum of 30% coverage for both
  classifiers. If these requirements are not met, it will fail the test.

Totality: total
Visibility: export

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

  Records the proportion of tests which satisfy a given condition.
  
  ```idris example
     prop_with_classifier : Property
     prop_with_classifier =
       property $ do
         xs <- forAll $ Gen.list (Range.linear 0 100) Gen.alpha
         for_ xs $ \\x -> do
           classify "newborns" $ x == 0
           classify "children" $ x > 0 && x < 13
           classify "teens" $ x > 12 && x < 20
  ```

Totality: total
Visibility: export

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

  Add a label for each test run. It produces a table showing the percentage
  of test runs that produced each label.

Totality: total
Visibility: export

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

  Like 'label', but uses 'Show' to render its argument for display.

Totality: total
Visibility: export

journalCoverage : Journal -> Coverage CoverCount

Totality: total
Visibility: export

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

  Is true when the test coverage satisfies the specified 'Confidence'
  contstraint for all 'Coverage CoverCount's

Totality: total
Visibility: export

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

  Is true when there exists a label that is sure to have failed according to
  the 'Confidence' constraint

Totality: total
Visibility: export

multOf100 : TestCount -> Bool

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

abortEarly : TerminationCriteria -> TestCount -> Coverage CoverCount -> Maybe Confidence -> Bool

Totality: total
Visibility: export