Skip to content
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

Handle quint quantified variables #2873

Merged
merged 6 commits into from
Mar 25, 2024

Conversation

bugarela
Copy link
Collaborator

@bugarela bugarela commented Mar 25, 2024

Hello :octocat:

This PR fixes a problem related to informalsystems/quint#1398. Imagine the following type:

type Option[a] = Some(a) | None

Quint generates two constructors for this type:

pure def Some(__SomeParam: a): Option[a]
pure def None(__NoneParam: ()): Option[a]

In those types, a is a quantified type variable, and the type scheme in the quint map, for both constructors, will have a in the typeVariables set, which represents quantified type variables in that type scheme.

So far, we've been ignoring those fields in apalache. But, since a has the same type name here between the two definitions, this is a problem. Our type converter will generate the same TlaType1 type number for both of them, and this will result in type issues inside Apalache.

In this PR, I add a simple fix to remove quantified variables names from the map that provides same TlaType1 type numbers to the same names, everytime we finish converting an OpDef. This is enough, since quint variables are only quantified in OpDefs.

I'm also reverting our original attempt to address related issues, as that was not the appropriate fix, and after informalsystems/quint#1409 it doens't have any effect.

  • Tests added for any new code
  • Ran make fmt-fix (or had formatting run automatically on all files edited)
  • Documentation added for any new functionality
  • Entries added to ./unreleased/ for any new functionality

@codecov-commenter
Copy link

codecov-commenter commented Mar 25, 2024

Codecov Report

Attention: Patch coverage is 90.00000% with 1 lines in your changes are missing coverage. Please review.

Project coverage is 78.88%. Comparing base (27f1885) to head (8844f46).

Files Patch % Lines
...ain/scala/at/forsyte/apalache/io/quint/Quint.scala 87.50% 1 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##             main    #2873      +/-   ##
==========================================
- Coverage   78.88%   78.88%   -0.01%     
==========================================
  Files         467      467              
  Lines       15966    15966              
  Branches     2577     2593      +16     
==========================================
- Hits        12595    12594       -1     
- Misses       3371     3372       +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@bugarela bugarela merged commit 735f95d into main Mar 25, 2024
10 checks passed
@apalache-bot apalache-bot mentioned this pull request Mar 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants