10.4. 派生实例🔗

Lean 可以自动生成许多类的实例，该过程称为 derivinginstances。实例派生可以在定义类型时调用，也可以作为独立命令调用。

syntaxInstance Deriving (Optional)

作为创建新归纳类型的命令的一部分，Lean.Parser.Command.declaration : commandderiving 子句指定应为其生成实例的以逗号分隔的类名列表：

optDeriving ::=
    (deriving derivingClass,*)?

syntaxStand-Alone Deriving of Instances

独立的 Lean.Parser.Command.deriving : commandderiving 命令指定多个类名称和主题名称。每个指定的类别都是针对每个指定的科目派生的。

command ::= ...
    | deriving instance derivingClass,* for term,*

Deriving Multiple Classes

指定多个类来派生多种类型后，如以下代码所示：

structure A where
structure B where

deriving instance BEq, Repr for A, B

所有类型都存在所有实例，因此所有四个 Lean.Parser.Command.synth : command#synth 命令都会成功：

instBEqA#synth BEq A
instBEqB#synth BEq B
instReprA#synth Repr A
instReprB#synth Repr B

Live ↪

10.4.1. 派生处理程序🔗

实例派生使用 deriving handlers 表，该表将类型类名称映射到为其派生实例的元程序。可以使用 registerDerivingHandler 将派生处理程序添加到表中，这应该在 Lean.Parser.Command.initialize : commandinitialize 块中调用。每个派生处理程序的类型应为 Array Name → CommandElabM Bool。当用户请求派生类的实例时，一次调用一个其注册的处理程序。它们提供了要为其派生实例的共同块中的所有名称，并且应该正确派生实例并返回 true，或者没有效果并返回 false。当处理程序返回 true 时，不会再调用其他处理程序。

Lean 包括以下类的派生处理程序：

BEq
DecidableEq
Hashable
Inhabited
LawfulBEq
Nonempty
Ord
ReflBEq
Repr
SizeOf
TypeName

def

Lean.Elab.registerDerivingHandler (className : Name)
  (handler : DerivingHandler) : IO Unit
Lean.Elab.registerDerivingHandler
  (className : Name)
  (handler : DerivingHandler) : IO Unit

Registers a deriving handler for a class. This function should be called in an initialize block.

A DerivingHandler is called on the fully qualified names of all types it is running for. For example, deriving instance Foo for Bar, Baz invokes fooHandler #[`Bar, `Baz].

Deriving Handlers

IsEnum 类的实例通过在类型和适当大小的 Fin 之间提供双射来证明该类型是有限枚举：

class IsEnum (α : Type) where
  size : Nat
  toIdx : α → Fin size
  fromIdx : Fin size → α
  to_from_id : ∀ (i : Fin size), toIdx (fromIdx i) = i
  from_to_id : ∀ (x : α), fromIdx (toIdx x) = x

对于归纳类型来说，这些枚举是简单的枚举，没有构造函数需要任何参数，所以此类的实例非常重复。 Bool 的实例是典型的：

instance : IsEnum Bool where
  size := 2
  toIdx
    | false => 0
    | true => 1
  fromIdx
    | 0 => false
    | 1 => true
  to_from_id
    | 0 => rfl
    | 1 => rfl
  from_to_id
    | false => rfl
    | true => rfl

派生处理程序以编程方式构造每个模式情况，类似于 IsEnum Bool 实现：

open Lean Elab Parser Term Command

def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do
  if h : declNames.size = 1 then
    let env ← getEnv
    if let some (.inductInfo ind) := env.find? declNames[0] then
      let mut tos : Array (TSyntax ``matchAlt) := #[]
      let mut froms := #[]
      let mut to_froms := #[]
      let mut from_tos := #[]
      let mut i := 0

      for ctorName in ind.ctors do
        let c := mkIdent ctorName
        let n := Syntax.mkNumLit (toString i)

        tos      := tos.push      (← `(matchAltExpr| | $c => $n))
        from_tos := from_tos.push (← `(matchAltExpr| | $c => rfl))
        froms    := froms.push    (← `(matchAltExpr| | $n => $c))
        to_froms := to_froms.push (← `(matchAltExpr| | $n => rfl))

        i := i + 1

      let cmd ← `(instance : IsEnum $(mkIdent declNames[0]) where
                    size := $(quote ind.ctors.length)
                    toIdx $tos:matchAlt*
                    fromIdx $froms:matchAlt*
                    to_from_id $to_froms:matchAlt*
                    from_to_id $from_tos:matchAlt*)
      elabCommand cmd

      return true
  return false

initialize
  registerDerivingHandler ``IsEnum deriveIsEnum

Live ↪