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

Scoped builder allows constructing invalid expressions applying LET/IN expressions #2517

Open
shonfeder opened this issue Apr 1, 2023 · 0 comments
Labels

Comments

@shonfeder
Copy link
Contributor

Afaik, the only support we have for something like lambda abstraction of operator in the Apalache IR is through let/in expressions like LET f(...) == ... IN f. When we need to construct an anonymous operator (e.g., in quint conversion), we get something that looks like this. However, it is not possible to apply an operator-expression of this form, as in (LET f(...) == ... IN f)(x). This has been discussed on #2483 and #2500.

I think one of the following should be done:

  1. Add support for applying operator of this form
  2. Catch and report these malformed expressions in the builder

(1) seems preferable and would make quint conversion easier, but I don't know how difficult it would be. (2) would at least lest us catch this inconvenience at the earliest opportunity, preventing an easy mistake.

WDYT @konnov and @Kukovec?

cc/ @gabrielamafra

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant