Lean4
/-- Find keys which match the expression, or some subexpression.
Note that repeated subexpressions will be visited each time they appear,
making this operation potentially very expensive.
It would be good to solve this problem!
Implementation: we reverse the results from `getMatch`,
so that we return lemmas matching larger subexpressions first,
and amongst those we return more specific lemmas first.
-/
partial def getSubexpressionMatches {α : Type} (d : DiscrTree α) (e : Expr) : MetaM (Array α) := do
match e with
| .bvar _ =>
return #[]
| .forallE _ _ _ _ =>
forallTelescope e
(fun args body => do
args.foldlM
(fun acc arg => do
pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg)))
(← d.getSubexpressionMatches body).reverse)
| .lam _ _ _ _ | .letE _ _ _ _ _ =>
lambdaLetTelescope e
(fun args body => do
args.foldlM
(fun acc arg => do
pure <| acc ++ (← d.getSubexpressionMatches (← inferType arg)))
(← d.getSubexpressionMatches body).reverse)
| _ =>
e.foldlM
(fun a f => do
pure <| a ++ (← d.getSubexpressionMatches f))
(← d.getMatch e).reverse
