TypedValue - Lack of information

[tfabbri]

The structure TypedValue presents a lack of information for Union and Record types.
Considering the following example where MyRecord1 and MyRecord2 are two records characterized by different structure:

types
    MyUnion = MyRecord1 | MyRecord2

at C code level is not possible to distinguish between the two types by checking the type field (both are characterized by type=VDM_RECORD).
Possible solution: Add a new field to TypedValue containing the name of the type (alias = 'MyRecord1' and alias='MyRecord2').

[bandurvp]

The runtime library now supports full is_ type checks, so it is now possible to implement the following:

types
    MyUnion = MyRecord1 | MyRecord2
...
return is_(exp, MyRecord1);

The runtime function is(...) takes as one of its arguments a text encoding of the type being queried, in this case either MyRecord1 or MyRecord2. There is a function in the Java side of VDM2C called IsExpTypeEncoder.encodeType that will emit this encoding. For examples of how this is used, refer to IsExpTypeEncoderTest.java in the Java side of the generator. I think this will give you all the information you need to progress with this. What do you think @tfabbri ?

[tfabbri]

To be honest I do not remember well the issue. The problem was about the support for union types as in #21. Have you developed such support?

[peterwvj]

Not directly, but as Victor said above, you can now generate the char encoding for such types - see #108 (comment) for details. Based on the encoding you can use the is function in the runtime to check if a value is of a given type. IsExpEncoderTest.java contains several examples and shows you how to utilize the encoder, #108 (comment) contains another example that includes union types.