ToExpr deriving handler

This module defines a ToExpr deriving handler for inductive types. It supports mutually inductive types as well.

The ToExpr deriving handlers support universe level polymorphism, via the Lean.ToLevel class. To use ToExpr in places where there is universe polymorphism, make sure a [ToLevel.{u}] instance is available, though be aware that the ToLevel mechanism does not support max or imax expressions.

Implementation note: this deriving handler was initially modeled after the Repr deriving handler, but

1. we need to account for universe levels,
2. the ToExpr class has two fields rather than one, and
3. we don't handle structures specially.

def Lean.Elab.Deriving.ToExpr.mkAppNTerm (f : Term) (args : Array Term) : MetaM Term

Given args := #[e₁, e₂, …, eₙ], constructs the syntax Expr.app (… (Expr.app (Expr.app f e₁) e₂) …) eₙ.

Equations

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

def Lean.Elab.Deriving.ToExpr.updateIndType (indVal : InductiveVal) (t : Term) : TermElabM Term

Fixes the output of mkInductiveApp to explicitly reference universe levels.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkToTypeExpr (indVal : InductiveVal) (argNames : Array Name) : TermElabM Term

Creates a term that evaluates to an expression representing the inductive type. Uses toExpr and toTypeExpr for the arguments to the type constructor.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) (levelInsts : Array Term) : TermElabM Term

Creates the body of the toExpr function for the ToExpr instance, which is a match expression that calls toExpr and toTypeExpr to assemble an expression for a given term. For recursive inductive types, auxFunName refers to the ToExpr instance for the current type. For mutually recursive types, we rely on the local instances set up by mkLocalInstanceLetDecls.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkToExprBody.mkAlts (header : Header) (indVal : InductiveVal) (auxFunName : Name) (levelInsts : Array Term) : TermElabM (Array (TSyntax `Lean.Parser.Term.matchAlt))

Create the match cases, one per constructor.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkLocalInstanceLetDecls (ctx : Context) (argNames : Array Name) (levelInsts : Array Term) : TermElabM (Array (TSyntax `Lean.Parser.Term.letDecl))

For nested and mutually recursive inductive types, we define partial instances, and the strategy is to have local ToExpr instances in scope for the body of each instance. This way, each instance can freely use toExpr and toTypeExpr for each of the types in ctx.

This is a modified copy of Lean.Elab.Deriving.mkLocalInstanceLetDecls, since we need to include the toTypeExpr field in the letDecl Note that, for simplicity, each instance gets its own definition of each others' toTypeExpr fields. These are very simple fields, so avoiding the duplication is not worth it.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command

Makes a toExpr function for the given inductive type. The implementation of each toExpr function for a (mutual) inductive type is given as top-level private definitions. These are assembled into ToExpr instances in mkInstanceCmds. For mutual/nested inductive types, then each of the types' ToExpr instances are provided as local instances, to wire together the recursion (necessitating these auxiliary definitions being partial).

Equations

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

def Lean.Elab.Deriving.ToExpr.mkAuxFunctions (ctx : Context) : TermElabM Syntax

Creates all the auxiliary functions (using mkAuxFunction) for the (mutual) inductive type(s). Wraps the resulting definition commands in mutual ... end.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkInstanceCmds (ctx : Context) (typeNames : Array Name) : TermElabM (Array Command)

Assuming all of the auxiliary definitions exist, creates all the instance commands for the ToExpr instances for the (mutual) inductive type(s). This is a modified copy of Lean.Elab.Deriving.mkInstanceCmds to account for ToLevel instances.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax)

Returns all the commands necessary to construct the ToExpr instances.

Equations

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

def Lean.Elab.Deriving.ToExpr.mkToExprInstanceHandler (declNames : Array Name) : Command.CommandElabM Bool

The main entry point to the ToExpr deriving handler.

Equations

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