Macros accessing global variables

Both macros and procedures generate Go functions in PGo. In other words, after parsing, there are not many differences between PlusCal's macro and procedure. However, I believe there should be (PlusCal created the distinction for a reason.)

The issue (that I observed as the result of one of the failing tests at the time) is that macros that attempt to access global state break PGo. Consider the following macro, extracted from test/pluscal/TwoPhaseCommit.tla:

--algorithm TwoPhaseCommit
variables stage = [mgr \in managers |-> "start"];

macro SetAll(state, kmgrs) {
    with (km \in kmgrs) {
        stage[km] := state
    };
}

When generating source code, PGo attempts to create a function SetAll which does what the macro is supposed to do. However, PlusCal expands macros at translation time -- as such, labels (as well as a set of other constructs) are not allowed in macros. When PGo is generating source code for the macro above, it notices the global variable assignment and tries to find the label to which it belongs (as part of the "atomicity" stage.) This breaks since this is a macro and therefore there are no labels.

I don't think there's an immediate fix for this problem (and it is a recurring pattern to have macros accessing global state, from a few other specs I analyzed). Perhaps what we could do is literally expand macros in the Go source code as well, since it's the only place where we will have labeling/atomicity context. This may lead to duplication, but since the set of things you can do in a macro is a lot more limited (no while, function call, labels, etc), it might not be too bad.

DistCompiler / pgo

Macros accessing global variables #18