Computed fields

Inductives can have computed fields which are recursive functions whose value is stored in the constructors, and can be accessed in constant time.

inductive Exp
  | hole
  | app (x y : Exp)
with
  f : Exp → Nat
    | .hole => 42
    | .app x y => f x + f y

-- `Exp.f x` runs in constant time, even if `x` is a dag-like value

This file implements the computed fields feature by simulating it via implemented_by. The main function is setComputedFields.

opaque Lean.Elab.ComputedFields.computedFieldAttr : TagAttribute

Marks a function as a computed field of an inductive.

Computed fields are specified in the with-block of an inductive type declaration. They can be used to allow certain values to be computed only once at the time of construction and then later be accessed immediately.

Example:

inductive NatList where
  | nil
  | cons : Nat → NatList → NatList
with
  @[computed_field] sum : NatList → Nat
  | .nil => 0
  | .cons x l => x + l.sum
  @[computed_field] length : NatList → Nat
  | .nil => 0
  | .cons _ l => l.length + 1

def Lean.Elab.ComputedFields.mkUnsafeCastTo (expectedType e : Expr) : MetaM Expr

def Lean.Elab.ComputedFields.isScalarField (ctor : Name) : CoreM Bool

structure Lean.Elab.ComputedFields.Contextextends Lean.InductiveVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• numParams : Nat
• numIndices : Nat
• all : List Name
• ctors : List Name
• numNested : Nat
• isRec : Bool
• isUnsafe : Bool
• isReflexive : Bool
• lparams : List Level
• params : Array Expr
• compFields : Array Name
• compFieldVars : Array Expr
• indices : Array Expr
• val : Expr

@[reducible, inline]

abbrev Lean.Elab.ComputedFields.M (α : Type) : Type

def Lean.Elab.ComputedFields.getComputedFieldValue (computedField : Name) (ctorTerm : Expr) : MetaM Expr

def Lean.Elab.ComputedFields.validateComputedFields : M Unit

def Lean.Elab.ComputedFields.mkImplType : M Unit

def Lean.Elab.ComputedFields.overrideCasesOn : M Unit

def Lean.Elab.ComputedFields.overrideConstructors : M Unit

def Lean.Elab.ComputedFields.overrideComputedFields : M Unit

def Lean.Elab.ComputedFields.mkComputedFieldOverrides (declName : Name) (compFields : Array Name) : MetaM Unit

def Lean.Elab.ComputedFields.setComputedFields (computedFields : Array (Name × Array Name)) : MetaM Unit

Sets the computed fields for a block of mutual inductives, adding the implementation via implemented_by.

The computedFields argument contains a pair for every inductive in the mutual block, consisting of the name of the inductive and the names of the associated computed fields.