Lean4
/-- If `e` has a structure as type with field `fieldName` (either directly or in a parent
structure), `mkProjection e fieldName` creates the projection expression `e.fieldName` -/
def mkProjection (e : Expr) (fieldName : Name) : MetaM Expr := do
let .const structName _ := (← whnf (← inferType e)).getAppFn |
throwError "{e} doesn't have a structure as type"
let some baseStruct := findField? (← getEnv) structName fieldName |
throwError "No parent of {structName } has field {fieldName}"
let mut e := e
for projName in (getPathToBaseStructure? (← getEnv) baseStruct structName).get! do
let type ← whnf (← inferType e)
let .const _structName us := type.getAppFn |
throwError "{e} doesn't have a structure as type"
e := mkAppN (.const projName us) (type.getAppArgs.push e)
mkDirectProjection e fieldName
