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

@[reducible, 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.{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 : lo.succ ≤ a ∧ a ≤ hi) : lo ≤ a.pred ∧ a.pred < 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

• SlimCheck.Gen.chooseNatLt lo hi h = Subtype.map Nat.pred ⋯ <$> SlimCheck.Gen.choose ℕ lo.succ hi ⋯

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

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

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

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

Equations

• SlimCheck.Gen.oneOf xs pos = do let __discr ← ULiftable.up (SlimCheck.Gen.chooseNatLt 0 xs.size pos) match __discr with | { down := ⟨x, ⋯⟩ } => xs.get ⟨x, h2⟩

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

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

Equations

• SlimCheck.Gen.elements xs pos = do let __discr ← ULiftable.up (SlimCheck.Gen.chooseNatLt 0 xs.length pos) match __discr with | { down := ⟨x, ⋯⟩ } => pure (xs.get ⟨x, h2⟩)

def SlimCheck.Gen.permutationOf {α : Type u} (xs : List α) : SlimCheck.Gen { ys : List α // xs.Perm 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 ⟨[], ⋯⟩

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

• x.prodOf y = do let __discr ← ULiftable.up x match __discr with | { down := a } => do let __discr ← ULiftable.up y match __discr with | { down := b } => pure (a, b)

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

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

Equations

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