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.

Equations

• Plausible.Gen α = ReaderT (ULift Nat) Plausible.Rand α

@[inline]

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

Equations

• x.up = do let size ← read liftM (Plausible.Rand.up (ReaderT.run x { down := size.down }))

@[inline]

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

Equations

• x.down = do let size ← read liftM (Plausible.Rand.down (ReaderT.run x { down := size.down }))

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

Lift Random.random to the Gen monad.

Equations

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

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

Lift BoundedRandom.randomR to the Gen monad.

Equations

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

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

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

Equations

• Plausible.Gen.chooseNatLt lo hi h = do let __discr ← Plausible.Gen.choose Nat (lo + 1) hi ⋯ match __discr with | ⟨val, h⟩ => pure ⟨val - 1, ⋯⟩

def Plausible.Gen.getSize : Plausible.Gen Nat

Get access to the size parameter of the Gen monad.

Equations

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

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

Apply a function to the size parameter.

Equations

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

def Plausible.Gen.chooseNat : Plausible.Gen Nat

Choose a Nat between 0 and getSize.

Equations

• Plausible.Gen.chooseNat = do let __do_lift ← Plausible.Gen.getSize let a ← Plausible.Gen.choose Nat 0 __do_lift ⋯ pure a.val

def Plausible.Gen.arrayOf {α : Type u} (x : Plausible.Gen α) : Plausible.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 Plausible.Gen.listOf {α : Type u} (x : Plausible.Gen α) : Plausible.Gen (List α)

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

Equations

• x.listOf = do let arr ← x.arrayOf pure arr.toList

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

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

Equations

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

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

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

Equations

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

def Plausible.Gen.permutationOf {α : Type u} (xs : List α) : Plausible.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.
• Plausible.Gen.permutationOf [] = pure ⟨[], ⋯⟩

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

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

Equations

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

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

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

Equations

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