10.4. 派生实例🔗

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

语法实例派生（可选）

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

optDeriving ::=
    (deriving derivingClass,*)?

语法独立的派生实例

独立的 Lean.Parser.Command.deriving : commandderiving 命令指定了几个类名和目标名。每个指定的类都会为每个指定的目标进行派生。

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

派生多个类

在为多个类型指定派生多个类后，如下面的代码所示：

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

在线查看 ↪

10.4.1. 派生处理器🔗

实例派生使用一张将类型类名称映射到元程序的派生处理器表；这些元程序为相应类型类派生实例。可以使用 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

定义

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

为一个类注册派生处理器。此函数应当在 initialize 块中调用。

DerivingHandler 接收它所处理的全部类型的完全限定名。例如， deriving instance Foo for Bar, Baz 会调用 fooHandler #[`Bar, `Baz]。

派生处理器

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

在线查看 ↪