Lean4
/-- Return the positions that `kabstract` would abstract for pattern `p` in expression `e`.
i.e. the positions that unify with `p`. -/
def kabstractPositions (p e : Expr) : MetaM (Array SubExpr.Pos) := do
let e ← instantiateMVars e
let mctx ← getMCtx
let pHeadIdx := p.toHeadIndex
let pNumArgs := p.headNumArgs
let rec /-- The main loop that loops through all subexpressions -/
visit (e : Expr) (pos : SubExpr.Pos) (positions : Array SubExpr.Pos) : MetaM (Array SubExpr.Pos) := do
let visitChildren : Array SubExpr.Pos → MetaM (Array SubExpr.Pos) :=
match e with
| .app fn arg => visit fn pos.pushAppFn >=> visit arg pos.pushAppArg
| .mdata _ expr => visit expr pos
| .proj _ _ struct => visit struct pos.pushProj
| .letE _ type value body _ =>
visit type pos.pushLetVarType >=> visit value pos.pushLetValue >=> visit body pos.pushLetBody
| .lam _ binderType body _ => visit binderType pos.pushBindingDomain >=> visit body pos.pushBindingBody
| .forallE _ binderType body _ => visit binderType pos.pushBindingDomain >=> visit body pos.pushBindingBody
| _ => pure
if e.hasLooseBVars then
visitChildren positions
else if e.toHeadIndex != pHeadIdx || e.headNumArgs != pNumArgs then
visitChildren positions
else
if ← isDefEq e p then
setMCtx mctx
visitChildren (positions.push pos)
else
visitChildren positions
visit e .root #[]
