structure Lean.StructureFieldInfo : Type

Data for a structure field. These are direct fields of a structure, including "subobject" fields for the embedded parents. The full collection of fields is the transitive closure of fields through the subobject fields.

• fieldName : Lean.Name

  The name of the field. This is a single-component name.

• projFn : Lean.Name

  The projection function associated to the field.

• subobject? : Option Lean.Name

  If this field is for a subobject (i.e., an embedded parent structure), contains the name of the parent structure.

• binderInfo : Lean.BinderInfo

  The binder info for the field from the structure definition.

• autoParam? : Option Lean.Expr

  If set, the field is an autoparam (a field declared using fld := by ... syntax). The expression evaluates to a tactic Syntax object. Generally this is an Expr.const expression.

instance Lean.instInhabitedStructureFieldInfo : Inhabited Lean.StructureFieldInfo

instance Lean.instReprStructureFieldInfo : Repr Lean.StructureFieldInfo

def Lean.StructureFieldInfo.lt (i₁ i₂ : Lean.StructureFieldInfo) : Bool

structure Lean.StructureParentInfo : Type

Data for a direct parent of a structure. Some structure parents are represented as subobjects (embedded structures), and for these the parent projection is a true projection. If a structure parent shares a field with a previous parent, it will become an implicit parent, and all the fields of the structure parent that do not occur in earlier parents are fields of the new structure

• structName : Lean.Name

  The name of the parent structure.

• subobject : Bool

  Whether this parent structure is represented as a subobject. If so, then there is a fieldInfo entry with the same projFn.

• projFn : Lean.Name

  The projection function associated to the field. For subobjects, this is the same as the projFn in its fieldInfo entry.

instance Lean.instInhabitedStructureParentInfo : Inhabited Lean.StructureParentInfo

structure Lean.StructureInfo : Type

Data about a type created with the structure command.

• structName : Lean.Name

  The name of the structure.

• fieldNames : Array Lean.Name

  The direct fields of a structure, sorted by position in the structure. For example, the s.3 notation refers to fieldNames[3 - 1].

• fieldInfo : Array Lean.StructureFieldInfo

  Information about the structure fields, sorted by fieldName.

• parentInfo : Array Lean.StructureParentInfo

  Information about structure parents. These are in the order they appear in the extends clause.

instance Lean.instInhabitedStructureInfo : Inhabited Lean.StructureInfo

def Lean.StructureInfo.lt (i₁ i₂ : Lean.StructureInfo) : Bool

Equations

• i₁.lt i₂ = i₁.structName.quickLt i₂.structName

def Lean.StructureInfo.getProjFn? (info : Lean.StructureInfo) (i : Nat) : Option Lean.Name

Equations

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

instance Lean.instInhabitedStructureState : Inhabited Lean.StructureState✝

opaque Lean.structureExt : Lean.PersistentEnvExtension Lean.StructureInfo Lean.StructureInfo (Unit × Lean.StructureState✝)

structure Lean.StructureDescr : Type

A descriptor for a structure, for constructing a StructureInfo via Lean.registerStructure.

• structName : Lean.Name

  The name of the structure.

• fields : Array Lean.StructureFieldInfo

  The fields should be in the order that they appear in the structure's constructor.

instance Lean.instInhabitedStructureDescr : Inhabited Lean.StructureDescr

def Lean.registerStructure (env : Lean.Environment) (e : Lean.StructureDescr) : Lean.Environment

Declare a new structure to the elaborator. Every structure created by structure or class has such an entry. This should be followed up with setStructureParents and setStructureResolutionOrder.

