Documentation

Lean.Elab.StructInst

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

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.
Instances For
    def Lean.Elab.Term.StructInst.mkStructInstField (lval : TSyntax `Lean.Parser.Term.structInstLVal) (binders : TSyntaxArray `Lean.Parser.Term.structInstFieldBinder) (type? : Option Term) (val : Term) :
    MacroM (TSyntax `Lean.Parser.Term.structInstField)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      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.
      Instances For

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

        • stx : Syntax

          The syntax of the explicit source.

        • structName : Name

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

        Instances For

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

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

          Instances For

            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
            Instances For

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

              • 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 }.

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

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

                Instances For

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

                  • ref : Syntax

                    The whole field syntax.

                  • The LHS decomposed into components.

                  • val : FieldVal

                    The value of the field.

                  • expr? : Option 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.

                  Instances For

                    The view for structure instance notation.

                    • ref : Syntax

                      The syntax for the whole structure instance.

                    • structName : Name

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

                    • params : Array (Name × Expr)

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

                    • fields : List Field

                      The fields of the structure instance.

                    • sources : SourcesView

                      The additional sources for fields for the structure instance.

                    Instances For

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

                      Equations
                      • { ref := ref, lhs := [head], val := val, expr? := expr? }.isSimple = true
                      • x✝.isSimple = false
                      Instances For

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • s.modifyFields f = (s.modifyFieldsM f).run
                            Instances For

                              Creates projection notation for the given structure field. Used

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

                                Finds a simple field of the given name.

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

                                  The constructor to use for the structure instance notation.

                                  • ctorFn : Expr

                                    The constructor function with applied structure parameters.

                                  • ctorFnType : Expr

                                    The type of ctorFn

                                  • instMVars : Array MVarId

                                    Instance metavariables for structure parameters that are instance implicit.

                                  • params : Array (Name × Expr)

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

                                  Instances For

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

                                    Equations
                                    Instances For

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

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

                                        Throws "failed to elaborate field" error.

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

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

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

                                            The result of elaborating a StructInstView structure instance view.

                                            • val : Expr

                                              The elaborated value.

                                            • The modified StructInstView view after elaboration.

                                            • instMVars : Array MVarId

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

                                            Instances For

                                              Context for default value propagation.

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

                                              • allStructNames : Array 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).
                                              Instances For

                                                State for default value propagation

                                                • progress : Bool

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

                                                Instances For

                                                  Collects all structures that may provide default values for fields.

                                                  Gets the maximum nesting depth of subobjects.

                                                  Returns whether the field is still missing.

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

                                                    Returns a field that is still missing.

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

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

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

                                                      Equations
                                                      Instances For

                                                        Returns the expr? for the given field.

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

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

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

                                                            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 Name) {α : Type} (xs : Array Expr) (k : MetaM α) (i : Nat := 0) :

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

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

                                                            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.
                                                            Instances For
                                                              @[irreducible]
                                                              def Lean.Elab.Term.StructInst.DefaultFields.tryToSynthesizeDefault.loop (structs : Array StructInstView) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) (i dist : Nat) :
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For

                                                                Performs one step of default value synthesis.

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

                                                                Synthesizes default values for all missing fields, if possible.

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