Improve error recoverability in ToIrListener

[bugarela]

Hello

Closes #1072, but that's not the main point.

After #1220, we go through ToIrListener even if there are parsing errors before that, which means we can now hit previously impossible scenarios such as a stack not having enough expressions.

I noticed that typing something like 1 + in the REPL was hitting a thrown error of not enough arguments in the stack, which means I was not creative enough when trying to break things in that first PR (I was using the LSP to check for errors and it is now really good at hiding thrown errors 😬).

$ quint
Quint REPL 0.14.4
Type ".exit" to exit, or ".help" for more information
>>> 1 +
node:internal/readline/emitKeypressEvents:74
            throw err;
            ^

AssertionError [ERR_ASSERTION]: popMany: too few elements in stack
    at popMany (/home/gabriela/projects/quint/quint/dist/src/parsing/ToIrListener.js:1181:25)
    ...

Now, I thought better safe then sorry, and added default "undefined" values for each component type we try to pop from stacks. Also, I removed all asserts: we don't want to throw anymore, as we have already identify errors and they will be reported, so we try to move further as much as we can.

$ quint
Quint REPL 0.14.4
Type ".exit" to exit, or ".help" for more information
>>> 1 +
syntax error: error: [QNT000] mismatched input '<EOF>' expecting {'{', 'nondet', 'val', 'def', 'pure', 'action', 'run', 'temporal', '[', 'all', 'any', 'if', '_', STRING, BOOL, INT, 'and', 'or', 'iff', 'implies', 'Set', 'List', 'Map', 'match', '-', '(', IDENTIFIER

This could be more elegant, but since @konnov is exploring a new parser, I don't want to spend too much time polishing this one right now. If we decide to keep antlr somehow, I can refactor this a bit.

• Tests added for any new code
• [-] Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• [-] Feature table on README.md updated for any listed functionality

[bugarela]

Instead of a simple undefined value, we now have something that resembles the original structure a bit more, since each stack has it's own default value.

Instead of val x = true we have val x = val y = true { true }

[thpani]

Code LGTM!

I'm not sure how I feel about the removed assertions; I find the code harder to read if invariants are not explicitly stated. I'd like to see what @konnov as to say.

[thpani]

I find the code harder to read if invariants are not explicitly stated

Or maybe we could add comments that explain that the previous assertions are enforced downstream.

[bugarela]

Code LGTM!

I'm not sure how I feel about the removed assertions; I find the code harder to read if invariants are not explicitly stated. I'd like to see what @konnov as to say.

Well, those are no longer invariants. We used to be able to assume all information was complete since we'd only ever call this code if the parser found no issues, and now we do, so this assumption is not true anymore. And yes, this new behavior makes the code more complicated because now we have to account for all these extra scenarios.

Or maybe we could add comments that explain that the previous assertions are enforced downstream.

Makes sense! I'll try to add something like this.

[konnov]

Can we replace assert with console.error? I am worried that we will run into hard-to-debug problems. If the IR has unexpected structure, we will see a message on the console at least.

[bugarela]

Can we replace assert with console.error? I am worried that we will run into hard-to-debug problems. If the IR has unexpected structure, we will see a message on the console at least.

Not really, because then users will see a bunch of logged messages on top of the parsing errors. Also, it is impossible to construct IR with a wrong structure, because of typescript types. What we might have is default values (not written by the user), which yes, can lead to hard-to-debug problems. One thing we could try to do throw errors if (the default value generators are ever called OR a previous assert would have been called) AND no parser errors were reported.

However, I think we should merge this anyway because:

1. This blocks releasing, since the current behavior is really bad (throwing on some malformed expressions)
2. We never ever seen this assertions fail when listening to proper parsed code, so it's very unlikely that we hit this problems with proper parsed code. And with non-proper code, there are much better error messages than assertions like this being already reported.

WDYT? Then, when our parser future is a bit more clear, we can work on making this safer for new iterations.

[bugarela]

There's something wrong with github, I think I had something on the other branch that made it think that this branch was merged when I merged the other one, but it was not. See https://github.com/informalsystems/quint/blob/main/quint/src/parsing/ToIrListener.ts, the asserts are still there.

[konnov]

Wow. How did it happen? I hope you did not lose your PR

[bugarela]

I don't think I can re-open this PR, but I should be able to open a new one with the same changes.

What happen was that I did merge this branch into the other in my local git in order to do manual tests with both, while I waited for reviews. I did not commit that merge, but somehow something was leaked into my actual commit (b0319f2) and now git thinks that commit is a merge commit. I tried reverting it but it's not working, I'll just make another branch + commit + PR for these changes and avoid more headaches over this. Sorry for the noise.