def Lean.setStructureParents {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (structName : Lean.Name) (parentInfo : Array Lean.StructureParentInfo) : m Unit

Set parent projection info for a structure defined in the current module. Throws an error if the structure has not already been registered with Lean.registerStructure.

Equations

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

def Lean.getStructureInfo? (env : Lean.Environment) (structName : Lean.Name) : Option Lean.StructureInfo

Gets the StructureInfo if structName has been declared as a structure to the elaborator.

Equations

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

def Lean.getStructureInfo (env : Lean.Environment) (structName : Lean.Name) : Lean.StructureInfo

Gets the StructureInfo for structName, which is assumed to have been declared as a structure to the elaborator. Panics on failure.

def Lean.getStructureCtor (env : Lean.Environment) (constName : Lean.Name) : Lean.ConstructorVal

Gets the constructor of an inductive type that has exactly one constructor. This is meant to be used with types that have had been registered as a structure by registerStructure, but this is not checked.

Warning: these do not need to be "structure-likes". A structure-like is non-recursive, and structure-likes have special kernel support.

Equations

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

def Lean.getStructureFields (env : Lean.Environment) (structName : Lean.Name) : Array Lean.Name

Gets the direct field names for the given structure, including subobject fields.

def Lean.getFieldInfo? (env : Lean.Environment) (structName fieldName : Lean.Name) : Option Lean.StructureFieldInfo

Get the StructureFieldInfo for the given direct field of the structure.

def Lean.isSubobjectField? (env : Lean.Environment) (structName fieldName : Lean.Name) : Option Lean.Name

If fieldName is a subobject (that it, if it is an embedded parent structure), then returns the name of that parent structure.

Equations

• Lean.isSubobjectField? env structName fieldName = match Lean.getFieldInfo? env structName fieldName with | some fieldInfo => fieldInfo.subobject? | x => none

def Lean.getStructureParentInfo (env : Lean.Environment) (structName : Lean.Name) : Array Lean.StructureParentInfo

Get information for all the parents that appear in the extends clause.

Equations

• Lean.getStructureParentInfo env structName = (Lean.getStructureInfo env structName).parentInfo

def Lean.getStructureSubobjects (env : Lean.Environment) (structName : Lean.Name) : Array Lean.Name

Return the parent structures that are embedded in the structure. This is the array of all results from Lean.isSubobjectField? in order.

Note: this is not a subset of the parents from getStructureParentInfo. If a direct parent cannot itself be represented as a subobject, sometimes one of its parents (or one of their parents, etc.) can.

Equations

• Lean.getStructureSubobjects env structName = Array.filterMap (Lean.isSubobjectField? env structName) (Lean.getStructureFields env structName)

partial def Lean.findField? (env : Lean.Environment) (structName fieldName : Lean.Name) : Option Lean.Name

Return the name of the structure that contains the field relative to structure structName. If structName contains the field itself, returns that, and otherwise recursively looks into parents that are subobjects.

def Lean.getStructureFieldsFlattened (env : Lean.Environment) (structName : Lean.Name) (includeSubobjectFields : Bool := true) : Array Lean.Name

Returns the full set of field names for the given structure, "flattening" all the parent structures that are subobject fields. If includeSubobjectFields is true, then subobject toParent projections are included, and otherwise they are omitted.

For example, given Bar such that

structure Foo where a : Nat
structure Bar extends Foo where b : Nat

this returns #[`toFoo, `a, `b], or #[`a, `b] when includeSubobjectFields := false.

def Lean.isStructure (env : Lean.Environment) (constName : Lean.Name) : Bool

Returns true if constName is the name of an inductive datatype created using the structure or class commands.

These are inductive types for which structure information has been registered with registerStructure. See also Lean.getStructureInfo?.

def Lean.getProjFnForField? (env : Lean.Environment) (structName fieldName : Lean.Name) : Option Lean.Name

def Lean.getProjFnInfoForField? (env : Lean.Environment) (structName fieldName : Lean.Name) : Option (Lean.Name × Lean.ProjectionFunctionInfo)

Equations

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

def Lean.mkDefaultFnOfProjFn (projFn : Lean.Name) : Lean.Name

Get the name of the auxiliary definition that would have the default value for the structure field.

Equations

• Lean.mkDefaultFnOfProjFn projFn = projFn ++ `_default

def Lean.getDefaultFnForField? (env : Lean.Environment) (structName fieldName : Lean.Name) : Option Lean.Name

partial def Lean.getPathToBaseStructureAux (env : Lean.Environment) (baseStructName structName : Lean.Name) (path : List Lean.Name) : Option (List Lean.Name)

def Lean.getPathToBaseStructure? (env : Lean.Environment) (baseStructName structName : Lean.Name) : Option (List Lean.Name)

If baseStructName is an ancestor structure for structName, then return a sequence of projection functions to go from structName to baseStructName. Returns [] if baseStructName == structName.

Equations

• Lean.getPathToBaseStructure? env baseStructName structName = Lean.getPathToBaseStructureAux env baseStructName structName []

def Lean.isStructureLike (env : Lean.Environment) (constName : Lean.Name) : Bool

Returns true iff constName is a non-recursive inductive datatype that has only one constructor and no indices.

Such types have special kernel support. This must be in sync with is_structure_like.

Equations

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

def Lean.getStructureLikeCtor? (env : Lean.Environment) (constName : Lean.Name) : Option Lean.ConstructorVal

Returns the constructor of the structure named constName if it is a non-recursive single-constructor inductive type with no indices.

Equations

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

def Lean.getStructureLikeNumFields (env : Lean.Environment) (constName : Lean.Name) : Nat

Return number of fields for a structure-like type

Equations

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

Resolution orders

This section is for computations to determine which namespaces to visit when resolving field notation. While the set of namespaces is clear (after a structure's namespace, it is the namespaces for all parents), the question is the order to visit them in.

We use the C3 superclass linearization algorithm from Barrett et al., "A Monotonic Superclass Linearization for Dylan", OOPSLA 1996. For reference, the C3 linearization is known as the "method resolution order" (MRO) in Python.

The basic idea is that we want to find a resolution order with the following property: For each structure S that appears in the resolution order, if its direct parents are P₁ .. Pₙ, then S P₁ ... Pₙ forms a subsequence of the resolution order.

This has a stability property where if S extends S', then the resolution order of S contains the resolution order of S' as a subsequence. It also has the key property that if P and P' are parents of S, then we visit P and P' before we visit the shared parents of P and P'.

Finding such a resolution order might not be possible. Still, we can enable a relaxation of the algorithm by ignoring one or more parent resolution orders, starting from the end.

In Hivert and Thiéry "Controlling the C3 super class linearization algorithm for large hierarchies of classes" https://arxiv.org/pdf/2401.12740 the authors discuss how in SageMath, which has thousands of classes, C3 can be difficult to control, since maintaining correct direct parent orders is a burden. They give suggestions that have worked for the SageMath project. We may consider introducing an environment extension with ordering hints to help guide the algorithm if we see similar difficulties.

structure Lean.StructureResolutionState : Type

• resolutions : Lean.PHashMap Lean.Name (Array Lean.Name)

instance Lean.instInhabitedStructureResolutionState : Inhabited Lean.StructureResolutionState

Equations

• Lean.instInhabitedStructureResolutionState = { default := { resolutions := default } }

opaque Lean.structureResolutionExt : Lean.EnvExtension Lean.StructureResolutionState

We use an environment extension to cache resolution orders. These are not expensive to compute, but worth caching, and we save olean storage space.

structure Lean.StructureResolutionOrderConflict : Type

"The badParent must come after the conflicts.

• isDirectParent : Bool
• badParent : Lean.Name
• conflicts : Array (Bool × Lean.Name)

  Conflicts that must come before badParent. The flag is whether it is a direct parent.

instance Lean.instInhabitedStructureResolutionOrderConflict : Inhabited Lean.StructureResolutionOrderConflict

Equations

• Lean.instInhabitedStructureResolutionOrderConflict = { default := { isDirectParent := default, badParent := default, conflicts := default } }

structure Lean.StructureResolutionOrderResult : Type

• resolutionOrder : Array Lean.Name
• conflicts : Array Lean.StructureResolutionOrderConflict

instance Lean.instInhabitedStructureResolutionOrderResult : Inhabited Lean.StructureResolutionOrderResult

Equations

• Lean.instInhabitedStructureResolutionOrderResult = { default := { resolutionOrder := default, conflicts := default } }

partial def Lean.computeStructureResolutionOrder {m : Type → Type} [Monad m] [Lean.MonadEnv m] (structName : Lean.Name) (relaxed : Bool) : m Lean.StructureResolutionOrderResult

Computes and caches the C3 linearization. Assumes parents have already been set with setStructureParents. If relaxed is false, then if the linearization cannot be computed, conflicts are recorded in the return value.

def Lean.computeStructureResolutionOrder.selectParent {m : Type → Type} [Monad m] (resOrders : Array (Array Lean.Name)) : m (Bool × Lean.Name)

def Lean.getStructureResolutionOrder {m : Type → Type} [Monad m] [Lean.MonadEnv m] (structName : Lean.Name) : m (Array Lean.Name)

Gets the resolution order for a structure.

Equations

• Lean.getStructureResolutionOrder structName = (fun (x : Lean.StructureResolutionOrderResult) => x.resolutionOrder) <$> Lean.computeStructureResolutionOrder structName true

def Lean.getAllParentStructures {m : Type → Type} [Monad m] [Lean.MonadEnv m] (structName : Lean.Name) : m (Array Lean.Name)

Returns the transitive closure of all parent structures of the structure. This is the same as Lean.getStructureResolutionOrder but without including structName.