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 involves 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

• https://hackage.haskell.org/package/QuickCheck
• https://softwarefoundations.cis.upenn.edu/qc-current/QuickChickInterface.html

class Plausible.Arbitrary (α : Type u) : 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.

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.

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

instance Plausible.Unit.Arbitrary : Plausible.Arbitrary Unit

instance Plausible.Sigma.Arbitrary {α : Type u_1} {β : Type u_2} [Plausible.Arbitrary α] [Plausible.Arbitrary β] : Plausible.Arbitrary ((_ : α) × β)

instance Plausible.Nat.Arbitrary : Plausible.Arbitrary Nat

instance Plausible.Fin.Arbitrary {n : Nat} : Plausible.Arbitrary (Fin n.succ)

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

instance Plausible.UInt8.Arbitrary : Plausible.Arbitrary UInt8

instance Plausible.UInt16.Arbitrary : Plausible.Arbitrary UInt16

instance Plausible.UInt32.Arbitrary : Plausible.Arbitrary UInt32

instance Plausible.UInt64.Arbitrary : Plausible.Arbitrary UInt64

instance Plausible.USize.Arbitrary : Plausible.Arbitrary USize

instance Plausible.Int.Arbitrary : Plausible.Arbitrary Int

instance Plausible.Bool.Arbitrary : Plausible.Arbitrary Bool

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

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.

instance Plausible.Char.arbitraryDefaultInstance : Arbitrary Char

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)

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

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

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

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

instance Plausible.String.Arbitrary : Plausible.Arbitrary String

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