informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
807 stars 31 forks source link

`[]` parsed incorrectly leading to unrelated error message #1468

Open bugarela opened 2 months ago

bugarela commented 2 months ago

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 commented 2 months ago

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

bugarela commented 1 month ago

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 commented 3 weeks ago

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 commented 3 weeks ago

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 commented 3 weeks ago

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.

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 commented 3 weeks ago

@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