-
Notifications
You must be signed in to change notification settings - Fork 31
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Use the empty tuple for the unit #1406
Conversation
We had been using the empty record `{}` for the unit, but this was causing problems with conversion to TLA+. We now use the empty tuple, `()`, which is easily and type-correctly represented in TLA+ as `<<>>`.
We now test that identifiers are sanitized, that imports and instances are resolved as expected, and that the unit is represented correctly.
a742359
to
c70ae5a
Compare
This is not working with the integration with Apalache, even after the new release. I can't understand what is happening, but it seems like a direct consequences of using tuples int the ETC type checker. Before this change, we had something like:
And after the change, we get:
Which results in the error:
I'm out of ideas on how to debug this, and I have no clue where the I'll leave this open for a bit to see if anything pops up. |
This should be accounted for in https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala#L238-L250 But if quint is tying the applicand as a tuple, then the conversion should be converting it to a tuple and nothing else, as per https://github.com/informalsystems/apalache/blob/8366559116b5147a506f8162f73f161bdd81be79/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala#L573 I think I don't understand the examples you posted, because if, in
Sorry this is not working as expected! |
Maybe it would help to detail the particulars of the error case you are hitting with Apalache, because at and We are testing that variants can be parsed and converted, and this includes a converted empty tuple: https://github.com/informalsystems/quint/pull/1406/files#diff-309e4c37edc4cfff3079aded89b649280575e6b691db8e8c8ce5ba859aa6e526R240 So seeing concretely where this is failing may help. I'm sure you've checked this, but if not, sanity checking that the quint inference is all as expected can't hurt. |
I think it may be the mix of the type inference rule linked above and the way that the types builder does its type validation? And the latter can be quite tricky to unravel, unfortunately. Here's an idea: since the current way the builder is set up doesn't seem to allow constructing empty tuples (since it insists they are Seq), try adding a special case in the converter for when the |
Aaaah, it has to be it! Thanks so much for looking this up! I think I understand your suggestion, and I'll try to implement it! |
Ok, I tried it but it doesn't help. The problem is not happening at the building stage, but at the typechecking pass. I think the only way to fix this in the building stage would be to build the empty tuples with the |
I had an idea and I quite like it. I changed conversion so the empty tuple is always translated into the uninterpreted type "UNIT" (as it is defined in Variants.tla). And then, the module looks like this:
|
Ah yeah! That's perfect. I think that is the right fix! We could always introduce a distinct
or something on the quint side if we want to match that more closely. But I think this is a great approach! |
Closes #1401
The integration tests assume fixes to Apalache added in
apalache-mc/apalache#2860,
so we'll need to cut a release for that, then update the expected version here,
before the CI will pass.
CHANGELOG.md
for any new functionalityREADME.md
updated for any listed functionality