macro generating multiple doElem

Stream: lean4

[Jonathan Protzenko]

how can I author a macro that produces multiple doElems, suitable for using within a do-block?

this is not working:

macro "let" e:ident " ⟵ " f:term : doElem =>
  `(doElem|
    let x := 0
    let $e := $f + x
  )

• I tried using the doSeq class from the Lean internal parser but then I got a panic
• I tried generating both bindings on a single line separated by ; but that didn't work either

any thoughts? thanks!

[Chris Bailey]

This doesn't answer your immediate question, but I tested this out using the coercion from Subtype A to A in hashmap_test1_fwd:

macro "let" e:ident " ⟵ " f:term : doElem =>
  `(doElem| let $e ← Result.attach $f)

And that doesn't seem to fix the elaboration time issue. After poking it some more there seems to just be a blowup in the later do blocks in the else branches of your larger definition, so I think it's a do elaboration issue and not the let desugaring.

[Jonathan Protzenko]

thanks Chris this is super helpful!

[Gabriel Ebner]

how can I author a macro that produces multiple doElems, suitable for using within a do-block?

This is maybe a tiny bit confusing, but do is heavily overloaded and you can use a "nested do" to combine multiple do-elems:

macro "let" e:ident " ⟵ " f:term : doElem =>
  `(doElem|do
    let x := 0
    let $e := $f + x
  )

#eval show Option _ from do let foo ⟵ 42; pure foo

[Jonathan Protzenko]

thanks Gabriel, that's great to know! indeed, equipped with this, I can confirm that my other issue (elaboration taking a long while for nested do-s) isn't related to the overloaded \langle, \rangle operator

[Jonathan Protzenko]

(see my most recent message in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/naming.20hypotheses.20when.20using.20do-notation/near/328123483)