-
-
Notifications
You must be signed in to change notification settings - Fork 40
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 single typevar map for entire spec #2629
Conversation
5fe1cee
to
2818928
Compare
Codecov Report
@@ Coverage Diff @@
## th/refactor-quint #2629 +/- ##
=====================================================
- Coverage 78.49% 78.49% -0.01%
=====================================================
Files 447 447
Lines 15654 15653 -1
Branches 2553 2544 -9
=====================================================
- Hits 12288 12287 -1
Misses 3366 3366
... and 3 files with indirect coverage changes 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
2818928
to
ecfea24
Compare
ecfea24
to
22df786
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!
* QuintTypeConverter.getVarNo() for details). | ||
*/ | ||
object QuintTypeConverter { | ||
def apply(quintType: QuintType): TlaType1 = new QuintTypeConverter().convert(quintType) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good catch! I can see how the companion object was creating a new instance every time
Use a single type converter for an entire quint spec.
We previously used one type converter per sub-expression. This re-initialized the map for translating Quint type variables (named) to Apalache TypeSystem 1 type variables (numbered), causing wrong type annotations. For example the type of the following Quint was translated as
(a,a) => {src: a, ts: a}
.Tests added for any new codemake fmt-fix
(or had formatting run automatically on all files edited)Documentation added for any new functionality./unreleased/
for any new functionality