Structure instance elaborator

A structure instance is notation to construct a term of a structure. Examples: { x := 2, y.z := true }, { s with cache := c' }, and { s with values[2] := v }. Structure instances are the preferred way to invoke a structure's constructor, since they hide Lean implementation details such as whether parents are represented as subobjects, and also they do correct processing of default values, which are complicated due to the fact that structures can override default values of their parents, and furthermore overridden default values can use fields that come after in the order the fields appear in the constructor.

This module elaborates structure instance notation. Note that the where syntax to define structures (Lean.Parser.Command.whereStructInst) macro expands into the structure instance notation elaborated by this module.

Recall that structure instances are (after removing parsing and pretty printing hints):

def structInst := leading_parser
  "{ " >> optional (sepBy1 termParser ", " >> " with ")
    >> structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
    >> optEllipsis
    >> optional (" : " >> termParser) >> " }"

def structInstField := leading_parser
  structInstLVal >> optional (many structInstFieldBinder >> optType >> structInstFieldDecl)

@[builtin_structInstFieldDecl_parser]
def structInstFieldDef := leading_parser
  " := " >> termParser

@[builtin_structInstFieldDecl_parser]
def structInstFieldEqns := leading_parser
  matchAlts

def structInstWhereBody := leading_parser
  structInstFields (sepByIndent structInstField "; " (allowTrailingSep := true))

@[builtin_structInstFieldDecl_parser]
def structInstFieldWhere := leading_parser
  "where" >> structInstWhereBody

def Lean.Elab.Term.StructInst.expandStructInstExpectedType : Macro

Transforms structure instances such as { x := 0 : Foo } into ({ x := 0 } : Foo). Structure instance notation makes use of the expected type.

Equations

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

def Lean.Elab.Term.StructInst.expandStructInstFields : Macro

Expands fields.

• Abbreviations. Example: { x } expands to { x := x }.
• Equations. Example: { f | 0 => 0 | n + 1 => n } expands to { f := fun x => match x with | 0 => 0 | n + 1 => n }.
• Binders and types. Example: { f n : Nat := n + 1 } expands to { f := fun n => (n + 1 : Nat) }.

Equations

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

structure Lean.Elab.Term.StructInst.ExplicitSourceView : Type

An explicit source is one of the structures sᵢ that appear in { s₁, …, sₙ with … }.

• stx : Syntax

  The syntax of the explicit source.

• fvar : Expr

  The local variable for this source.

• structName : Name

  The name of the structure for the type of the explicit source.

def Lean.Elab.Term.StructInst.instInhabitedExplicitSourceView.default : ExplicitSourceView

Equations

• Lean.Elab.Term.StructInst.instInhabitedExplicitSourceView.default = { stx := default, fvar := default, structName := default }

instance Lean.Elab.Term.StructInst.instInhabitedExplicitSourceView : Inhabited ExplicitSourceView

Equations

• Lean.Elab.Term.StructInst.instInhabitedExplicitSourceView = { default := Lean.Elab.Term.StructInst.instInhabitedExplicitSourceView.default }

structure Lean.Elab.Term.StructInst.SourcesView : Type

A view of the sources of fields for the structure instance notation.

• explicit : Array ExplicitSourceView

  Explicit sources (i.e., one of the structures sᵢ that appear in { s₁, …, sₙ with … }).

• implicit : Option Syntax

  The syntax for a trailing ... This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications.

instance Lean.Elab.Term.StructInst.instInhabitedSourcesView : Inhabited SourcesView

Equations

• Lean.Elab.Term.StructInst.instInhabitedSourcesView = { default := Lean.Elab.Term.StructInst.instInhabitedSourcesView.default }

def Lean.Elab.Term.StructInst.instInhabitedSourcesView.default : SourcesView

Equations

• Lean.Elab.Term.StructInst.instInhabitedSourcesView.default = { explicit := default, implicit := default }

inductive Lean.Elab.Term.StructInst.FieldLHS : Type

A component of a left-hand side for a field appearing in structure instance syntax.

• fieldName (ref : Syntax) (name : Name) : FieldLHS

  A name component for a field left-hand side. For example, x and y in { x.y := v }.

• parentFieldName (ref : Syntax) (structName name : Name) : FieldLHS

  (Can't be written by users.) A field setting an entire parent. The structName is the name of the parent structure, and name is the projection field name. Always appears as the only LHS component.

• fieldIndex (ref : Syntax) (idx : Nat) : FieldLHS

  A numeric index component for a field left-hand side. For example 3 in { x.3 := v }.

• modifyOp (ref index : Syntax) : FieldLHS

  An array indexing component for a field left-hand side. For example [3] in { arr[3] := v }.

def Lean.Elab.Term.StructInst.instInhabitedFieldLHS.default : FieldLHS

Equations

• Lean.Elab.Term.StructInst.instInhabitedFieldLHS.default = Lean.Elab.Term.StructInst.FieldLHS.fieldName default default

instance Lean.Elab.Term.StructInst.instInhabitedFieldLHS : Inhabited FieldLHS

Equations

• Lean.Elab.Term.StructInst.instInhabitedFieldLHS = { default := Lean.Elab.Term.StructInst.instInhabitedFieldLHS.default }

instance Lean.Elab.Term.StructInst.instToFormatFieldLHS : ToFormat FieldLHS

Equations

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

structure Lean.Elab.Term.StructInst.FieldView : Type

Field StructInstView is a representation of a field in the structure instance.

• ref : Syntax

  The whole field syntax.

• lhs : List FieldLHS

  The LHS components. This is nonempty.

• val : Term

  The value of the field.

def Lean.Elab.Term.StructInst.instInhabitedFieldView.default : FieldView

Equations

• Lean.Elab.Term.StructInst.instInhabitedFieldView.default = { ref := default, lhs := default, val := default }

instance Lean.Elab.Term.StructInst.instInhabitedFieldView : Inhabited FieldView

Equations

• Lean.Elab.Term.StructInst.instInhabitedFieldView = { default := Lean.Elab.Term.StructInst.instInhabitedFieldView.default }

structure Lean.Elab.Term.StructInst.StructInstView : Type

The view for structure instance notation.

• ref : Syntax

  The syntax for the whole structure instance.

• fields : Array FieldView

  The fields of the structure instance.

• sources : SourcesView

  The additional sources for fields for the structure instance.

instance Lean.Elab.Term.StructInst.instInhabitedStructInstView : Inhabited StructInstView

Equations

• Lean.Elab.Term.StructInst.instInhabitedStructInstView = { default := Lean.Elab.Term.StructInst.instInhabitedStructInstView.default }

def Lean.Elab.Term.StructInst.instInhabitedStructInstView.default : StructInstView

Equations

• Lean.Elab.Term.StructInst.instInhabitedStructInstView.default = { ref := default, fields := default, sources := default }

instance Lean.Elab.Term.StructInst.instToFormatFieldView : ToFormat FieldView

Equations

• Lean.Elab.Term.StructInst.instToFormatFieldView = { format := Lean.Elab.Term.StructInst.instToFormatFieldView._private_1 }

instance Lean.Elab.Term.StructInst.instToFormatStructInstView : ToFormat StructInstView

Equations

• Lean.Elab.Term.StructInst.instToFormatStructInstView = { format := Lean.Elab.Term.StructInst.instToFormatStructInstView._private_1 }

def Lean.Elab.Term.StructInst.elabStructInst : TermElab

Equations

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