Enums with identical literals not always detected

[treiher]

The detection of identical literals does not work correctly in some cases.

package Test is

   type A is (A => 2, B => 0) with Size => 2;

   type B is (A => 0) with Size => 1;

   type C is
      message
         A : A;
         AA : A;
         AAAA : B;
      end message;

end Test;

Actual

rflx: model error: contradicting condition 0 from field "Initial" to "A" on path [] in "Test.C" (A = 0
   ∧ A = 2)

Expected

rflx: parser error: "Test.B" contains identical literals as "Test.A": A

[senier]

Thanks! I'll try this with the current state once #248 is done. Are you sure this is a "parser"-related issue. Isn't this actually a model error?

[treiher]

The current check for identical literals is done in the parser, but I think it would better fit in the model. An appropriate location would be model.Model.

[senier]

Moving those checks to the model is not easily doable, as we store enumeration elements as a dict. Consequently, duplicate elements are not available anymore after parsing. While we could change the data structure, I don't think it's worth the effort.

I changed your example, as your literals also conflict with the types (which creates even more noise):

package Test is
                                                                                                                                                                              
   type A is (E1 => 2, E2 => 0) with Size => 2;

   type B is (E1 => 0) with Size => 1;

   type C is
      message
         A : A;
         AA : A;
         AAAA : B;
      end message;

end Test;

After the integration of #248, I get:

Parsing test.rflx
Processing Test
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:9:10: model: info: on path: "A"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:9:10: model: info: on path: "A"
test.rflx:10:10: model: info: on path: "AA"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:9:10: model: info: on path: "A"
test.rflx:10:10: model: info: on path: "AA"
test.rflx:11:10: model: info: on path: "AAAA"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:5:4: parser: error: conflicting literals: E1
test.rflx:5:15: parser: info: previous occurrence of "E1"

The last two lines correctly indicate the problem, even though the location information is wrong. After fixing that, I get:

Parsing test.rflx
Processing Test
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:9:10: model: info: on path: "A"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:9:10: model: info: on path: "A"
test.rflx:10:10: model: info: on path: "AA"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:7:4: model: error: contradicting condition in "Test.C"
test.rflx:9:10: model: info: on path: "A"
test.rflx:10:10: model: info: on path: "AA"
test.rflx:11:10: model: info: on path: "AAAA"
test.rflx:3:4: model: info: unsatisfied "E1 = 2"
test.rflx:5:4: model: info: unsatisfied "E1 = 0"
test.rflx:5:4: parser: error: conflicting literals: E1
test.rflx:3:15: parser: info: previous occurrence of "E1"

The contradicting conditions errors are technically correct, but of cause only present due to the bogus enumeration elements. We could try to flag the type errors in the parser and omit the contradiction test in such cases. However, doing this is not straightforward. Again, I don't think it's worth the effort. I'd just fix the location issue and leave the contradiction errors.

What do you think?

[treiher]

Moving those checks to the model is not easily doable, as we store enumeration elements as a dict. Consequently, duplicate elements are not available anymore after parsing.

We are currently using only the dicts for checking duplicates between different enumeration types, thus it should be possible to move the check_types part in parser.Parser to model.Model. You are right about checking for duplicates in one enum, which is already done in parser.grammar.

We could try to flag the type errors in the parser and omit the contradiction test in such cases. However, doing this is not straightforward. Again, I don't think it's worth the effort.

I agree. That would increase the complexity with little benefit.