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

We are unshadowing non-nested lambdas only because of Apalache #1443

Open
bugarela opened this issue May 21, 2024 · 0 comments
Open

We are unshadowing non-nested lambdas only because of Apalache #1443

bugarela opened this issue May 21, 2024 · 0 comments

Comments

@bugarela
Copy link
Collaborator

Our first approach to unshadowing is quite drastic: add a scope suffix (_123 in varname_123) to all lambda parameters and let definitions. This is not ideal, as these suffix will appear on some places: like the generated TLA+ version or, now, the new nondetPicks fields.

In the unshadower improvement I'm working on, we stop unshadowing things that are not nested, which is unnecessary. However, I found that this breaks the translation to ApalacheIR in some specific cases like this:

set.filter(e => f(e)).forall(e => g(e))

because the operators: forall, exists, filter, map and mapBy are translated as bindings, so the result looks like:

∀e  ({e ∈ set): f(e)}): g(e): e.

And there is shadowing of e there, although there is no shadowing in the Quint version

This was referenced May 21, 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

No branches or pull requests

1 participant