Traces: type error incorrectly reported for trace tests

[peterwvj]

It seems like the trace environment used to type check a trace test is wrong. For some reason, R is reported as an unknown type, when the trace below is executed.

module A
exports all
definitions 
types

R :: x : int;

operations

op : R ==> R
op (-) == return mk_R(1);

end A

module B

imports from A all
definitions

traces

T :
let r = A`op(mk_A`R(1))
in
  A`op(r);

end B

If the one test derived from the trace is send to the interpreter the test result is reported as:

Generated 1 tests
Test 1 = A`op(mk_R(1))
Result = [Error 3126: Unknown type 'R' in constructor in 'B' (.../A.vdmsl) at line 26:8, FAILED]

T 1 {1.0,NONE,999} = Trace completed

The interpreter thinks that the test is not type correct. Clearly this is wrong, since the record type is imported from module A. The test should pass.

[nickbattle]

This is because the trace expander turns the op argument into "mk_R(1)", rather than "mk_A`R(1)". There is another related problem here in that if you generate a record value for an argument, but the type of that record is a "struct" export, you cannot then re-construct the value as "mk_R(...)".

I think the simplest thing to do is to suppress mk_R expressions during rtace argument expansion. There are already other categories of expression that are suppressed for similar reasons - for example, and argument of "new A()" would create an object value, but its toString is not "new A()".

Naively adding a simple suppression in TraceExpander does build an Overture that passes the test above, and is capable of executing all of Paul's specifications. Unfortunately, something goes horribly wrong in the combinatorial testing unit tests (Maven), with type invariant violations. I'd better try to unpick that, in case there is something serious wrong.

[nickbattle]

OK, those errors were harmless - they were "expected" type invariant violations, though why anyone would write a test like that...

So the fix is now available in ncb/development. I'll merge it into test too, so people can try it before the release.

[nickbattle]

When enhancement #519 is implemented, all this is much simplified. The new traces component in VDMJ separates the business of type checking from the business of expanding the test values for display. So there is no particular problem in not being able to deal with "toString" values in the display.