Accepting labels as macros' arguments

[shayanh]

PlusCal and MPCal don't accept labels as macros' arguments. Input labels in macros can be used in goto statements. For example, by having this we can define the following macro, which is useful for defining failure:

macro mayFail(fLabel) {
    if (EXPLORE_FAIL) {
        either {
            skip;
        } or {
            goto fLabel;
        };
    };
};

I think we can extend macros behavior in MPCal by substituting goto labels with the arguments values if the labels are present in the macro's arguments.

Finn's comment:

straw-man syntax, if I remember: label fLabel as an argument, to distinguish

[shayanh]

More precise description:

label type

In PlusCal and MPCal labels are static names and a variable cannot store a label. We propose a new type of variable that stores labels. As a result we can pass labels to macros and procedures(?) as their arguments.

archetype Foo()
label myLabel;
{
    l1: skip;
    l2: myLabel := l1;
}

Motivation

For simulating failure behavior, being able to pass labels as macros' arguments helps to avoid code duplication (DRY principle). For instance, the following macro is really helpful for the failure behavior simulation:

macro mayFail(label fLabel) {
    either { skip; } or {
        goto fLabel;
    }
}