Generating tables with subtyping (Bug in Generatorfactory.cpp)

When generating a table with a variable typed X, the type check should be done in several cases.

For example: If P is typed Y and X isa Y, then:

If P(x[X]) is generated, typecheck should be done.

If ~P(x[X]) is generated, typecheck should not be done as ~P(d) holds for all elements outside of X anyway.

If it is the other way round: P is typed Y and Y isa X, it is the other way

If ~P(x[X]) is generated, typecheck should be done, well in fact not a check, but we should generate the ~P table + all X's that are no Y.

If P(x[X]) is generated, typecheck should not be done as P does not hold outside of Y anyway.

This is still incorrectly implemented (attached file shows this) even though we have already iterated many times over this code! Should be implemented carefully!!!!

Comments (3)