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

@[inline, reducible]

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.{u, 0} ℕ) Rand α

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

Lift Random.random to the Gen monad.

Equations

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

def SlimCheck.Gen.choose (α : Type u) [Preorder α] [BoundedRandom Id α] (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

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

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.

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

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

def SlimCheck.Gen.arrayOf {α : Type u} (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.

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

Create a 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

def SlimCheck.Gen.oneOf {α : Type u} (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.

def SlimCheck.Gen.elements {α : Type u} (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.

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

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 := (_ : List.Perm [] []) }

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

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

Equations

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

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 (liftM (ReaderT.run x { down := size }))