Lean4
/-- Decompose function `f = (← fData.toExpr)` into composition of two functions.
Returns none if the decomposition would produce composition with identity function. -/
def nontrivialDecomposition (fData : FunctionData) : MetaM (Option (Expr × Expr)) := do
let mut lctx := fData.lctx
let insts := fData.insts
let x := fData.mainVar
let xId := x.fvarId!
let xName ← withLCtx lctx insts xId.getUserName
let fn := fData.fn
let mut args := fData.args
if fn.containsFVar xId then
return ← fData.peeloffArgDecomposition
let mut yVals : Array Expr := #[]
let mut yVars : Array Expr := #[]
for argId in fData.mainArgs do
let yVal := args[argId]!
let yVal' := yVal.expr
let yId ← withLCtx lctx insts mkFreshFVarId
let yType ← withLCtx lctx insts (inferType yVal')
if yType.containsFVar fData.mainVar.fvarId! then
return none
lctx := lctx.mkLocalDecl yId (xName.appendAfter (toString argId)) yType
let yVar := Expr.fvar yId
yVars := yVars.push yVar
yVals := yVals.push yVal'
args := args.set! argId ⟨yVar, yVal.coe⟩
let g ←
withLCtx lctx insts do
mkLambdaFVars #[x] (← mkProdElem yVals)
let f ←
withLCtx lctx insts do
(mkLambdaFVars yVars (Mor.mkAppN fn args)) >>= mkUncurryFun yVars.size
let f' ← fData.toExpr
if (← withReducibleAndInstances <| isDefEq f' f <||> isDefEq f' g) then
return none
return (f, g)
