Gen Monad

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

Main definitions

• Gen monad

References

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

@[reducible, inline]

abbrev Plausible.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.

@[inline]

def Plausible.Gen.up {α : Type u} (x : Gen α) : Gen (ULift α)

@[inline]

def Plausible.Gen.down {α : Type u_1} (x : Gen (ULift α)) : Gen α

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

Lift Random.random to the Gen monad.

def Plausible.Gen.choose (α : Type u) [LE α] [BoundedRandom Id α] (lo hi : α) (h : lo ≤ hi) : Gen { a : α // lo ≤ a ∧ a ≤ hi }

Lift BoundedRandom.randomR to the Gen monad.

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

Generate a Nat example between lo and hi (exclusively).

def Plausible.Gen.getSize : Gen Nat

Get access to the size parameter of the Gen monad.

def Plausible.Gen.resize {α : Type u_1} (f : Nat → Nat) (x : Gen α) : Gen α

Apply a function to the size parameter.

def Plausible.Gen.chooseNat : Gen Nat

Choose a Nat between 0 and getSize.

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

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

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

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

def Plausible.Gen.oneOf {α : Type u} (xs : Array (Gen α)) (pos : 0 < xs.size := by decide) : Gen α

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

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

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

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

Generate a random permutation of a given list.

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

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

def Plausible.Gen.run {α : Type} (x : Gen α) (size : Nat) : BaseIO α

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