Fix handling of \values keyword

[FliegendeWurst]

Related Issue

This pull request resolves #3717.

Intended Change

Fix by always using the type for Seq, not the type of the containing class.

Plan

• Add a simple test case for usage of \values

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• There are changes to the (Java) code

Ensuring quality

• I have tested the feature as follows: a file with \values now loads a bit further (see Enhanced-for loop example with \values not loadable #3717 (comment))

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[WolframPfeifer]

@flo2702 Can you take a look here? I think you were involved at some time in the implementation of foreach loops ...

[flo2702]

I just pushed some fixes, which allow the proofs to load further. They still don't close automatically, but this may be due to errors in the spec or just the difficulty in the proofs. @FliegendeWurst Maybe you can take another look at it now.

@unp1 I removed some assert false statements in JavaDLTheory that lead to an assertion failure every time a \values expression is parsed. git blame says that you wrote that class, and I don't entirely understand what it does, so is this right?

[unp1]

Hi,

@unp1 I removed some assert false statements in JavaDLTheory that lead to an assertion failure every time a \values expression is parsed. git blame says that you wrote that class, and I don't entirely understand what it does, so is this right?

fine to remove them. The idea was more that JavaDLTheory should never be asked whether it is responsible for literals etc. But that was not a valid thought :-) and it should just return false.

[wadoon]

@FliegendeWurst @unp1 @flo2702 PR seems to 99% finish, or?

@flo2702 mentioned that some proofs are not closing, but it seems that this does not affect the test cases. This is a bad omen, and I would suggest at least a proof or test case for future regression avoidance.