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

[] parsed incorrectly leading to unrelated error message #1468

Open
bugarela opened this issue Jul 26, 2024 · 6 comments
Open

[] parsed incorrectly leading to unrelated error message #1468

bugarela opened this issue Jul 26, 2024 · 6 comments
Labels
bug Something isn't working parser Quint parser

Comments

@bugarela
Copy link
Collaborator

Using [] like this:

module test {
  pure val foo = {
    pure val bar = 1
    [bar].concat(2)
  }
}

causes a completely unrelated error about cyclic definitions:

test.qnt:3:5 - error: [QNT099] Found cyclic declarations. Use fold and foldl instead of recursion
3:     pure val bar = 1
       ^^^^^^^^^^^^^^^^
4:     [bar].concat(2)
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: parsing failed

because this is (wrongfully) parsed as:

module test {
  pure val foo = pure val bar = field(nth(1, bar), "concat") { 2 }
}
@bugarela bugarela added bug Something isn't working parser Quint parser labels Jul 26, 2024
@bugarela
Copy link
Collaborator Author

Workaround: use List(bar) instead of [bar]

@bugarela
Copy link
Collaborator Author

I stumbled upon a similar issue while writing typescript and the autoformatter immediately made me understand I wrote something different then what I expected. I wrote

const a = foo(x)
[a, bar]

(forgetting the return keyword in the last line). As soon as I saved the file, it got formatted into

const a = foo(x)[a, bar]

which made me realize something was wrong.

@bugarela
Copy link
Collaborator Author

bugarela commented Sep 18, 2024

A similar issue was reported by @angbrav involving tuple constructors and operator calls. In this example, one tuple construction ((bar, 1)) is parsed as the parameters in a operator call, and later, one operator call (head()) is parsed as a field access + empty tuple construction. So they "cancel each other out" and form a valid module.

module test {
  pure def foo(x) =
    pure val bar = x
    (bar, 1)

  pure def foo2(x) =
    pure val baz = x.head()
    x
}

is parsed as

module test {
  pure def foo(x) =
    pure val bar = x(bar, 1)
    pure def foo2(x) =
      pure val baz = x.head { Tup() }
    x
}

@bugarela
Copy link
Collaborator Author

bugarela commented Sep 18, 2024

Wrapping the first top-level def in curly braces fixes the problem:

module test {
  pure def foo(x) = {
    pure val bar = x
    (bar, 1)
  }

  pure def foo2(x) =
    pure val baz = x.head()
    x
}

@ivan-gavran
Copy link
Contributor

I just stumbled upon a similar issue as @angbrav . I cannot create a minimal example (because I do not udnerstand what exactly is happening) so let me describe how/when the problem occurs.

  • a function that returns a tuple
  • if it just returns a tuple, all is good
  • it if has one helper val, all is good
  • if it has two helpers vals, a parsing error is reported that an existing function does not exist.
  • as soon as I wrap all in curly braces, all is good again.

Is it an instance of the same error? To the best of my understanding, any number of helper vals before a single expression should be legal syntax

@bugarela
Copy link
Collaborator Author

@ivan-gavran I'd guess not the number of vals, but the content of them. Does any of them end with a char sequence like (.*)? If yes, then it is probably the same thing I described in here

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working parser Quint parser
Projects
None yet
Development

No branches or pull requests

2 participants