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.
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. Deprecated.
Instances For
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
Instances For
Data about a type created with the structure
command.
- structName : Name
The name of the structure.
The direct fields of a structure, sorted by position in the structure. For example, the
s.3
notation refers tofieldNames[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.
Instances For
Equations
Instances For
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.
Instances For
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
Instances For
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
Instances For
Gets the StructureInfo
if structName
has been declared as a structure to the elaborator.
Equations
Instances For
Gets the StructureInfo
for structName
, which is assumed to have been declared as a structure to the elaborator.
Panics on failure.
Equations
Instances For
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
Instances For
Gets the direct field names for the given structure, including subobject fields.
Equations
Instances For
If fieldName
is a subobject (that it, if it is an embedded parent structure),
then returns the name of that parent structure.
Equations
Instances For
Gets information for all the parents that appear in the extends
clause.
Equations
Instances For
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
Instances For
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.
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
Instances For
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
Instances For
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
Instances For
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
Instances For
Equations
Instances For
Equations
Instances For
Gets the name of the auxiliary definition that would have the default value for the structure field if it exists.
Equations
Instances For
Gets the name of the auxiliary definition that would have the inherited default value for the structure field if it exists.
Equations
Instances For
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
Instances For
Returns the name of the auxiliary definition for a default value for the field, even if inherited, if any such definition exists.
Equations
Instances For
Gets the name of the auxiliary definition that would have the autoParam definition for a field.
Equations
Instances For
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
Instances For
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
Instances For
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
Instances For
Returns the constructor of the structure named constName
if it is a non-recursive single-constructor inductive type with no indices.
Equations
Instances For
Returns the number of fields for a structure-like type
Equations
Instances For
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.
Equations
We use an environment extension to cache resolution orders. These are not expensive to compute, but worth caching, and we save olean storage space.
- conflicts : Array StructureResolutionOrderConflict
Instances For
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.
Returns the transitive closure of all parent structures of the structure.
This is the same as Lean.getStructureResolutionOrder
but without including structName
.