Lean4
/-- Perform head-structure-eta-reduction on expression `e`. That is, if `e` is of the form
`⟨f.1, f.2, ..., f.n⟩` with `f` definitionally equal to `e`, then
`headStructureEtaReduce e = headStructureEtaReduce f` and `headStructureEtaReduce e = e` otherwise.
-/
partial def headStructureEtaReduce (e : Expr) : MetaM Expr := do
let env ← getEnv
let (ctor, args) := e.getAppFnArgs
let some (.ctorInfo { induct := struct, numParams, .. }) := env.find? ctor |
pure e
let some { fieldNames, .. } := getStructureInfo? env struct |
pure e
let (params, fields) := args.toList.splitAt numParams
trace[simps.debug]"rhs is constructor application with params{(indentD params)}\nand fields {indentD fields}"
let field0 :: fieldsTail := fields |
return e
let fieldName0 :: fieldNamesTail := fieldNames.toList |
return e
let (fn0, fieldArgs0) := field0.getAppFnArgs
unless fn0 == struct ++ fieldName0 do
trace[simps.debug]"{fn0 } ≠ {struct ++ fieldName0}"
return e
let (params', reduct :: _) := fieldArgs0.toList.splitAt numParams |
unreachable!
unless params' == params do
trace[simps.debug]"{params' } ≠ {params}"
return e
trace[simps.debug]"Potential structure-eta-reduct:{(indentExpr e)}\nto{indentExpr reduct}"
let allArgs := params.toArray.push reduct
let isEta ←
(fieldsTail.zip fieldNamesTail).allM fun (field, fieldName) ↦
if field.getAppFnArgs == (struct ++ fieldName, allArgs) then pure true else isProof field
unless isEta do
return e
trace[simps.debug]"Structure-eta-reduce:{(indentExpr e)}\nto{indentExpr reduct}"
headStructureEtaReduce reduct
