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.

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 : Lean.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.mkStructInstField (lval : Lean.TSyntax `Lean.Parser.Term.structInstLVal) (binders : Lean.TSyntaxArray `Lean.Parser.Term.structInstFieldBinder) (type? : Option Lean.Term) (val : Lean.Term) : Lean.MacroM (Lean.TSyntax `Lean.Parser.Term.structInstField)

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

Expands fields.

• Abbrevations. 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 : Lean.Syntax

  The syntax of the explicit source.

• structName : Lean.Name

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

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

Equations

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

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

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

• explicit : Array Lean.Elab.Term.StructInst.ExplicitSourceView

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

• implicit : Option Lean.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 Lean.Elab.Term.StructInst.SourcesView

Equations

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

def Lean.Elab.Term.StructInst.SourcesView.isNone : Lean.Elab.Term.StructInst.SourcesView → Bool

Returns true if the structure instance has no sources (neither explicit sources nor a ..).

Equations

• x.isNone = match x with | { explicit := #[], implicit := none } => true | x => false

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

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

• fieldName: Lean.Syntax → Lean.Name → Lean.Elab.Term.StructInst.FieldLHS

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

• fieldIndex: Lean.Syntax → Nat → Lean.Elab.Term.StructInst.FieldLHS

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

• modifyOp: Lean.Syntax → Lean.Syntax → Lean.Elab.Term.StructInst.FieldLHS

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

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

Equations

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

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

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

FieldVal StructInstView is a representation of a field value in the structure instance.

• term: Lean.Syntax → Lean.Elab.Term.StructInst.FieldVal

  A term to use for the value of the field.

• nested: Lean.Elab.Term.StructInst.StructInstView → Lean.Elab.Term.StructInst.FieldVal

  A StructInstView to use for the value of a subobject field.

• default: Lean.Elab.Term.StructInst.FieldVal

  A field that was not provided and should be synthesized using default values.

instance Lean.Elab.Term.StructInst.instInhabitedField : Inhabited Lean.Elab.Term.StructInst.Field

Equations

• Lean.Elab.Term.StructInst.instInhabitedField = { default := { ref := default, lhs := default, val := default, expr? := default } }

instance Lean.Elab.Term.StructInst.instInhabitedFieldVal : Inhabited Lean.Elab.Term.StructInst.FieldVal

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

Equations

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

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

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

• ref : Lean.Syntax

  The whole field syntax.

• lhs : List Lean.Elab.Term.StructInst.FieldLHS

  The LHS decomposed into components.

• val : Lean.Elab.Term.StructInst.FieldVal

  The value of the field.

• expr? : Option Lean.Expr

  The elaborated field value, filled in at elabStruct. Missing fields use a metavariable for the elaborated value and are later solved for in DefaultFields.propagate.

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

The view for structure instance notation.

• ref : Lean.Syntax

  The syntax for the whole structure instance.

• structName : Lean.Name

  The name of the structure for the type of the structure instance.

• params : Array (Lean.Name × Lean.Expr)

  Used for default values, to propagate structure type parameters. It is initially empty, and then set at elabStruct.

• fields : List Lean.Elab.Term.StructInst.Field

  The fields of the structure instance.

• sources : Lean.Elab.Term.StructInst.SourcesView

  The additional sources for fields for the structure instance.

def Lean.Elab.Term.StructInst.Field.isSimple : Lean.Elab.Term.StructInst.Field → Bool

Returns if the field has a single component in its LHS.

partial def Lean.Elab.Term.StructInst.StructInstView.allDefault (s : Lean.Elab.Term.StructInst.StructInstView) : Bool

true iff all fields of the given structure are marked as default

def Lean.Elab.Term.StructInst.formatField (formatStruct : Lean.Elab.Term.StructInst.StructInstView → Lean.Format) (field : Lean.Elab.Term.StructInst.Field) : Lean.Format

Equations

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

partial def Lean.Elab.Term.StructInst.formatStruct : Lean.Elab.Term.StructInst.StructInstView → Lean.Format

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

Equations

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

instance Lean.Elab.Term.StructInst.instToStringStructInstView : ToString Lean.Elab.Term.StructInst.StructInstView

instance Lean.Elab.Term.StructInst.instToFormatField : Lean.ToFormat Lean.Elab.Term.StructInst.Field

instance Lean.Elab.Term.StructInst.instToStringField : ToString Lean.Elab.Term.StructInst.Field

Equations

• Lean.Elab.Term.StructInst.instToStringField = { toString := toString ∘ Lean.format }

def Lean.Elab.Term.StructInst.StructInstView.modifyFieldsM {m : Type → Type} [Monad m] (s : Lean.Elab.Term.StructInst.StructInstView) (f : List Lean.Elab.Term.StructInst.Field → m (List Lean.Elab.Term.StructInst.Field)) : m Lean.Elab.Term.StructInst.StructInstView

def Lean.Elab.Term.StructInst.StructInstView.modifyFields (s : Lean.Elab.Term.StructInst.StructInstView) (f : List Lean.Elab.Term.StructInst.Field → List Lean.Elab.Term.StructInst.Field) : Lean.Elab.Term.StructInst.StructInstView

def Lean.Elab.Term.StructInst.mkProjStx? (s : Lean.Syntax) (structName fieldName : Lean.Name) : Lean.Elab.TermElabM (Option Lean.Syntax)

Creates projection notation for the given structure field. Used

def Lean.Elab.Term.StructInst.findField? (fields : List Lean.Elab.Term.StructInst.Field) (fieldName : Lean.Name) : Option Lean.Elab.Term.StructInst.Field

Finds a simple field of the given name.

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

The constructor to use for the structure instance notation.

• ctorFn : Lean.Expr

  The constructor function with applied structure parameters.

• ctorFnType : Lean.Expr

  The type of ctorFn

• instMVars : Array Lean.MVarId

  Instance metavariables for structure parameters that are instance implicit.

• params : Array (Lean.Name × Lean.Expr)

  Type parameter names and metavariables for each parameter. Used to seed StructInstView.params.

def Lean.Elab.Term.StructInst.markDefaultMissing (e : Lean.Expr) : Lean.Expr

Annotates an expression that it is a value for a missing field.

Equations

• Lean.Elab.Term.StructInst.markDefaultMissing e = Lean.mkAnnotation `structInstDefault e

def Lean.Elab.Term.StructInst.defaultMissing? (e : Lean.Expr) : Option Lean.Expr

If the expression has been annotated by markDefaultMissing, returns the unannotated expression.

Equations

• Lean.Elab.Term.StructInst.defaultMissing? e = Lean.annotation? `structInstDefault e

def Lean.Elab.Term.StructInst.throwFailedToElabField {α : Type} (fieldName structName : Lean.Name) (msgData : Lean.MessageData) : Lean.Elab.TermElabM α

Throws "failed to elaborate field" error.

def Lean.Elab.Term.StructInst.trySynthStructInstance? (s : Lean.Elab.Term.StructInst.StructInstView) (expectedType : Lean.Expr) : Lean.Elab.TermElabM (Option Lean.Expr)

If the struct has all-missing fields, tries to synthesize the structure using typeclass inference.

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

The result of elaborating a StructInstView structure instance view.

• val : Lean.Expr

  The elaborated value.

• struct : Lean.Elab.Term.StructInst.StructInstView

  The modified StructInstView view after elaboration.

• instMVars : Array Lean.MVarId

  Metavariables for instance implicit fields. These will be registered after default value propagation.

structure Lean.Elab.Term.StructInst.DefaultFields.Context : Type

Context for default value propagation.

• structs : Array Lean.Elab.Term.StructInst.StructInstView

  The current path through .nested subobject structures. We must search for default values overridden in derived structures.

• allStructNames : Array Lean.Name

  The collection of structures that could provide a default value.

• maxDistance : Nat

  Consider the following example:

  structure A where
    x : Nat := 1
  
  structure B extends A where
    y : Nat := x + 1
    x := y + 1
  
  structure C extends B where
    z : Nat := 2*y
    x := z + 3
  

  And we are trying to elaborate a structure instance for C. There are default values for x at A, B, and C. We say the default value at C has distance 0, the one at B distance 1, and the one at A distance 2. The field maxDistance specifies the maximum distance considered in a round of Default field computation. Remark: since C does not set a default value of y, the default value at B is at distance 0.

  The fixpoint for setting default values works in the following way.

  • Keep computing default values using maxDistance == 0.
  • We increase maxDistance whenever we failed to compute a new default value in a round.
  • If maxDistance > 0, then we interrupt a round as soon as we compute some default value. We use depth-first search.
  • We sign an error if no progress is made when maxDistance == structure hierarchy depth (2 in the example above).

structure Lean.Elab.Term.StructInst.DefaultFields.State : Type

State for default value propagation

• progress : Bool

  Whether progress has been made so far on this round of the propagation loop.

partial def Lean.Elab.Term.StructInst.DefaultFields.collectStructNames (struct : Lean.Elab.Term.StructInst.StructInstView) (names : Array Lean.Name) : Array Lean.Name

Collects all structures that may provide default values for fields.

partial def Lean.Elab.Term.StructInst.DefaultFields.getHierarchyDepth (struct : Lean.Elab.Term.StructInst.StructInstView) : Nat

Gets the maximum nesting depth of subobjects.

def Lean.Elab.Term.StructInst.DefaultFields.isDefaultMissing? {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (field : Lean.Elab.Term.StructInst.Field) : m Bool

Returns whether the field is still missing.

partial def Lean.Elab.Term.StructInst.DefaultFields.findDefaultMissing? {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (struct : Lean.Elab.Term.StructInst.StructInstView) : m (Option Lean.Elab.Term.StructInst.Field)

Returns a field that is still missing.

def Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (struct : Lean.Elab.Term.StructInst.StructInstView) : m (Array Lean.Elab.Term.StructInst.Field)

Returns all fields that are still missing.

Equations

• Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing struct = (Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing.go struct *> get).run' #[]

partial def Lean.Elab.Term.StructInst.DefaultFields.allDefaultMissing.go {m : Type → Type} [Monad m] [Lean.MonadMCtx m] (struct : Lean.Elab.Term.StructInst.StructInstView) : StateT (Array Lean.Elab.Term.StructInst.Field) m Unit

def Lean.Elab.Term.StructInst.DefaultFields.getFieldName (field : Lean.Elab.Term.StructInst.Field) : Lean.Name

Returns the name of the field. Assumes all fields under consideration are simple and named.

@[reducible, inline]

abbrev Lean.Elab.Term.StructInst.DefaultFields.M (α : Type) : Type

Equations

• Lean.Elab.Term.StructInst.DefaultFields.M = ReaderT Lean.Elab.Term.StructInst.DefaultFields.Context (StateRefT' IO.RealWorld Lean.Elab.Term.StructInst.DefaultFields.State Lean.Elab.TermElabM)

def Lean.Elab.Term.StructInst.DefaultFields.isRoundDone : Lean.Elab.Term.StructInst.DefaultFields.M Bool

Returns whether we should interrupt the round because we have made progress allowing nonzero depth.

def Lean.Elab.Term.StructInst.DefaultFields.getFieldValue? (struct : Lean.Elab.Term.StructInst.StructInstView) (fieldName : Lean.Name) : Option Lean.Expr

Returns the expr? for the given field.

Equations

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

def Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValue? (struct : Lean.Elab.Term.StructInst.StructInstView) (cinfo : Lean.ConstantInfo) : Lean.Elab.TermElabM (Option Lean.Expr)

Instantiates a default value from the given default value declaration, if applicable.

partial def Lean.Elab.Term.StructInst.DefaultFields.mkDefaultValue?.process (struct : Lean.Elab.Term.StructInst.StructInstView) : Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)

partial def Lean.Elab.Term.StructInst.DefaultFields.reduce (structNames : Array Lean.Name) (e : Lean.Expr) : Lean.MetaM Lean.Expr

Reduces a default value. It performs beta reduction and projections of the given structures to reduce them to the provided values for fields.

partial def Lean.Elab.Term.StructInst.DefaultFields.reduce.withReduceLCtx (structNames : Array Lean.Name) {α : Type} (xs : Array Lean.Expr) (k : Lean.MetaM α) (i : Nat := 0) : Lean.MetaM α

Reduce the types and values of the local variables xs in the local context.

def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault (structs : Array Lean.Elab.Term.StructInst.StructInstView) (allStructNames : Array Lean.Name) (maxDistance : Nat) (fieldName : Lean.Name) (mvarId : Lean.MVarId) : Lean.Elab.TermElabM Bool

Attempts to synthesize a default value for a missing field fieldName using default values from each structure in structs.

Equations

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

@[irreducible]

def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault.loop (structs : Array Lean.Elab.Term.StructInst.StructInstView) (allStructNames : Array Lean.Name) (maxDistance : Nat) (fieldName : Lean.Name) (mvarId : Lean.MVarId) (i dist : Nat) : Lean.Elab.TermElabM Bool

partial def Lean.Elab.Term.StructInst.DefaultFields.step (struct : Lean.Elab.Term.StructInst.StructInstView) : Lean.Elab.Term.StructInst.DefaultFields.M Unit

Performs one step of default value synthesis.

partial def Lean.Elab.Term.StructInst.DefaultFields.propagateLoop (hierarchyDepth d : Nat) (struct : Lean.Elab.Term.StructInst.StructInstView) : Lean.Elab.Term.StructInst.DefaultFields.M Unit

Main entry point to default value synthesis in the M monad.

def Lean.Elab.Term.StructInst.DefaultFields.propagate (struct : Lean.Elab.Term.StructInst.StructInstView) : Lean.Elab.TermElabM Unit

Synthesizes default values for all missing fields, if possible.

Equations

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

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