Lean4
/-- Get `FunctionData` for `f`. Throws if `f` can't be put into funProp-normal form. -/
def getFunctionData (f : Expr) : MetaM FunctionData := do
lambdaTelescope f fun xs b => do
let xId := xs[0]!.fvarId!
Mor.withApp b fun fn args => do
let mut fn := fn
let mut args := args
if let .proj n i x := fn then
let some info := getStructureInfo? (← getEnv) n |
unreachable!
let some projName := info.getProjFn? i |
unreachable!
let p ← mkAppM projName #[x]
fn := p.getAppFn
args := p.getAppArgs.map (fun a => { expr := a }) ++ args
let mainArgs :=
args |>.mapIdx (fun i ⟨arg, _⟩ => if arg.containsFVar xId then some i else none) |>.filterMap id
return
{ lctx := ← getLCtx
insts := ← getLocalInstances
fn := fn
args := args
mainVar := xs[0]!
mainArgs := mainArgs }
