Expr.foldlM

Stream: mathlib4

[Jeremy Salwen]

Is Expr.foldlM supposed to traverse all subexpressions recursively, or just direct children? The name and docstring suggest the former, but based on this example, it seems to do the latter:

import Qq
import Lean
import Lean.Expr
import Mathlib.Lean.Expr.Traverse

open Lean Meta Elab Term Lean.Meta Tactic Qq

def foo: Expr:= q(∀ (f:Nat->Nat) (a b c:Nat), f (a+b) = c)

def logSubexprs : Nat → Expr → MetaM Nat
| _, e => do
  dbg_trace e
  return 0

#eval foo.foldlM logSubexprs 0

Normally I would look at the implementation to figure out what it's supposed to do, but it's a bit over my head:
https://github.com/leanprover-community/mathlib4/blob/77ba88838571d5d50acc4a65740e1080026fa12e/Mathlib/Lean/Expr/Traverse.lean#L28-L30

/-- `e.foldlM f a` folds the monadic function `f` over the subterms of the expression `e`,
with initial value `a`. -/
def foldlM {α : Type} {m} [Monad m] (f : α → Expr → m α) (x : α) (e : Expr) : m α :=
Prod.snd <$> (StateT.run (e.traverseChildren $ fun e' =>
    Functor.mapConst e' (get >>= monadLift ∘ flip f e' >>= set)) x : m _)

What would be the recommended way of folding over all children recursively, would I just use MetaM.transform?

[Kyle Miller]

It's a fold over the immediate subexpressions of each expression

[Kyle Miller]

I don't know the answer to your question, but one recursive version of that is https://github.com/leanprover-community/mathlib4/blob/f7b450735677ab422ab00e78d84818f9c5f96d86/Mathlib/Lean/Expr/ReplaceRec.lean#L28

[Jeremy Salwen]

This seems to do the trick for me:

def Expr.foldlRecM [Monad m] [AddMessageContext m] [MonadOptions m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m]
(f: α -> Expr -> m α) (init: α) (e: Expr): m α := do
  Prod.snd <$> (StateT.run (transform e $ fun e' =>
    Functor.mapConst TransformStep.continue (get >>= monadLift ∘ flip f e' >>= set)) init : m _)