Adding to do-blocks in macros

Stream: metaprogramming / tactics

[Devon Tuma]

I'm working on trying to get syntax like Pr[b ∧ x[0] ≠ 0 | b ←$ᵗ Bool; x ←$ᵗ Vector F 3] to work, and I'm wondering if there is a better approach that makes explicit use of do-blocks. I have some hacky code here that can handle simple cases, but it isn't as general as a do-block would be (e.g. later calls can't depend on earlier variables). It would be nice if I could generate do b ←$ᵗ Bool; x ←$ᵗ Vector F 3; b ∧ x[0] ≠ 0 in the above example, and then just consider the odds of it returning true, since then free variable binding would be handled automatically. However I'm having trouble understanding how to make use of the do-notation parser in the macro definition. Is there a more natural way to handle something like this?