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

inductive Plausible.GenError : Type

Error thrown on generation failure, e.g. because you've run out of resources.

• genError : String → GenError

instance Plausible.instInhabitedGenError : Inhabited GenError

Equations

• Plausible.instInhabitedGenError = { default := Plausible.instInhabitedGenError.default }

def Plausible.instInhabitedGenError.default : GenError

Equations

• Plausible.instInhabitedGenError.default = Plausible.GenError.genError default

@[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. It allows failure to generate via the ExceptT transformer

Equations

• Plausible.Gen α = Plausible.RandT (ReaderT (ULift Nat) (Except Plausible.GenError)) α

instance Plausible.instMonadLiftGen {m : Type u_1 → Type u_2} [MonadLiftT m (ReaderT (ULift Nat) (Except GenError))] : MonadLiftT (RandGT StdGen m) Gen

Equations

• Plausible.instMonadLiftGen = { monadLift := fun {α : Type ?u.20} (m_1 : Plausible.RandGT StdGen m α) => liftM ∘ StateT.run m_1 }

instance Plausible.instMonadErrorGen : MonadExcept GenError Gen

Equations

• Plausible.instMonadErrorGen = inferInstance

def Plausible.Gen.genFailure (e : GenError) : IO.Error

Equations

• Plausible.Gen.genFailure (Plausible.GenError.genError mes) = IO.userError (toString "generation failure: " ++ toString mes)

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Lift Random.random to the Gen monad.

Equations

• Plausible.Gen.chooseAny α = liftM (Plausible.Random.rand α)

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.

Equations

• Plausible.Gen.choose α lo hi h = liftM (Plausible.Random.randBound α lo hi h)

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).

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 : 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 : Gen α) : 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 : 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 : Gen α) : 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 : Gen α) : Gen (List α)

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

Equations

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

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.

Equations

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

def Plausible.Gen.elements {α : Type u} (xs : List α) (pos : 0 < xs.length) : 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 α) : 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 : Gen α) (y : Gen β) : 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)

instance Plausible.instMonadLiftStateIOGen : MonadLift (ReaderT (ULift Nat) (Except GenError)) IO

Equations

• Plausible.instMonadLiftStateIOGen = { monadLift := fun {α : Type} (m : ReaderT (ULift Nat) (Except Plausible.GenError) α) => Plausible.errorOfGenError✝ (m.run { down := 0 }) }

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

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

Equations

• x.run size = Plausible.runRand (liftM x)

def Plausible.Gen.printSamples {t : Type} [Repr t] (g : Gen t) : IO PUnit

Print (at most) 10 samples of a given type to stdout for debugging. Sadly specialized to Type 0

Equations

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

def Plausible.Gen.runUntil {α : Type} (attempts : Option Nat := none) (x : Gen α) (size : Nat) : IO α

Execute a Gen until it actually produces an output. May diverge for bad generators!

Equations

• Plausible.Gen.runUntil attempts x size = (Plausible.Gen.runUntil.repeatGen attempts x).run size

partial def Plausible.Gen.runUntil.repeatGen {α : Type} (attempts : Option Nat) (x : Gen α) : Gen α

def Plausible.Gen.runUntil.decr : Option Nat → Option Nat

Equations

• Plausible.Gen.runUntil.decr (some n) = some (n - 1)
• Plausible.Gen.runUntil.decr none = none

def Plausible.test : Gen Nat

Equations

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