Type of record pattern not resolved

[peterwvj]

Description

The type of a record pattern in an invariant is not being resolved.

Steps to Reproduce

1. Create a file with the following content

module A

exports all
definitions 

state S of
inv mk_S() == true
init s == s = mk_S()
end 

end A

2. Type-check the model

3. Inspect the type of the record pattern (first occurence of mk_S()) in the type-checked AST.

Expected behavior: [What you expect to happen]

The type of the record pattern should be a record type.

Actual behavior: [What actually happens]

The type of the record pattern is unresolved (see attached screenshot).

Reproduces how often: [What percentage of the time does it reproduce?]

Every time.

Versions

Overture 2.6.0.
Ubuntu 17.10
OpenJDK 8, 64 bit.

Additional Information

None.

[nickbattle]

This seems to be OK on VDMJ. I'll try to track it down in Overture.

[nickbattle]

From a quick look, this appears to be (yet) another case where VDMJ works by using a reference to the same piece of AST from two or more places, and hence fixing one instance fixes them all. In Overture, you cannot duplicate pieces of AST like this - adding something to the AST in one place removes it from where it came from. These can be tricky to fix. I'll look at it more closely tomorrow.

[peterwvj]

Thanks, Nick!

[nickbattle]

So I tried adding the obvious changes to type check the copy of the record pattern, but for some reason that doesn't work. I'm still trying to understand why... and all the visitors aren't helping :-(

[nickbattle]

Of course it's about type resolution, not type checking... duh. So I just pushed a type resolve change for StateDefinitions to ncb/development. Can you give it a try?

[peterwvj]

I just tried your fix on a few examples, and it seems to do the job. Many thanks.