Deriving Handler for `Arbitrary` #

This file defines a handler which automatically derives Arbitrary instances for inductive types.

(Note that the deriving handler technically derives ArbitraryFueled instancces, but every ArbitraryFueled instance automatically results in an Arbitrary instance, as detailed in Arbitrary.lean.)

Note that the resulting Arbitrary and ArbitraryFueled instance should be considered to be opaque, following the convention for the deriving handler for Mathlib's Encodable typeclass.

Example usage:

-- Datatype for binary trees
inductive Tree
  | Leaf : Tree
  | Node : Nat → Tree → Tree → Tree
  deriving Arbitrary

To sample from a derived generator, users can simply call Arbitrary.runArbitrary, specify the type for the desired generated values and provide some Nat to act as the generator's fuel parameter (10 in the example below):

#eval Arbitrary.runArbitrary (α := Tree) 10

To view the code for the derived generator, users can enable trace messages using the plausible.deriving.arbitrary trace class as follows:

set_option trace.plausible.deriving.arbitrary true

Main definitions #

Deriving handler for ArbitraryFueled typeclass

source

def Plausible.getCtorArgsNamesAndTypes (_header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) (ctorName : Lean.Name) :

Lean.MetaM (Array (Lean.Name × Lean.Expr))

Takes the name of a constructor for an algebraic data type and returns an array containing (argument_name, argument_type) pairs.

If the algebraic data type is defined using anonymous constructor argument syntax, i.e.

inductive T where
  C1 : τ1 → … → τn
  …

Lean produces macro scopes when we try to access the names for the constructor args. In this case, we remove the macro scopes so that the name is user-accessible. (This will result in constructor argument names being non-unique in the array that is returned -- it is the caller's responsibility to produce fresh names.)

Equations

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

Instances For

source

def Plausible.mkHeaderWithOnlyImplicitBinders (className : Lean.Name) (arity : Nat) (indVal : Lean.InductiveVal) :

Lean.Elab.TermElabM Lean.Elab.Deriving.Header

Variant of Deriving.Util.mkHeader where we don't add an explicit binder of the form ($targetName : $targetType) to the field binders (i.e. binders contains only implicit binders)

Equations

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

Instances For

source

def Plausible.mkArbitraryFueledInstanceCmds (ctx : Lean.Elab.Deriving.Context) (typeNames : Array Lean.Name) (useAnonCtor : Bool := true) :

Lean.Elab.TermElabM (Array Lean.Command)

Variant of Deriving.Util.mkInstanceCmds which is specialized to creating ArbitraryFueled instances that have Arbitrary inst-implicit binders.

Note that we can't use mkInstanceCmds out of the box, since it expects the inst-implicit binders and the instance we're creating to both belong to the same typeclass.

Equations