sampleable
Class #
This class permits the creation samples of a given type
controlling the size of those values using the gen
monad`. It also
helps minimize examples by creating smaller versions of given values.
When testing a proposition like ∀ n : ℕ, prime n → n ≤ 100
,
slim_check
requires that ℕ
have an instance of sampleable
and for
prime n
to be decidable. slim_check
will then use the instance of
sampleable
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
slim_check
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 slim_check
moves on to trying more examples.
This is a port of the Haskell QuickCheck library.
Main definitions #
sampleable
classsampleable_functor
andsampleable_bifunctor
classsampleable_ext
class
sampleable
#
sampleable α
provides ways of creating examples of type α
,
and given such an example x : α
, gives us a way to shrink it
and find simpler examples.
sampleable_ext
#
sampleable_ext
generalizes the behavior of sampleable
and makes it possible to express instances 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, sampleable_ext
provides a proxy representation
proxy_repr
that can be printed and shrunken as well
as interpreted (using interp
) as an object of the right type.
sampleable_functor
and sampleable_bifunctor
#
sampleable_functor F
and sampleable_bifunctor F
makes it possible
to create samples of and shrink F α
given a sampling function and a
shrinking function for arbitrary α
.
This allows us to separate the logic for generating the shape of a
collection from the logic for generating its contents. Specifically,
the contents could be generated using either sampleable
or
sampleable_ext
instance and the sampleable_(bi)functor
does not
need to use that information
Shrinking #
Shrinking happens when slim_check
find a counter-example to a
property. It is likely that the example will be more complicated than
necessary so slim_check
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 sampleable
class, beside having the sample
function, 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.
slim_check
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
slim_check
is guaranteed to terminate.
Tags #
random testing
References #
sizeof_lt x y
compares the sizes of x
and y
.
Equations
- slim_check.sizeof_lt x y = (sizeof x < sizeof y)
shrink_fn α
is the type of functions that shrink an
argument of type α
Equations
- slim_check.shrink_fn α = Π (x : α), lazy_list {y // slim_check.sizeof_lt y x}
- wf : has_sizeof α
- sample : slim_check.gen α
- shrink : Π (x : α), lazy_list {y // sizeof y < sizeof x}
sampleable α
provides ways of creating examples of type α
,
and given such an example x : α
, gives us a way to shrink it
and find simpler examples.
Instances of this typeclass
- slim_check.sampleable.functor
- slim_check.sampleable.bifunctor
- slim_check.fin.sampleable'
- slim_check.nat.sampleable
- slim_check.fin.sampleable
- slim_check.pnat.sampleable
- slim_check.int.sampleable
- slim_check.bool.sampleable
- slim_check.sigma.sampleable
- slim_check.rat.sampleable
- slim_check.char.sampleable
- slim_check.no_shrink.sampleable
- slim_check.string.sampleable
- slim_check.nat_le.sampleable
- slim_check.nat_ge.sampleable
- slim_check.nat_gt.sampleable
- slim_check.le.sampleable
- slim_check.ge.sampleable
- slim_check.int_le.sampleable
- slim_check.int_ge.sampleable
- slim_check.int_lt.sampleable
- slim_check.int_gt.sampleable
- slim_check.perm.slim_check
- slim_check.perm'.slim_check
Instances of other typeclasses for slim_check.sampleable
- slim_check.sampleable.has_sizeof_inst
- wf : Π (α : Type ?) [_inst_1 : has_sizeof α], has_sizeof (F α)
- sample : Π {α : Type ?}, slim_check.gen α → slim_check.gen (F α)
- shrink : Π (α : Type ?) [_inst_1_1 : has_sizeof α], slim_check.shrink_fn α → slim_check.shrink_fn (F α)
- p_repr : Π (α : Type ?), has_repr α → has_repr (F α)
sampleable_functor F
makes it possible to create samples of and
shrink F α
given a sampling function and a shrinking function for
arbitrary α
Instances of this typeclass
Instances of other typeclasses for slim_check.sampleable_functor
- slim_check.sampleable_functor.has_sizeof_inst
- wf : Π (α : Type ?) (β : Type ?) [_inst_1 : has_sizeof α] [_inst_2 : has_sizeof β], has_sizeof (F α β)
- sample : Π {α : Type ?} {β : Type ?}, slim_check.gen α → slim_check.gen β → slim_check.gen (F α β)
- shrink : Π (α : Type ?) (β : Type ?) [_inst_1_1 : has_sizeof α] [_inst_2 : has_sizeof β], slim_check.shrink_fn α → slim_check.shrink_fn β → slim_check.shrink_fn (F α β)
- p_repr : Π (α : Type ?) (β : Type ?), has_repr α → has_repr β → has_repr (F α β)
sampleable_bifunctor F
makes it possible to create samples of
and shrink F α β
given a sampling function and a shrinking function
for arbitrary α
and β
Instances of this typeclass
Instances of other typeclasses for slim_check.sampleable_bifunctor
- slim_check.sampleable_bifunctor.has_sizeof_inst
- proxy_repr : Type ?
- wf : has_sizeof (slim_check.sampleable_ext.proxy_repr α)
- interp : slim_check.sampleable_ext.proxy_repr α → α . "mk_trivial_interp"
- p_repr : has_repr (slim_check.sampleable_ext.proxy_repr α)
- sample : slim_check.gen (slim_check.sampleable_ext.proxy_repr α)
- shrink : slim_check.shrink_fn (slim_check.sampleable_ext.proxy_repr α)
sampleable_ext
generalizes the behavior of sampleable
and makes it possible to express instances 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, sampleable_ext
provides a proxy representation
proxy_repr
that can be printed and shrunken as well
as interpreted (using interp
) as an object of the right type.
Instances of this typeclass
- slim_check.sampleable_ext.of_sampleable
- slim_check.sampleable_ext.functor
- slim_check.sampleable_ext.bifunctor
- slim_check.Prop.sampleable_ext
- slim_check.total_function.pi.sampleable_ext
- slim_check.total_function.finsupp.sampleable_ext
- slim_check.total_function.dfinsupp.sampleable_ext
- slim_check.injective_function.pi_injective.sampleable_ext
- slim_check.total_function.pi_pred.sampleable_ext
- slim_check.total_function.pi_uncurry.sampleable_ext
Instances of other typeclasses for slim_check.sampleable_ext
- slim_check.sampleable_ext.has_sizeof_inst
Equations
- slim_check.sampleable_ext.of_sampleable = {proxy_repr := α, wf := slim_check.sampleable.wf _inst_1, interp := id α, p_repr := _inst_2, sample := slim_check.sampleable.sample α _inst_1, shrink := slim_check.sampleable.shrink _inst_1}
Equations
- slim_check.sampleable.bifunctor = {wf := slim_check.sampleable_bifunctor.wf α β slim_check.sampleable.wf, sample := slim_check.sampleable_bifunctor.sample F (slim_check.sampleable.sample α) (slim_check.sampleable.sample β), shrink := slim_check.sampleable_bifunctor.shrink α β slim_check.sampleable.shrink slim_check.sampleable.shrink}
Equations
- slim_check.sampleable_ext.functor = {proxy_repr := F (slim_check.sampleable_ext.proxy_repr α), wf := slim_check.sampleable_functor.wf (slim_check.sampleable_ext.proxy_repr α) slim_check.sampleable_ext.wf, interp := functor.map (slim_check.sampleable_ext.interp α), p_repr := slim_check.sampleable_functor.p_repr (slim_check.sampleable_ext.proxy_repr α) slim_check.sampleable_ext.p_repr, sample := slim_check.sampleable_functor.sample F (slim_check.sampleable_ext.sample α), shrink := slim_check.sampleable_functor.shrink (slim_check.sampleable_ext.proxy_repr α) slim_check.sampleable_ext.shrink}
Equations
- slim_check.sampleable_ext.bifunctor = {proxy_repr := F (slim_check.sampleable_ext.proxy_repr α) (slim_check.sampleable_ext.proxy_repr β), wf := slim_check.sampleable_bifunctor.wf (slim_check.sampleable_ext.proxy_repr α) (slim_check.sampleable_ext.proxy_repr β) slim_check.sampleable_ext.wf, interp := bifunctor.bimap (slim_check.sampleable_ext.interp α) (slim_check.sampleable_ext.interp β), p_repr := slim_check.sampleable_bifunctor.p_repr (slim_check.sampleable_ext.proxy_repr α) (slim_check.sampleable_ext.proxy_repr β) slim_check.sampleable_ext.p_repr slim_check.sampleable_ext.p_repr, sample := slim_check.sampleable_bifunctor.sample F (slim_check.sampleable_ext.sample α) (slim_check.sampleable_ext.sample β), shrink := slim_check.sampleable_bifunctor.shrink (slim_check.sampleable_ext.proxy_repr α) (slim_check.sampleable_ext.proxy_repr β) slim_check.sampleable_ext.shrink slim_check.sampleable_ext.shrink}
nat.shrink' k n
creates a list of smaller natural numbers by
successively dividing n
by 2 and subtracting the difference from
k
. For example, nat.shrink 100 = [50, 75, 88, 94, 97, 99]
.
Equations
- slim_check.nat.shrink' k n hn ls = dite (n ≤ 1) (λ (h : n ≤ 1), ls.reverse) (λ (h : ¬n ≤ 1), have h₂ : 0 < n, from _, have this : 1 * n / 2 < n, from _, have this : n / 2 < n, from _, let m : ℕ := n / 2 in have h₀ : m ≤ k, from _, have h₃ : 0 < m, from _, have h₁ : k - m < k, from _, slim_check.nat.shrink' k m h₀ (⟨k - m, h₁⟩ :: ls))
nat.shrink n
creates a list of smaller natural numbers by
successively dividing by 2 and subtracting the difference from
n
. For example, nat.shrink 100 = [50, 75, 88, 94, 97, 99]
.
Transport a sampleable
instance from a type α
to a type β
using
functions between the two, going in both directions.
Function g
is used to define the well-founded order that
shrink
is expected to follow.
Equations
- slim_check.nat.sampleable = {wf := nat.has_sizeof, sample := slim_check.gen.sized (λ (sz : ℕ), slim_check.gen.freq [(1, coe <$> slim_check.gen.choose_any (fin (sz ^ 3).succ)), (3, coe <$> slim_check.gen.choose_any (fin sz.succ))] _), shrink := λ (x : ℕ), lazy_list.of_list (slim_check.nat.shrink x)}
iterate_shrink p x
takes a decidable predicate p
and a
value x
of some sampleable type and recursively shrinks x
.
It first calls shrink x
to get a list of candidate sample,
finds the first that satisfies p
and recursively tries
to shrink that one.
Equations
- slim_check.iterate_shrink p = slim_check.iterate_shrink._proof_1.fix (λ (x : α) (f_rec : Π (y : α), has_well_founded.r y x → option α), trace ("" ++ to_string x ++ (" : " ++ to_string (slim_check.sampleable.shrink x).to_list ++ "")) (λ («_» : unit), has_pure.pure ()) >>= λ (_x : unit), lazy_list.find (λ (a : {y // sizeof y < sizeof x}), p ↑a) (slim_check.sampleable.shrink x) >>= λ (y : {y // sizeof y < sizeof x}), f_rec ↑y _ <|> option.some y.val)
Equations
- slim_check.fin.sampleable = slim_check.sampleable.lift ℕ fin.of_nat' subtype.val slim_check.fin.sampleable._proof_1
Equations
- slim_check.fin.sampleable' = slim_check.sampleable.lift ℕ fin.of_nat subtype.val slim_check.fin.sampleable'._proof_1
Equations
- slim_check.pnat.sampleable = slim_check.sampleable.lift ℕ nat.succ_pnat pnat.nat_pred slim_check.pnat.sampleable._proof_1
Equations
- slim_check.int.sampleable = {wf := slim_check.int.has_sizeof, sample := slim_check.gen.sized (λ (sz : ℕ), slim_check.gen.freq [(1, subtype.val <$> slim_check.gen.choose (-(↑sz ^ 3 + 1)) (↑sz ^ 3 + 1) _), (3, subtype.val <$> slim_check.gen.choose (-(↑sz + 1)) (↑sz + 1) _)] _), shrink := λ (x : ℤ), lazy_list.of_list ((slim_check.nat.shrink x.nat_abs).bind (λ (_x : {m // has_well_founded.r m x.nat_abs}), slim_check.int.sampleable._match_1 x _x))}
- slim_check.int.sampleable._match_1 x ⟨y, h⟩ = [⟨↑y, h⟩, ⟨-↑y, _⟩]
Provided two shrinking functions prod.shrink
shrinks a pair (x, y)
by
first shrinking x
and pairing the results with y
and then shrinking
y
and pairing the results with x
.
All pairs either contain x
untouched or y
untouched. We rely on
shrinking being repeated for x
to get maximally shrunken and then
for y
to get shrunken too.
Equations
- slim_check.prod.shrink shr_a shr_b (x₀, x₁) = let xs₀ : lazy_list {y // slim_check.sizeof_lt y (x₀, x₁)} := lazy_list.map (subtype.map (λ (a : α), (a, x₁)) _) (shr_a x₀), xs₁ : lazy_list {y // slim_check.sizeof_lt y (x₀, x₁)} := lazy_list.map (subtype.map (λ (a : β), (x₀, a)) _) (shr_b x₁) in xs₀.append (λ («_» : unit), xs₁)
Equations
- slim_check.prod.sampleable = {wf := λ (α : Type u) (β : Type v) (_inst_1 : has_sizeof α) (_inst_2 : has_sizeof β), prod.has_sizeof α β, sample := λ (α : Type u) (β : Type v) (sama : slim_check.gen α) (samb : slim_check.gen β), uliftable.up sama >>= λ (_p : ulift α), slim_check.prod.sampleable._match_2 α β samb _p, shrink := slim_check.prod.shrink, p_repr := prod.has_repr}
- slim_check.prod.sampleable._match_2 α β samb {down := x} = uliftable.up samb >>= λ (_p : ulift β), slim_check.prod.sampleable._match_1 α β x _p
- slim_check.prod.sampleable._match_1 α β x {down := y} = has_pure.pure (x, y)
Equations
- slim_check.sigma.sampleable = slim_check.sampleable.lift (α × β) (λ (_x : α × β), slim_check.sigma.sampleable._match_1 _x) (λ (_x : Σ (_x : α), β), slim_check.sigma.sampleable._match_2 _x) slim_check.sigma.sampleable._proof_1
- slim_check.sigma.sampleable._match_1 (x, y) = ⟨x, y⟩
- slim_check.sigma.sampleable._match_2 ⟨x, y⟩ = (x, y)
shrinking function for sum types
Equations
- slim_check.sum.shrink shrink_α shrink_β (sum.inr x) = lazy_list.map (subtype.map sum.inr _) (shrink_β x)
- slim_check.sum.shrink shrink_α shrink_β (sum.inl x) = lazy_list.map (subtype.map sum.inl _) (shrink_α x)
Equations
- slim_check.sum.sampleable = {wf := λ (α : Type u) (β : Type v) (Iα : has_sizeof α) (Iβ : has_sizeof β), sum.has_sizeof α β, sample := λ (α : Type u) (β : Type v) (sam_α : slim_check.gen α) (sam_β : slim_check.gen β), uliftable.up_map sum.inl sam_α <|> uliftable.up_map sum.inr sam_β, shrink := λ (α : Type u) (β : Type v) (Iα : has_sizeof α) (Iβ : has_sizeof β) (shr_α : slim_check.shrink_fn α) (shr_β : slim_check.shrink_fn β), slim_check.sum.shrink shr_α shr_β, p_repr := sum.has_repr}
Equations
- slim_check.rat.sampleable = slim_check.sampleable.lift (ℤ × ℕ+) (λ (x : ℤ × ℕ+), x.cases_on rat.mk_pnat) (λ (r : ℚ), (r.num, ⟨r.denom, _⟩)) slim_check.rat.sampleable._proof_1
sampleable_char
can be specialized into customized sampleable char
instances.
The resulting instance has 1 / length
chances of making an unrestricted choice of characters
and it otherwise chooses a character from characters
with uniform probabilities.
Equations
- slim_check.sampleable_char length characters = {wf := char.has_sizeof, sample := slim_check.gen.choose_nat 0 length _ >>= λ (x : ↥(set.Icc 0 length)), ite (x.val = 0) (slim_check.sampleable.sample ℕ >>= λ (n : ℕ), has_pure.pure (char.of_nat n)) (slim_check.gen.choose_nat 0 (characters.length - 1) _ >>= λ (i : ↥(set.Icc 0 (characters.length - 1))), has_pure.pure (characters.mk_iterator.nextn ↑i).curr), shrink := λ (_x : char), lazy_list.nil}
Equations
- slim_check.char.sampleable = slim_check.sampleable_char 3 " 0123abcABC:,;`\\/"
list.shrink_removes
shrinks a list by removing chunks of size k
in
the middle of the list.
Equations
- slim_check.list.shrink_removes k hk xs n hn = dite (k > n) (λ (hkn : k > n), lazy_list.nil) (λ (hkn : ¬k > n), dite (k = n) (λ (hkn' : k = n), have this : 1 < xs.sizeof, from _, lazy_list.singleton ⟨list.nil α, this⟩) (λ (hkn' : ¬k = n), have h₂ : k < xs.length, from _, slim_check.list.shrink_removes._match_1 k hk xs n hn h₂ (λ (xs₁ xs₂ : list α) (h : (xs₁, xs₂) = list.split_at k xs) (h₄ : xs₁ = list.take k xs) (h₃ : xs₂ = list.drop k xs) (this : sizeof xs₂ < sizeof xs) (h₁ : n - k = xs₂.length) (h₅ : ∀ (a : list α), slim_check.sizeof_lt a xs₂ → slim_check.sizeof_lt (xs₁ ++ a) xs), slim_check.list.shrink_removes k hk xs₂ (n - k) h₁) (list.split_at k xs) _))
- slim_check.list.shrink_removes._match_1 k hk xs n hn h₂ _f_1 (xs₁, xs₂) h = have h₄ : xs₁ = list.take k xs, from _, have h₃ : xs₂ = list.drop k xs, from _, have this : sizeof xs₂ < sizeof xs, from _, have h₁ : n - k = xs₂.length, from _, have h₅ : ∀ (a : list α), slim_check.sizeof_lt a xs₂ → slim_check.sizeof_lt (xs₁ ++ a) xs, from _, lazy_list.cons ⟨xs₂, this⟩ (λ («_» : unit), subtype.map (has_append.append xs₁) h₅ <$> _f_1 xs₁ xs₂ h h₄ h₃ this h₁ h₅)
list.shrink_one xs
shrinks list xs
by shrinking only one item in
the list.
Equations
- slim_check.list.shrink_one shr (x :: xs) = (subtype.map (λ (x' : α), x' :: xs) _ <$> shr x).append (λ («_» : unit), subtype.map ((λ (_x : α) (_y : list α), _x :: _y) x) _ <$> slim_check.list.shrink_one shr xs)
- slim_check.list.shrink_one shr list.nil = lazy_list.nil
list.shrink_with shrink_f xs
shrinks xs
by first
considering xs
with chunks removed in the middle (starting with
chunks of size xs.length
and halving down to 1
) and then
shrinks only one element of the list.
This strategy is taken directly from Haskell's QuickCheck
Equations
- slim_check.list.shrink_with shr xs = let n : ℕ := xs.length in ((lazy_list.cons n (λ («_» : unit), lazy_list.map subtype.val (slim_check.sampleable.shrink n).reverse)).bind (λ (k : ℕ), dite (0 < k) (λ (hk : 0 < k), slim_check.list.shrink_removes k hk xs n rfl) (λ (hk : ¬0 < k), lazy_list.nil))).append (λ («_» : unit), slim_check.list.shrink_one shr xs)
Equations
- slim_check.list.sampleable = {wf := λ (α : Type u) (Iα : has_sizeof α), list.has_sizeof α, sample := λ (α : Type u) (sam_α : slim_check.gen α), sam_α.list_of, shrink := λ (α : Type u) (Iα : has_sizeof α) (shr_α : slim_check.shrink_fn α), slim_check.list.shrink_with shr_α, p_repr := list.has_repr}
Equations
- slim_check.Prop.sampleable_ext = {proxy_repr := bool, wf := bool.has_sizeof, interp := coe coe_to_lift, p_repr := bool.has_repr, sample := slim_check.gen.choose_any bool bool.random, shrink := λ (_x : bool), lazy_list.nil}
no_shrink
is a type annotation to signal that
a certain type is not to be shrunk. It can be useful in
combination with other types: e.g. xs : list (no_shrink ℤ)
will result in the list being cut down but individual
integers being kept as is.
Equations
Instances for slim_check.no_shrink
Equations
- slim_check.no_shrink.inhabited = {default := inhabited.default _inst_1}
Introduction of the no_shrink
type.
Equations
Selector of the no_shrink
type.
Equations
Equations
- slim_check.string.sampleable = {wf := slim_check.sampleable.wf (slim_check.sampleable.lift (list char) list.as_string string.to_list slim_check.string.sampleable._proof_1), sample := (slim_check.sampleable.sample char).list_of >>= λ (x : list char), has_pure.pure x.as_string, shrink := slim_check.sampleable.shrink (slim_check.sampleable.lift (list char) list.as_string string.to_list slim_check.string.sampleable._proof_1)}
implementation of sampleable (tree α)
Equations
- slim_check.tree.sample sample n = ite (n > 0) (tree.node <$> sample <*> slim_check.tree.sample sample (n / 2) <*> slim_check.tree.sample sample (n / 2)) (has_pure.pure tree.nil)
rec_shrink x f_rec
takes the recursive call f_rec
introduced
by well_founded.fix
and turns it into a shrinking function whose
result is adequate to use in a recursive call.
Equations
- slim_check.rec_shrink t sh ⟨t', ht'⟩ = (λ (t'' : {y // slim_check.sizeof_lt y t'}), ⟨⟨t''.val, _⟩, _⟩) <$> sh t' ht'
Equations
- slim_check.tree.functor = {map := tree.map, map_const := λ (α β : Type u_1), tree.map ∘ function.const β}
Recursion principle for shrinking tree-like structures.
Equations
- slim_check.rec_shrink_with shrink_a = _.fix (λ (t : α) (f_rec : Π (y : α), sizeof_measure α y t → lazy_list {y_1 // slim_check.sizeof_lt y_1 y}), (lazy_list.of_list (shrink_a t (λ (_x : {y // slim_check.sizeof_lt y t}), slim_check.rec_shrink_with._match_1 t f_rec _x))).join)
- slim_check.rec_shrink_with._match_1 t f_rec ⟨t', h⟩ = slim_check.rec_shrink t f_rec ⟨t', h⟩
tree.shrink_with shrink_f t
shrinks xs
by using the empty tree,
each subtrees, and by shrinking the subtree to recombine them.
This strategy is taken directly from Haskell's QuickCheck
Equations
- slim_check.tree.shrink_with shrink_a = slim_check.rec_shrink_with (λ (t : tree α), slim_check.tree.shrink_with._match_1 shrink_a t t)
- slim_check.tree.shrink_with._match_1 shrink_a t (tree.node x t₀ t₁) = λ (f_rec : slim_check.shrink_fn {y // slim_check.sizeof_lt y (tree.node x t₀ t₁)}), have h₂ : slim_check.sizeof_lt tree.nil (tree.node x t₀ t₁), from _, have h₀ : slim_check.sizeof_lt t₀ (tree.node x t₀ t₁), from _, have h₁ : slim_check.sizeof_lt t₁ (tree.node x t₀ t₁), from _, [lazy_list.of_list [⟨tree.nil α, h₂⟩, ⟨t₀, h₀⟩, ⟨t₁, h₁⟩], lazy_list.map (λ (_x : {y // slim_check.sizeof_lt y (x, ⟨t₀, h₀⟩, ⟨t₁, h₁⟩)}), slim_check.tree.shrink_with._match_2 x t₀ t₁ h₀ h₁ _x) (slim_check.prod.shrink shrink_a (slim_check.prod.shrink f_rec f_rec) (x, ⟨t₀, h₀⟩, ⟨t₁, h₁⟩))]
- slim_check.tree.shrink_with._match_1 shrink_a t tree.nil = λ (f_rec : slim_check.shrink_fn {y // slim_check.sizeof_lt y tree.nil}), list.nil
- slim_check.tree.shrink_with._match_2 x t₀ t₁ h₀ h₁ ⟨(y, ⟨t'₀, _x⟩, ⟨t'₁, _x_1⟩), hy⟩ = ⟨tree.node y t'₀ t'₁, _⟩
Equations
- slim_check.sampleable_tree = {wf := λ (α : Type u_1) (Iα : has_sizeof α), tree.has_sizeof_inst α, sample := λ (α : Type u_1) (sam_α : slim_check.gen α), slim_check.gen.sized (slim_check.tree.sample sam_α), shrink := λ (α : Type u_1) (Iα : has_sizeof α) (shr_α : slim_check.shrink_fn α), slim_check.tree.shrink_with shr_α, p_repr := tree.has_repr}
Type tag that signals to slim_check
to use small values for a given type.
Equations
- slim_check.small α = α
Instances for slim_check.small
Add the small
type tag
Equations
- slim_check.small.mk x = x
Type tag that signals to slim_check
to use large values for a given type.
Equations
- slim_check.large α = α
Instances for slim_check.large
Add the large
type tag
Equations
- slim_check.large.mk x = x
Equations
Equations
Equations
- slim_check.small.inhabited = {default := inhabited.default _inst_1}
Equations
- slim_check.large.inhabited = {default := inhabited.default _inst_1}
Equations
- slim_check.small.sampleable_functor = {wf := λ (α : Type u_1) (_x : has_sizeof α), _x, sample := λ (α : Type u_1) (samp : slim_check.gen α), slim_check.gen.resize (λ (n : ℕ), n / 5 + 5) samp, shrink := λ (α : Type u_1) (_x : has_sizeof α), id, p_repr := λ (α : Type u_1), id}
Equations
- slim_check.large.sampleable_functor = {wf := λ (α : Type u_1) (_x : has_sizeof α), _x, sample := λ (α : Type u_1) (samp : slim_check.gen α), slim_check.gen.resize (λ (n : ℕ), n * 5) samp, shrink := λ (α : Type u_1) (_x : has_sizeof α), id, p_repr := λ (α : Type u_1), id}
Equations
- slim_check.ulift.sampleable_functor = {wf := λ (α : Type v) (h : has_sizeof α), {sizeof := λ (_x : ulift α), slim_check.ulift.sampleable_functor._match_1 α h _x}, sample := λ (α : Type v) (samp : slim_check.gen α), uliftable.up_map ulift.up samp, shrink := λ (α : Type v) (_x : has_sizeof α) (shr : slim_check.shrink_fn α) (_x_1 : ulift α), slim_check.ulift.sampleable_functor._match_2 α _x shr _x_1, p_repr := λ (α : Type v) (h : has_repr α), {repr := repr ∘ ulift.down}}
- slim_check.ulift.sampleable_functor._match_1 α h {down := x} = sizeof x
- slim_check.ulift.sampleable_functor._match_2 α _x shr {down := x} = lazy_list.map (subtype.map ulift.up _) (shr x)
Subtype instances #
The following instances are meant to improve the testing of properties of the form
∀ i j, i ≤ j, ...
The naive way to test them is to choose two numbers i
and j
and check that
the proper ordering is satisfied. Instead, the following instances make it
so that j
will be chosen with considerations to the required ordering
constraints. The benefit is that we will not have to discard any choice
of j
.
Subtypes of ℕ
#
Equations
- slim_check.nat_le.sampleable = {wf := subtype.has_sizeof (λ (x : ℕ), x ≤ y), sample := slim_check.gen.choose_nat 0 y slim_check.nat_le.sampleable._proof_1 >>= λ (_p : ↥(set.Icc 0 y)), slim_check.nat_le.sampleable._match_1 _p, shrink := λ (_x : {x // x ≤ y}), slim_check.nat_le.sampleable._match_2 _x}
- slim_check.nat_le.sampleable._match_1 ⟨x, h⟩ = has_pure.pure ⟨x, _⟩
- slim_check.nat_le.sampleable._match_2 ⟨x, h⟩ = (λ (a : {x' // x' < x}), a.rec_on (λ (x' : ℕ) (h' : x' < x), ⟨⟨x', _⟩, h'⟩)) <$> slim_check.sampleable.shrink x
Equations
- slim_check.nat_ge.sampleable = {wf := subtype.has_sizeof (λ (y : ℕ), x ≤ y), sample := slim_check.sampleable.sample ℕ >>= λ (_p : ℕ), slim_check.nat_ge.sampleable._match_1 _p, shrink := λ (_x : {y // x ≤ y}), slim_check.nat_ge.sampleable._match_2 _x}
- slim_check.nat_ge.sampleable._match_1 y = has_pure.pure ⟨x + y, _⟩
- slim_check.nat_ge.sampleable._match_2 ⟨y, h⟩ = (λ (a : {y' // sizeof y' < sizeof (y - x)}), a.rec_on (λ (δ : ℕ) (h' : sizeof δ < sizeof (y - x)), ⟨⟨x + δ, _⟩, _⟩)) <$> slim_check.sampleable.shrink (y - x)
Equations
- slim_check.nat_gt.sampleable = {wf := subtype.has_sizeof (λ (y : ℕ), x < y), sample := slim_check.sampleable.sample ℕ >>= λ (_p : ℕ), slim_check.nat_gt.sampleable._match_1 _p, shrink := λ (x_1 : {y // x < y}), slim_check.sampleable.shrink x_1}
- slim_check.nat_gt.sampleable._match_1 y = has_pure.pure ⟨x + y + 1, _⟩
Subtypes of any linear_ordered_add_comm_group
#
Equations
- slim_check.le.sampleable = {wf := subtype.has_sizeof (λ (x : α), x ≤ y), sample := slim_check.sampleable.sample α >>= λ (x : α), has_pure.pure ⟨y - |x|, _⟩, shrink := λ (_x : {x // x ≤ y}), lazy_list.nil}
Equations
- slim_check.ge.sampleable = {wf := subtype.has_sizeof (λ (y : α), x ≤ y), sample := slim_check.sampleable.sample α >>= λ (y : α), has_pure.pure ⟨x + |y|, _⟩, shrink := λ (_x : {y // x ≤ y}), lazy_list.nil}
Subtypes of ℤ
#
Specializations of le.sampleable
and ge.sampleable
for ℤ
to help instance search.
Equations
- slim_check.perm.slim_check = {wf := subtype.has_sizeof (λ (ys : list α), xs ~ ys), sample := slim_check.gen.permutation_of xs, shrink := λ (_x : {ys // xs ~ ys}), lazy_list.nil}
Equations
- slim_check.perm'.slim_check = {wf := subtype.has_sizeof (λ (ys : list α), ys ~ xs), sample := subtype.map id list.perm.symm <$> slim_check.gen.permutation_of xs, shrink := λ (_x : {ys // ys ~ xs}), lazy_list.nil}
Print (at most) 10 samples of a given type to stdout for debugging.
Equations
- slim_check.print_samples g = io.run_rand (uliftable.down (list.mmap (g.run ∘ ulift.up) (list.range 10) >>= λ (xs : list t), has_pure.pure {down := list.map repr xs})) >>= λ (xs : list string), list.mmap' io.put_str_ln xs