Fix and improve meta capabilities

[grayswandyr]

The meta capability system is broken in Alloy 6. In addition to fixing it, it would be very useful to improve the system, at the very least by providing such capabilities for var and non-var stuff.

[nmacedo]

I've fixed this and added additional meta-sigs, ssig$ and vsig$ for static and mutable sigs, respectively, and likewise for fields with sfield$ and vfield$. Names are temporary, let me know your suggestions (and whether I should add anything else).

[grayswandyr]

Thanks!

As far as I'm concerned, the chosen names are ok with me. The alternative is to write static and var rather than s and v but this will create long names...

Now, for the sake of the discussion, I'm copy-pasting this doc from Alloy 4:

When the model contains at least one attempt to reference a meta atom, then the model will be automatically augmented with meta atoms as follows:

1. For each user-defined sig X, we add a meta atom "X$"; and for each field Y in a user defined sig X, we add a meta atom "X$Y".
2. Given the meta atom "X$" representing some user signature; "X$.fields" represents the meta atoms for its immediate fields and "X$.subfields" the meta atoms for it and all descendants' fields.
3. Given the meta atom "X$Y" representing some field; "X$Y.value" represents the actual field value in the real world.
4. An atom "sig$" is added that represents the union of all meta atoms that represent signatures as well as a "field$" atom representing the union of all meta atoms that represent fields.

IIUC, you refined item 4 by adding ssig$, vsig$, sfield$ and vfield$, right?

If possible, I was also thinking it could be useful:

• to also add var$ (= vsig$ + vfield$) and static$ (= ssig$ + sfield$);
• to also refine item 2 with operations .vfields, .sfields, .vsubfields and .ssubfields (with obvious meanings).

[nmacedo]

• Yes, I thought of using static and var prefixes but also felt it would be too long.

• Sure, I can add the var$ and static$ macros. By the way, the sig$ and field$ are now defined simply as macros ssig$ + vsig$, and sfield$ + vfield$, respectively.

• Glad you brought up the documentation, because there's actually another field defined in the code that is not documented, the parent of a signature. I don't know why it's been excluded from the documentation, but it is available in the standard distribution.

[grayswandyr]

* Glad you brought up the documentation, because there's actually another field defined in the code that is not documented, the `parent` of a signature. I don't know why it's been excluded from the documentation, but it is available in the standard distribution.

Good to know. It's only defined for extends I suppose? An ancestors field could be in order too, for completeness.

[grayswandyr]

After discussion: exhibiting parent and adding a var meta-sig should be enough to yield all the meta-stuff discussed just above.

[nmacedo]

Done, there are now sigs static$ and var$ for the static and mutable elements, respectively. Variants of sig$ and field$ were removed, they can be obtained by intersecting with the new sigs (e.g., sig$ & var$ for the mutable sigs, field$ & static$ for the static fields).