search

informalsystems / quint

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

Improve error reporting on let-ins missing a body like `val foo = 1` #1536

Open bugarela opened 3 hours ago

bugarela commented 3 hours ago

Having this type of error on the ANTLR scope is really bad, because it is never able to provide a useful error and many times this breaks parsing of anything below the partial expression. This is a very common problem because even advanced users will write this type of partial expressions on WIP definitions, and it breaks analysis much more than it should.

The grammar should be fine in expressions like this, and then we can report a missing body in toIrListener.

bugarela commented 3 hours ago

perhaps the same for "an if always needs an else" errors