@[implicit_reducible]

instance Strata.Laurel.instToStringInferHoleTypesStats : ToString InferHoleTypesStats

Equations

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

Hole Type Inference

Annotate each .Hole node with a type inferred from its surrounding context using the SemanticModel and computeExprType. After this pass every Hole carries some ty so that the hole elimination pass can generate correctly typed uninterpreted functions.

Every node is handled by inferExpr with an expectedType parameter. For statement positions the expected type is TVoid, except for the last statement in a block which inherits the block's expected type, and for return expressions which use the procedure's output type.

inductive Strata.Laurel.InferHoleTypesStats : Type

• holesAnnotated : InferHoleTypesStats

  Number of holes successfully annotated with an inferred type.

• holesLeftUnknown : InferHoleTypesStats

  Number of holes left with Unknown type (context could not determine type).

structure Strata.Laurel.InferHoleState : Type

• model : SemanticModel
• currentOutputType : HighTypeMd
• statistics : Statistics
• diagnostics : List DiagnosticModel

def Strata.Laurel.inferHoleTypes (model : SemanticModel) (program : Program) : Program × List DiagnosticModel × Statistics

Annotate every .Hole in the program with a type inferred from context.

Equations

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