max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improve performance of structure instance notation elaboration (#13760)

Browse source 
This PR improves elaboration performance for structure instance notation
with large numbers of fields. It also uses beta-reducing substitution
for structure parameters, which is already the case for structure
fields.

It substitutes field values into types when they are needed, avoiding
quadratic runtime complexity.
This commit is contained in:
Kyle Miller 2026-05-21 09:53:33 -07:00 • committed by GitHub
parent ed790e99b0
commit 1842bb5476
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/StructInst.lean
View file

@ -414,6 +414,7 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (structureType? : Option Exp
for _ in *...ctorVal.numParams do
let .forallE _ d b bi := type
| throwError "unexpected constructor type"
let d := d.instantiateBetaRevRange 0 params.size params
let param ←
if bi.isInstImplicit then
let mvar ← mkFreshExprMVar d .synthetic
@ -422,7 +423,8 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (structureType? : Option Exp
else
mkFreshExprMVar d
params := params.push param
type := b.instantiate1 param
type := b
type := type.instantiateBetaRevRange 0 params.size params
let structType := mkAppN (.const ctorVal.induct us) params
if let some structureType := structureType? then
discard <| isDefEq structureType structType
@ -611,7 +613,8 @@ private structure StructInstContext where
fieldViews : ExpandedFields
private structure StructInstState where
/-- The type of the flat constructor with applied parameters and applied fields. -/
/-- Initially the type of the flat constructor after applying parameters. After each field, we
replace it with its body. May have bvars; needs to be instantiated with `fields`. -/
type : Expr
/-- A set of the structure name and all its parents. -/
structNameSet : NameSet := {}
@ -721,7 +724,7 @@ private def normalizeExpr (e : Expr) (zetaDeltaImpl : Bool := true) : StructInst
private def addStructFieldAux (fieldName : Name) (e : Expr) : StructInstM Unit := do
trace[Elab.structInst] "field {fieldName} := {.nestD e}"
modify fun s => { s with
type := s.type.bindingBody!.instantiateBetaRevRange 0 1 #[e]
type := s.type.bindingBody!
fields := s.fields.push e
fieldMap := s.fieldMap.insert fieldName e
}
@ -1141,6 +1144,8 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
private partial def loop : StructInstM Expr := withViewRef do
let type := (← get).type
if let .forallE fieldName fieldType _ binfo := type then
let fields := (← get).fields
let fieldType := fieldType.instantiateBetaRevRange 0 fields.size fields
if let some fieldValue := (← get).fieldMap.find? fieldName then
-- This is a field that was added by `addParentInstanceFields`
trace[Elab.structInst] "processing inferred field `{fieldName}` : {fieldType}\ninferred value:{inlineExprTrailing fieldValue}"