I understand you used OBJECT_TYPE because of the rule ambiguity. However, this raises a concern, because it allows for multiple chaining of ids (e.g., Mode.photo.photo, Mode.photo.photo.photo, etc.) which should not be syntactically valid.

We could avoid the ambiguity by forcing the OBJECT_TYPE to always start with a lowercase letter and declare enumCall as ID '.' ID, but Java packages are allowed start with an uppercase letter (even though it's highly discouraged).

So, we can introduce another terminal, just for enums:

enumCall: 
	ENUM_CALL;

// ...

ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*;

This way, you guarantee the enums are always represented by two ids separated by a dot, without ambiguity.

That's understandable, my issue with that, at the time of development, was if ID and ID_UPPER wouldn't, even if they are slightly different, lead to ambiguity due to other grammar rules. I should've explored more formats.

It would be nice to have support for enums that live in another package, via qualified name. I agree with @rcosta358 that we want a first version working, and then we can think about this. To achieve this, we need a name resolution (à lá Spoon).

Why global? Shouldn't it only be visible within the class or package where it was declared?

If there is an enum that is used across methods, and a shared package is needed, when the context is reinitialized, the local context is cleaned. If it's kept in the global context, the placement is irrelevant.
For example, the following common package a layer above the testSuite.

When line 134 is changed to context.addVarToContext(varName, enumRead.getReference(), refinement, enumRead), the following occurs:

That's not really a shared package because it's not even included in the verification, each test is ran individually from its file or folder.

The issue is: if I declare an enum X in class A, should I be able to use it in class B? It might be fine, just raising some questions about how it should work.

Also, if we can use enums from different classes, we should make sure they have their fully qualified name to distinguish enums with the same name from different classes.

I didn't realize the testing was that restrictive. I can try and create some test scenarios that take into consideration global and local context. The other option would be to restrict enum verification to only in the same file, but that feels like a cop-out instead of an actual fix/intended functionality. 🤔

I don't like the "enum#%s#%s" format because it's hard to read in the error messages. Here you can simply return the enumText, and everywhere else still use this format but change it to "%s.%s" instead.

I should've gone with a better format, I admit. I wasn't sure due to the rest of the existing types.

We might want to "decode" enums when they come back in the error messages back to their Refinement version. Two approaches: 1) having a translation map. 2) storing the source of each variable in the Verification Condition (I'm doing this in aeon, and I think we discussed it for LJ).

This is not specific for Enums, we might want to do this for other types.

is there a reason for this to be an IntSort if we created the EnumSorts before?

It was part of a case I was trying to cover, but I ended up learning that it could only use a sort with an actual enum type, not the abstract class java.lang.Enum. I think I forgot to remove it 💫