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

Recursion check in operator definitions #171

Closed
bugarela opened this issue Aug 22, 2022 · 4 comments
Closed

Recursion check in operator definitions #171

bugarela opened this issue Aug 22, 2022 · 4 comments
Assignees
Labels
effort-easy Can be completed within about 1 day impact-medium Medium impact parser Quint parser usability Usability issues

Comments

@bugarela
Copy link
Collaborator

As recursion is not allowed, we should detect recursion in operator and lambda definitions to report them as unsupported. This should be a simple occurs check of the operator's name in its body.

@bugarela bugarela self-assigned this Aug 22, 2022
@bugarela bugarela added the typechecker Type checker for Quint label Aug 22, 2022
@bugarela bugarela added this to the T1.3.2 Type System milestone Aug 22, 2022
@bugarela
Copy link
Collaborator Author

bugarela commented Sep 1, 2022

We should probably do it before type checking.

Maybe correlates with #129 and #177

@bugarela bugarela added impact-medium Medium impact effort-easy Can be completed within about 1 day labels Nov 30, 2022
@konnov konnov added the usability Usability issues label Feb 17, 2023
@konnov
Copy link
Contributor

konnov commented Feb 17, 2023

I just ran into this issue by typing a wrong name and introducing infinite recursion. The plugin feedback was too complex for me to understand. It would be great to have this fixed :)

@bugarela
Copy link
Collaborator Author

bugarela commented Mar 3, 2023

Minimal example:

module foo {
  val a = a
}

I'll wait until the refactor of the lookup system to fix this because this depends too much on it and I will have to completely re-do the check when it changes.

@konnov
Copy link
Contributor

konnov commented Jul 4, 2023

Handled by #1008, including the MWE

@konnov konnov closed this as completed Jul 4, 2023
@konnov konnov assigned konnov and unassigned bugarela Jul 4, 2023
@konnov konnov added parser Quint parser and removed typechecker Type checker for Quint labels Jul 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
effort-easy Can be completed within about 1 day impact-medium Medium impact parser Quint parser usability Usability issues
Projects
None yet
Development

No branches or pull requests

2 participants