Gen Monad

This monad is used to formulate randomized computations with a parameter to specify the desired size of the result. This is a port of the Haskell QuickCheck library.

Main definitions

• Gen monad

Tags

random testing

References

• https://hackage.haskell.org/package/QuickCheck

ink

@[inline]

abbrev SlimCheck.Gen (α : Type u) : Type u

Monad to generate random examples to test properties with. It has a Nat parameter so that the caller can decide on the size of the examples.

Equations

• SlimCheck.Gen α = ReaderT (ULift ℕ) Rand α

ink

def SlimCheck.Gen.chooseAny (α : Type u) [inst : Random α] : SlimCheck.Gen α

Lift Random.random to the Gen monad.

Equations

• SlimCheck.Gen.chooseAny α x = Random.rand α

ink

def SlimCheck.Gen.choose (α : Type u) [inst : Preorder α] [inst : BoundedRandom α] (lo : α) (hi : α) (h : lo ≤ hi) : SlimCheck.Gen { a // lo ≤ a ∧ a ≤ hi }

Lift BoundedRandom.randomR to the Gen monad.

Equations

• SlimCheck.Gen.choose α lo hi h x = Random.randBound α lo hi h

ink

theorem SlimCheck.Gen.chooseNatLt_aux {lo : ℕ} {hi : ℕ} (a : ℕ) (h : Nat.succ lo ≤ a ∧ a ≤ hi) : lo ≤ Nat.pred a ∧ Nat.pred a < hi

ink

def SlimCheck.Gen.chooseNatLt (lo : ℕ) (hi : ℕ) (h : lo < hi) : SlimCheck.Gen { a // lo ≤ a ∧ a < hi }

Generate a Nat example between x and y (exclusively).

Equations

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

ink

def SlimCheck.Gen.getSize : SlimCheck.Gen ℕ

Get access to the size parameter of the Gen monad.

Equations

• SlimCheck.Gen.getSize = do let __do_lift ← read pure __do_lift.down

ink

def SlimCheck.Gen.resize {α : Type u_1} (f : ℕ → ℕ) (x : SlimCheck.Gen α) : SlimCheck.Gen α

Apply a function to the size parameter.

Equations

• SlimCheck.Gen.resize f x = withReader (ULift.up ∘ f ∘ ULift.down) x

ink

def SlimCheck.Gen.arrayOf {α : Type} (x : SlimCheck.Gen α) : SlimCheck.Gen (Array α)

Create an Array of examples using x. The size is controlled by the size parameter of Gen.

Equations

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

ink

def SlimCheck.Gen.listOf {α : Type} (x : SlimCheck.Gen α) : SlimCheck.Gen (List α)

Create an List of examples using x. The size is controlled by the size parameter of Gen.

Equations

• SlimCheck.Gen.listOf x = SlimCheck.Gen.arrayOf x >>= pure ∘ Array.toList

ink

def SlimCheck.Gen.oneOf {α : Type} (xs : Array (SlimCheck.Gen α)) (pos : autoParam (0 < Array.size xs) _auto✝) : SlimCheck.Gen α

Given a list of example generators, choose one to create an example.

Equations

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

ink

def SlimCheck.Gen.elements {α : Type} (xs : List α) (pos : 0 < List.length xs) : SlimCheck.Gen α

Given a list of examples, choose one to create an example.

Equations

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

ink

def SlimCheck.Gen.permutationOf {α : Type} (xs : List α) : SlimCheck.Gen { ys // ys ~ xs }

Generate a random permutation of a given list.

Equations

• One or more equations did not get rendered due to their size.
• SlimCheck.Gen.permutationOf [] = pure { val := [], property := (_ : [] ~ []) }

ink

def SlimCheck.Gen.prodOf {α : Type u} {β : Type u} (x : SlimCheck.Gen α) (y : SlimCheck.Gen β) : SlimCheck.Gen (α × β)

Given two generators produces a tuple consisting out of the result of both

Equations

• SlimCheck.Gen.prodOf x y = do let __do_lift ← x let __do_lift_1 ← y pure (__do_lift, __do_lift_1)

ink

def SlimCheck.Gen.run {α : Type} (x : SlimCheck.Gen α) (size : ℕ) : BaseIO α

Execute a Gen inside the IO monad using size as the example size

Equations

• SlimCheck.Gen.run x size = IO.runRand (ReaderT.run x { down := size })