SampleableExt
Class #
This class permits the creation samples of a given type
controlling the size of those values using the Gen
monad`.
Shrinkable
Class #
This class helps minimize examples by creating smaller versions of given values.
When testing a proposition like ∀ n : ℕ, prime n → n ≤ 100∀ n : ℕ, prime n → n ≤ 100→ n ≤ 100≤ 100
,
SlimCheck
requires that ℕ
have an instance of SampleableExt
and for
prime n
to be decidable. SlimCheck
will then use the instance of
SampleableExt
to generate small examples of ℕ and progressively increase
in size. For each example n
, prime n
is tested. If it is false,
the example will be rejected (not a test success nor a failure) and
SlimCheck
will move on to other examples. If prime n
is true, n ≤ 100≤ 100
will be tested. If it is false, n
is a counter-example of ∀ n : ℕ, prime n → n ≤ 100∀ n : ℕ, prime n → n ≤ 100→ n ≤ 100≤ 100
and the test fails. If n ≤ 100≤ 100
is true,
the test passes and SlimCheck
moves on to trying more examples.
This is a port of the Haskell QuickCheck library.
Main definitions #
SampleableExt
classShrinkable
class
SampleableExt
#
SampleableExt
can be used in two ways. The first (and most common)
is to simply generate values of a type directly using the Gen
monad,
if this is what you want to do then SampleableExt.mkSelfContained
is
the way to go.
Furthermore it makes it possible to express generators for types that
do not lend themselves to introspection, such as ℕ → ℕ→ ℕ
.
If we test a quantification over functions the
counter-examples cannot be shrunken or printed meaningfully.
For that purpose, SampleableExt
provides a proxy representation
proxy
that can be printed and shrunken as well
as interpreted (using interp
) as an object of the right type. If you
are using it in the first way, this proxy type will simply be the type
itself and the interp
function id
.
`Shrinkable #
Given an example x : α
, Shrinkable α
gives us a way to shrink it
and suggest simpler examples.
Shrinking #
Shrinking happens when SlimCheck
find a counter-example to a
property. It is likely that the example will be more complicated than
necessary so SlimCheck
proceeds to shrink it as much as
possible. Although equally valid, a smaller counter-example is easier
for a user to understand and use.
The Shrinkable
class, , has a shrink
function so that we can use
specialized knowledge while shrinking a value. It is not responsible
for the whole shrinking process however. It only has to take one step
in the shrinking process. SlimCheck
will repeatedly call shrink
until no more steps can be taken. Because shrink
guarantees that the
size of the candidates it produces is strictly smaller than the
argument, we know that SlimCheck
is guaranteed to terminate.
Tags #
random testing
References #
- https://hackage.haskell.org/package/QuickCheck
- shrink : (x : α) → List { y // WellFoundedRelation.rel y x }
Given an example x : α
, Shrinkable α
gives us a way to shrink it
and suggest simpler examples.
Instances
- proxy : Type v
- proxyRepr : Repr proxy
- shrink : SlimCheck.Shrinkable proxy
- sample : SlimCheck.Gen proxy
- interp : proxy → α
SampleableExt
can be used in two ways. The first (and most common)
is to simply generate values of a type directly using the Gen
monad,
if this is what you want to do then SampleableExt.mkSelfContained
is
the way to go.
Furthermore it makes it possible to express generators for types that
do not lend themselves to introspection, such as ℕ → ℕ→ ℕ
.
If we test a quantification over functions the
counter-examples cannot be shrunken or printed meaningfully.
For that purpose, SampleableExt
provides a proxy representation
proxy
that can be printed and shrunken as well
as interpreted (using interp
) as an object of the right type.
Instances
Use to generate instance whose purpose is to simply generate values
of a type directly using the Gen
monad
Equations
- SlimCheck.SampleableExt.mkSelfContained sample = SlimCheck.SampleableExt.mk α sample id
First samples a proxy value and interprets it. Especially useful if the proxy and target type are the same.
Equations
- SlimCheck.SampleableExt.interpSample α = SlimCheck.SampleableExt.interp <$> SlimCheck.SampleableExt.sample
Nat.shrink' n
creates a list of smaller natural numbers by
successively dividing n
by 2 . For example, Nat.shrink 5 = [2, 1, 0]
.
Equations
- One or more equations did not get rendered due to their size.
Fin.shrink
works like Nat.shrink
but instead operates on Fin
.
Equations
- SlimCheck.Fin.shrink m = let shrinks := SlimCheck.Nat.shrink ↑m; List.map (fun x => { val := ↑↑x, property := (_ : WellFoundedRelation.rel (↑↑x) m) }) shrinks
Equations
- SlimCheck.Fin.shrinkable = SlimCheck.Shrinkable.mk SlimCheck.Fin.shrink
Equations
- SlimCheck.Int_sizeOfAbs = { sizeOf := Int.natAbs }
Int.shrinkable
operates like Nat.shrinkable
but also includes the negative variants.
Equations
- One or more equations did not get rendered due to their size.
Equations
- SlimCheck.Bool.shrinkable = SlimCheck.Shrinkable.mk fun x => []
Equations
- SlimCheck.Char.shrinkable = SlimCheck.Shrinkable.mk fun x => []
Equations
- One or more equations did not get rendered due to their size.
Equations
- SlimCheck.Nat.sampleableExt = SlimCheck.SampleableExt.mkSelfContained do let __do_lift ← SlimCheck.Gen.getSize Lean.Internal.coeM (SlimCheck.Gen.choose ℕ 0 __do_lift (_ : 0 ≤ __do_lift))
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
This can be specialized into customized SampleableExt Char
instances.
The resulting instance has 1 / length
chances of making an unrestricted choice of characters
and it otherwise chooses a character from chars
with uniform probabilities.
Equations
- One or more equations did not get rendered due to their size.
Equations
- SlimCheck.Char.sampleableDefault = SlimCheck.Char.sampleable 3 (String.toList " 0123abcABC:,;`\\/") SlimCheck.Char.sampleableDefault.proof_1
Equations
- One or more equations did not get rendered due to their size.
An annotation for values that should never get shrinked.
Equations
- SlimCheck.NoShrink α = α
Equations
Equations
Equations
- SlimCheck.NoShrink.inhabited = inst
Equations
- SlimCheck.NoShrink.repr = inst
Equations
- SlimCheck.NoShrink.shrinkable = SlimCheck.Shrinkable.mk fun x => []
Equations
- SlimCheck.NoShrink.sampleableExt = SlimCheck.SampleableExt.mkSelfContained ((SlimCheck.NoShrink.mk ∘ SlimCheck.SampleableExt.interp) <$> SlimCheck.SampleableExt.sample)