elaboration of nested actions: f (← t) (← u)

Stream: metaprogramming / tactics

[Mathis Bouverot-Dupuis]

Hello ! Is there a description somewhere of how Lean elaborates the syntax for "nested actions" (terms such as f (← t) (← u)) ? Either in a paper or in some documentation page? Or is the best/only description the implementation?

[Robin Arnez]

See the language reference documentation
Basically

f (← t) (← u)

converts to

let x ← t
let y ← u
f x y

[Mathis Bouverot-Dupuis]

AFAICT the reference documentation only gives examples. It can get quite involved in some cases, hence why I'm looking for a formal-ish description of the process.

For instance I find the following quite surprising:

#check (fun (m : Type -> Type) (_ : Bind m) (f : m Nat -> m Unit) (t : m Bool) (a b : m Nat) => do
  f (if (<- t) then a else b))

which is elaborated to:

fun m x f t a b => do
  let __do_lift ← t
  f (if __do_lift = true then a else b)

i.e. ← t is hoisted above f, which doesn't match my intuition: what if f throws away its argument? Then the elaborated code evaluates the side effects of t but not the side-effects of the remainder of the argument to f (i.e. a or b).

[Aaron Liu]

the hoisting is done to the nearest enclosing do block, so if you want the hoisting of t to occur within the argument of f you can do f (do if (<- t) then a else b)

[Eric Wieser]

It's perhaps worth noting that these are different ifs; the original example is if the term, Aaron's suggested replacement is if the doElem

[Eric Wieser]

Notably this means that

do
   if c then
    return (← t)
  else
    return (← e)

is not the same as

do
  let _t ← t
  let _e ← e
  if c then
    return _t
  else
    return _e

which would of course defeat the point of an if, and instead means

do
  if c then
    let _t ← t
    return _t
  else
    let _e ← e
    return _e

[Sebastian Graf]

See https://github.com/leanprover/lean4/blob/bda15f6c25557f2b9e4062e640562fc9370e3069/src/Lean/Elab/Do/Legacy.lean#L1317 for the exact way that nested actions expand.