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 : Name

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

• projFn : Name

  The projection function associated to the field.

• subobject? : Option Name

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

• binderInfo : BinderInfo

  The binder info for the field from the structure definition.

• autoParam? : Option Expr

  Deprecated.

instance Lean.instInhabitedStructureFieldInfo : Inhabited StructureFieldInfo

Equations

• Lean.instInhabitedStructureFieldInfo = { default := { fieldName := default, projFn := default, subobject? := default, binderInfo := default, autoParam? := default } }

instance Lean.instReprStructureFieldInfo : Repr StructureFieldInfo

Equations

• Lean.instReprStructureFieldInfo = { reprPrec := Lean.reprStructureFieldInfo✝ }

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

Equations

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

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 : 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 : 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 StructureParentInfo

Equations

• Lean.instInhabitedStructureParentInfo = { default := { structName := default, subobject := default, projFn := default } }

structure Lean.StructureInfo : Type

Data about a type created with the structure command.

• structName : Name

  The name of the structure.

• fieldNames : Array 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 StructureFieldInfo

  Information about the structure fields, sorted by fieldName.

• parentInfo : Array StructureParentInfo

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

instance Lean.instInhabitedStructureInfo : Inhabited StructureInfo

Equations

• Lean.instInhabitedStructureInfo = { default := { structName := default, fieldNames := default, fieldInfo := default, parentInfo := default } }

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

Equations

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

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

Equations

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

instance Lean.instInhabitedStructureState : Inhabited Lean.StructureState✝

Equations

• Lean.instInhabitedStructureState = { default := { map := default } }

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

structure Lean.StructureDescr : Type

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

• structName : Name

  The name of the structure.

• fields : Array StructureFieldInfo

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

instance Lean.instInhabitedStructureDescr : Inhabited StructureDescr

Equations

• Lean.instInhabitedStructureDescr = { default := { structName := default, fields := default } }

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

Declares 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.

Equations

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

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

Sets 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 : Environment) (structName : Name) : Option 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 : Environment) (structName : Name) : StructureInfo

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

Equations

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

def Lean.getStructureCtor (env : Environment) (constName : Name) : 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 : Environment) (structName : Name) : Array Name

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

Equations

• Lean.getStructureFields env structName = (Lean.getStructureInfo env structName).fieldNames

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

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

Equations

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

def Lean.isSubobjectField? (env : Environment) (structName fieldName : Name) : Option 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 : Environment) (structName : Name) : Array StructureParentInfo

Gets 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 : Environment) (structName : Name) : Array Name

Returns 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 : Environment) (structName fieldName : Name) : Option Name

Returns 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.findParentProjStruct? (env : Environment) (structName projName : Name) : Option Name

Given a structure structName and a parent projection name projName (e.g. toParentStructName), returns the corresponding parent structure name. The parent projection name is a single-component name.

Note: this relies on the fact that projection names are checked to be consistent across all parents.

Equations

• Lean.findParentProjStruct? env structName projName = StateT.run' (Lean.findParentProjStruct?.go env projName structName) ∅

partial def Lean.findParentProjStruct?.go (env : Environment) (projName structName : Name) : StateM NameSet (Option Name)

def Lean.mkFlatCtorOfStructCtorName (structCtorName : Name) : Name

Gets the name for a structure constructor where the fields have been fully flattened. This constructor simulates a flat representation for structures, and it is used by structure instance notation when elaborating structure fields and for organizing the fields into subobjects.

The body of the flat constructor has the following properties (recursively):

• the fields come in order
• for subobject fields, the value is the unfolded flat constructor for that field
• for standard fields, the value is one of the flat constructor parameters

Equations

• Lean.mkFlatCtorOfStructCtorName structCtorName = structCtorName ++ `_flat_ctor

def Lean.getStructureFieldsFlattened (env : Environment) (structName : Name) (includeSubobjectFields : Bool := true) : Array 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.

Equations

• Lean.getStructureFieldsFlattened env structName includeSubobjectFields = Lean.getStructureFieldsFlattenedAux✝ env structName #[] includeSubobjectFields

def Lean.isStructure (env : Environment) (constName : 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?.

Equations

• Lean.isStructure env constName = (Lean.getStructureInfo? env constName).isSome

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

Equations

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

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

Equations

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

def Lean.mkDefaultFnOfProjFn (projFn : Name) : Name

Gets the name of the auxiliary definition that would have the default value for the structure field if it exists.

Equations

• Lean.mkDefaultFnOfProjFn projFn = projFn ++ `_default

def Lean.mkInheritedDefaultFnOfProjFn (projFn : Name) : Name

Gets the name of the auxiliary definition that would have the inherited default value for the structure field if it exists.

Equations

• Lean.mkInheritedDefaultFnOfProjFn projFn = projFn ++ `_inherited_default

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

Returns the name of the auxiliary definition that defines a default value for the field, if any such definition exists. This is not an inherited default. We need to store provided defaults so that it is possible to resolve defaults according to the resolution order.

Equations

• Lean.getDefaultFnForField? env structName fieldName = Lean.getFnForFieldUsing?✝ Lean.mkDefaultFnOfProjFn env structName fieldName

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

Returns the name of the auxiliary definition for a default value for the field, even if inherited, if any such definition exists.

Equations

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

def Lean.mkAutoParamFnOfProjFn (projFn : Name) : Name

Gets the name of the auxiliary definition that would have the autoParam definition for a field.

Equations

• Lean.mkAutoParamFnOfProjFn projFn = projFn ++ `_autoParam

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

Returns the name of the auxiliary definition that defines the autoParam for the field, if any such definition exists. This is not the inherited autoParam, but the one that is defined or overridden by this structure. The effective autoParams are collected in the flat constructor.

Equations

• Lean.getAutoParamFnForField? env structName fieldName = Lean.getFnForFieldUsing?✝ Lean.mkAutoParamFnOfProjFn env structName fieldName

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

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

Equations

• Lean.getPathToBaseStructure? env baseStructName structName = StateT.run' (Lean.getPathToBaseStructure?.go env baseStructName structName []).run ∅

partial def Lean.getPathToBaseStructure?.go (env : Environment) (baseStructName structName : Name) (path : List Name) : OptionT (StateM NameSet) (List Name)

def Lean.isStructureLike (env : Environment) (constName : 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 : Environment) (constName : Name) : Option 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 : Environment) (constName : Name) : Nat

Returns the 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 : PHashMap Name (Array Name)

instance Lean.instInhabitedStructureResolutionState : Inhabited StructureResolutionState

Equations

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

opaque Lean.structureResolutionExt : EnvExtension 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 : Name
• conflicts : Array (Bool × Name)

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

instance Lean.instInhabitedStructureResolutionOrderConflict : Inhabited StructureResolutionOrderConflict

Equations

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

structure Lean.StructureResolutionOrderResult : Type

• resolutionOrder : Array Name
• conflicts : Array StructureResolutionOrderConflict

instance Lean.instInhabitedStructureResolutionOrderResult : Inhabited StructureResolutionOrderResult

Equations

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

partial def Lean.computeStructureResolutionOrder {m : Type → Type} [Monad m] [MonadEnv m] (structName : Name) (relaxed : Bool) : m 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.

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

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

Equations

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

def Lean.getStructureResolutionOrder {m : Type → Type} [Monad m] [MonadEnv m] (structName : Name) : m (Array 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] [MonadEnv m] (structName : Name) : m (Array Name)

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

Equations

• Lean.getAllParentStructures structName = (fun (x : Array Lean.Name) => x.erase structName) <$> Lean.getStructureResolutionOrder structName