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

def Plausible.instReprGenError.repr : GenError → Nat → Std.Format

Equations

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

instance Plausible.instReprGenError : Repr GenError

Equations

• Plausible.instReprGenError = { reprPrec := Plausible.instReprGenError.repr }

instance Plausible.instBEqGenError : BEq GenError

Equations

• Plausible.instBEqGenError = { beq := Plausible.instBEqGenError.beq }

def Plausible.instBEqGenError.beq : GenError → GenError → Bool

Equations

• Plausible.instBEqGenError.beq (Plausible.GenError.genError a) (Plausible.GenError.genError b) = (a == b)
• Plausible.instBEqGenError.beq x✝¹ x✝ = false

def Plausible.Gen.genericFailure : GenError

Equations

• Plausible.Gen.genericFailure = Plausible.GenError.genError "Generation failure."

@[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 Except monad

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 a) = IO.userError (toString "generation failure: " ++ toString a)

@[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

The following section defines various combinators for generators, which are used in the body of derived generators (for derived Arbitrary instances).

The code for these combinators closely mirrors those used in Rocq/Coq QuickChick (see link in the References section below).

References

• https://github.com/QuickChick/QuickChick/blob/master/src/Generators.v

def Plausible.Gen.oneOfWithDefault {α : Type} (default : Gen α) (gs : List (Gen α)) : Gen α

Picks one of the generators in gs at random, returning the default generator if gs is empty.

(This is a more ergonomic version of Plausible's Gen.oneOf which doesn't require the caller to supply a proof that the list index is in bounds.)

Equations

• default.oneOfWithDefault [] = default
• default.oneOfWithDefault gs = do let idx ← Plausible.Gen.choose Nat 0 (gs.length - 1) ⋯ gs.getD idx.val default

def Plausible.Gen.frequency {α : Type} (default : Gen α) (gs : List (Nat × Gen α)) : Gen α

frequency picks a generator from the list gs according to the weights in gs. If gs is empty, the default generator is returned.

Equations

• default.frequency gs = do let n ← Plausible.Gen.choose Nat 0 ((List.map Prod.fst gs).sum - 1) ⋯ (Plausible.Gen.pick✝ default gs n.val).snd

def Plausible.Gen.sized {α : Type} (f : Nat → Gen α) : Gen α

sized f constructs a generator that depends on its size parameter

Equations

• Plausible.Gen.sized f = Plausible.Gen.getSize >>= f

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