Add conversion of remaining quint set operators #2451
Conversation
There was a problem hiding this comment.
It's not clear for me whether the binding we're doing is enough to support lambdas with multiple arguments. In Quint, they are unpacked, while TLA+ supports multiple quantified variables in forall and exists.
We can postpone this, of course, I'd just like to point out this scenario in case we don't have it mapped out already (either in the code or in an issue).
| @@ -44,6 +44,14 @@ class Quint(moduleData: QuintOutput) { | |||
| s"__QUINT_LAMBDA${n}" | |||
| } | |||
|
|
|||
| // benign state to generate unique variable names | |||
There was a problem hiding this comment.
Did you mean
| // benign state to generate unique variable names | |
| // begin state to generate unique variable names |
There was a problem hiding this comment.
I did mean benign, in the sense of https://www.sciencedirect.com/science/article/abs/pii/0020019088902293
the idea being that from outside of the conversion function we’re building up with this object, the state can’t interact with or track or interfere with anything.
| @@ -220,4 +231,73 @@ class TestQuintEx extends AnyFunSuite { | |||
| assert(exn.getMessage.contains( | |||
| "Input was not a valid representation of the QuintIR: too many arguments passed to binary operator forall")) | |||
| } | |||
|
|
|||
There was a problem hiding this comment.
I'm missing tests to forall and exists, specially one that tests them with multiple lambda arguments (I'm not sure if this would support that as is).
There was a problem hiding this comment.
Exists and forall were introduced in the previous PR, and you can see the teats for those on line 200/211 above.
I have totally overlooked the multi argument bindings of forall and exists, and I think of lambdas more generally! Thanks for pointing that out. I will add support for those in a follow up!
|
Thanks for the careful review and catching my oversight! |
Closes #2438
All remaining set operator are added here, with the exception of
oneOf, whichwill be addressed in #2450.
Thanks to @konnov and @bugarela for the assist on reasoning thru the less
straight forward operators,
oneOfandchooseSome.make fmt-fix(or had formatting run automatically on all files edited)./unreleased/for any new functionality