`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`

,
`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`

will be tested. If it is false, `n`

is a counter-example of
`∀ n : ℕ, Prime n → n ≤ 100`

and the test fails. If `n ≤ 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`

class`Shrinkable`

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 #

Given an example `x : α`

, `Shrinkable α`

gives us a way to shrink it
and suggest simpler examples.

- shrink : α → List α

## Instances

`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.

- proxy : Type v
- proxyRepr : Repr (SlimCheck.SampleableExt.proxy α)
- shrink : SlimCheck.Shrinkable (SlimCheck.SampleableExt.proxy α)
- sample : SlimCheck.Gen (SlimCheck.SampleableExt.proxy α)
- interp : SlimCheck.SampleableExt.proxy α → α

## 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

## Instances For

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

## Instances For

`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

- SlimCheck.Nat.shrink n = if h : 0 < n then let m := n / 2; let_fun this := ⋯; m :: SlimCheck.Nat.shrink m else []

## Instances For

## Equations

- SlimCheck.Nat.shrinkable = { shrink := SlimCheck.Nat.shrink }

## Equations

- SlimCheck.Fin.shrinkable = { shrink := fun (m : Fin n.succ) => do let a ← SlimCheck.Nat.shrink ↑m pure ↑a }

`Int.shrinkable`

operates like `Nat.shrinkable`

but also includes the negative variants.

## Equations

- SlimCheck.Int.shrinkable = { shrink := fun (n : ℤ) => (List.map (fun (x : ℤ) => [x, -x]) do let a ← SlimCheck.Nat.shrink n.natAbs pure ↑a).join }

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- SlimCheck.Bool.shrinkable = { shrink := fun (x : Bool) => [] }

## Equations

- SlimCheck.Char.shrinkable = { shrink := fun (x : Char) => [] }

## 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.

Shrink a list of a shrinkable type, either by discarding an element or shrinking an element.

## 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 let a ← SlimCheck.Gen.choose ℕ 0 __do_lift ⋯ pure ↑a

## 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.

## 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.

## Instances For

## Equations

- SlimCheck.Char.sampleableDefault = SlimCheck.Char.sampleable 3 " 0123abcABC:,;`\\/".toList SlimCheck.Char.sampleableDefault.proof_1

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- SlimCheck.List.sampleableExt = SlimCheck.SampleableExt.mk (List (SlimCheck.SampleableExt.proxy α)) SlimCheck.SampleableExt.sample.listOf (List.map SlimCheck.SampleableExt.interp)

An annotation for values that should never get shrunk.

## Equations

- SlimCheck.NoShrink α = α

## Instances For

## Equations

## Instances For

## Equations

- x.get = x

## Instances For

## Equations

- SlimCheck.NoShrink.inhabited = inst

## Equations

- SlimCheck.NoShrink.repr = inst

## Equations

- SlimCheck.NoShrink.shrinkable = { shrink := fun (x : SlimCheck.NoShrink α) => [] }

## Equations

- SlimCheck.NoShrink.sampleableExt = SlimCheck.SampleableExt.mkSelfContained ((SlimCheck.NoShrink.mk ∘ SlimCheck.SampleableExt.interp) <$> SlimCheck.SampleableExt.sample)

Print (at most) 10 samples of a given type to stdout for debugging.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Create a `Gen α`

expression from the argument of `#sample`

## Instances For

`#sample type`

, where `type`

has an instance of `SampleableExt`

, prints ten random
values of type `type`

using an increasing size parameter.

```
#sample Nat
-- prints
-- 0
-- 0
-- 2
-- 24
-- 64
-- 76
-- 5
-- 132
-- 8
-- 449
-- or some other sequence of numbers
#sample List Int
-- prints
-- []
-- [1, 1]
-- [-7, 9, -6]
-- [36]
-- [-500, 105, 260]
-- [-290]
-- [17, 156]
-- [-2364, -7599, 661, -2411, -3576, 5517, -3823, -968]
-- [-643]
-- [11892, 16329, -15095, -15461]
-- or whatever
```

## Equations

- SlimCheck.«command#sample_» = Lean.ParserDescr.node `SlimCheck.command#sample_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#sample ") (Lean.ParserDescr.cat `term 0))