Lean4
/-- Auxiliary function of `getCompositeOfProjections`. -/
partial def getCompositeOfProjectionsAux (proj : String) (e : Expr) (pos : Array Nat) (args : Array Expr) :
MetaM (Expr × Array Nat) := do
let env ← getEnv
let .const structName _ := (← whnf (← inferType e)).getAppFn |
throwError "{e} doesn't have a structure as type"
let projs := getStructureFieldsFlattened env structName
let projInfo :=
projs.toList.map fun p ↦ do
((← dropPrefixIfNotNumber? proj (p.lastComponentAsString ++ "_")).toString, p)
let some (projRest, projName) := projInfo.reduceOption.getLast? |
throwError "Failed to find constructor {(proj.dropRight 1)} in structure {structName}."
let newE ← mkProjection e projName
let newPos :=
pos ++
(← findProjectionIndices structName projName)
-- we do this here instead of in a recursive call in order to not get an unnecessary eta-redex
if projRest.isEmpty then
let newE ← mkLambdaFVars args newE
return (newE, newPos)
let type ← inferType newE
forallTelescopeReducing type fun typeArgs _tgt ↦ do
getCompositeOfProjectionsAux projRest (mkAppN newE typeArgs) newPos (args ++ typeArgs)
