Documentation

Lean.Elab.Deriving.ToExpr

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.

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

Equations
    Instances For

      Fixes the output of mkInductiveApp to explicitly reference universe levels.

      Equations
        Instances For

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

          Equations
            Instances For
              def Lean.Elab.Deriving.ToExpr.mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) (levelInsts : Array 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
                Instances For
                  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
                    Instances For
                      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
                        Instances For

                          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
                            Instances For

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

                              Equations
                                Instances For

                                  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
                                    Instances For

                                      Returns all the commands necessary to construct the ToExpr instances.

                                      Equations
                                        Instances For

                                          The main entry point to the ToExpr deriving handler.

                                          Equations
                                            Instances For