Documentation

Plausible.Arbitrary

`Arbitrary` Typeclass #

The Arbitrary typeclass represents types for which there exists a random generator suitable for property-based testing, similar to Haskell QuickCheck's Arbitrary typeclass and Rocq/Coq QuickChick's Gen typeclass.

(Note: the SampleableExt involvs types which have both a generator & a shrinker, and possibly a non trivial proxy type, whereas Arbitrary describes types which have a generator only.)

Main definitions #

Arbitrary typeclass

References #

class Plausible.Arbitrary (α : Type u) :

The Arbitrary typeclass represents types for which there exists a random generator suitable for property-based testing.

This is the equivalent of Haskell QuickCheck's Arbitrary typeclass.
In QuickChick, this typeclass is called Gen, but Gen is already a reserved keyword in Plausible, so we call this typeclass Arbitrary following the Haskell QuickCheck convention).

arbitrary : Gen α
A random generator for values of the given type.

Instances

def Plausible.Arbitrary.runArbitrary {α : Type} [Arbitrary α] (size : Nat) :

IO α

Samples from the generator associated with the Arbitrary instance for a type, using size as the size parameter for the generator. To invoke this function, you will need to specify what type α is, for example by doing runArbitrary (α := Nat) 10.

Equations

Plausible.Arbitrary.runArbitrary size = Plausible.Arbitrary.arbitrary.run size

Instances For

instance Plausible.Sum.Arbitrary {α β : Type} [Plausible.Arbitrary α] [Plausible.Arbitrary β] :

Plausible.Arbitrary (α ⊕ β)

Equations

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

instance Plausible.Unit.Arbitrary :

Plausible.Arbitrary Unit

Equations

Plausible.Unit.Arbitrary = { arbitrary := pure () }

instance Plausible.Sigma.Arbitrary {α : Type u_1} {β : Type u_2} [Plausible.Arbitrary α] [Plausible.Arbitrary β] :

Plausible.Arbitrary ((_ : α) × β)

Equations

Plausible.Sigma.Arbitrary = { arbitrary := do let p ← Plausible.Arbitrary.arbitrary.prodOf Plausible.Arbitrary.arbitrary pure ⟨p.fst, p.snd⟩ }

instance Plausible.Nat.Arbitrary :

Plausible.Arbitrary Nat

Equations

Plausible.Nat.Arbitrary = { arbitrary := do let __do_lift ← Plausible.Gen.getSize let a ← Plausible.Gen.choose Nat 0 __do_lift ⋯ pure a.val }

instance Plausible.Fin.Arbitrary {n : Nat} :

Plausible.Arbitrary (Fin n.succ)

Equations

Plausible.Fin.Arbitrary = { arbitrary := do let __do_lift ← Plausible.Gen.getSize let m ← Plausible.Gen.choose Nat 0 (min __do_lift n) ⋯ pure (Fin.ofNat n.succ m.val) }

instance Plausible.BitVec.Arbitrary {n : Nat} :

Plausible.Arbitrary (BitVec n)

Equations

Plausible.BitVec.Arbitrary = { arbitrary := do let __do_lift ← Plausible.Gen.getSize let m ← Plausible.Gen.choose Nat 0 (min __do_lift (2 ^ n)) ⋯ pure (BitVec.ofNat n m.val) }

instance Plausible.UInt8.Arbitrary :

Plausible.Arbitrary UInt8

Equations

Plausible.UInt8.Arbitrary = { arbitrary := do let __do_lift ← Plausible.Gen.getSize let n ← Plausible.Gen.choose Nat 0 (min __do_lift UInt8.size) ⋯ pure (UInt8.ofNat n.val) }

instance Plausible.UInt16.Arbitrary :

Plausible.Arbitrary UInt16

Equations

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

instance Plausible.UInt32.Arbitrary :

Plausible.Arbitrary UInt32

Equations

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

instance Plausible.UInt64.Arbitrary :

Plausible.Arbitrary UInt64

Equations

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

instance Plausible.USize.Arbitrary :

Plausible.Arbitrary USize

Equations

Plausible.USize.Arbitrary = { arbitrary := do let __do_lift ← Plausible.Gen.getSize let n ← Plausible.Gen.choose Nat 0 (min __do_lift USize.size) ⋯ pure (USize.ofNat n.val) }

instance Plausible.Int.Arbitrary :

Plausible.Arbitrary Int

Equations

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

instance Plausible.Bool.Arbitrary :

Plausible.Arbitrary Bool

Equations

Plausible.Bool.Arbitrary = { arbitrary := Plausible.Gen.chooseAny Bool }

def Plausible.Char.arbitraryFromList (p : Nat) (chars : List Char) (pos : 0 < chars.length) :

This can be specialized into customized Arbitrary Char instances. The resulting instance has 1 / p chances of making an unrestricted choice of characters and it otherwise chooses a character from chars with uniform probability.

Equations

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

Instances For

instance Plausible.Char.arbitraryDefaultInstance :

Pick a simple ASCII character 2/3s of the time, and otherwise pick any random Char encoded by the next Nat (or \0 if there is no such character)

Equations

Plausible.Char.arbitraryDefaultInstance = Plausible.Char.arbitraryFromList 3 " 0123abcABC:,;`\\/".toList Plausible.Char.arbitraryDefaultInstance._proof_1

instance Plausible.Option.Arbitrary {α : Type} [Plausible.Arbitrary α] :

Plausible.Arbitrary (Option α)

Equations

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

instance Plausible.Prod.Arbitrary {α : Type u} {β : Type v} [Plausible.Arbitrary α] [Plausible.Arbitrary β] :

Plausible.Arbitrary (α × β)

Equations

Plausible.Prod.Arbitrary = { arbitrary := Plausible.Arbitrary.arbitrary.prodOf Plausible.Arbitrary.arbitrary }

instance Plausible.List.Arbitrary {α : Type u_1} [Plausible.Arbitrary α] :

Plausible.Arbitrary (List α)

Equations

Plausible.List.Arbitrary = { arbitrary := Plausible.Arbitrary.arbitrary.listOf }

instance Plausible.ULift.Arbitrary {α : Type (max u_1 u_2)} [Plausible.Arbitrary α] :

Plausible.Arbitrary (ULift α)

Equations

Plausible.ULift.Arbitrary = { arbitrary := do let x ← Plausible.Arbitrary.arbitrary pure { down := x } }

instance Plausible.String.Arbitrary :

Plausible.Arbitrary String

Equations

Plausible.String.Arbitrary = { arbitrary := do let __do_lift ← Plausible.Arbitrary.arbitrary.listOf pure { data := __do_lift } }

instance Plausible.Array.Arbitrary {α : Type u_1} [Plausible.Arbitrary α] :

Plausible.Arbitrary (Array α)

Equations

Plausible.Array.Arbitrary = { arbitrary := Plausible.Arbitrary.arbitrary.arrayOf }