Implement parsers for commands and logic formulas

[jfet97]

just test cases are missing

[jfet97]

Added a reference test, both as .sil file and as manually written ast to check against. Later we'll see what is the best way to test this stuff.

[jfet97]

@Yurand2000 @Alex23087 I would say this branch is good as it is, further tests can be added later. Please have a look, but avoid blocking the merge of this branch for things of secondary importance. Let's try to move forward as there's a lot of stuff still to do

[Yurand2000]

It is not in our interests to halt the progress of the project and as reviewers we will assess that your production meets quality criteria, as it is normal procedure for any code that has been and will be merged into the codebase.

[jfet97]

Why do we have two lexers? Why are there duplicate tokens for the two parsers? A single lexer is enough.

Now we have just one lexer, no more duplicated tokens.

As an advice I would use Hashtbl.find_opt to avoid using exceptions where possible

Advice accepted.

Refactor tokens so that they are specified in a separate file, to avoid cluttering the parser file.

Now we do not have duplicated tokens anymore, so the tokens are less and they do not need to be taken elsewhere.

The top_level rule returns either a formula or a command, thus use the Either type instead of returning the formula inside a skip command.

Done.

why are there two rules to parse atomic commands and their respective formulas? isn't there an optional construct in menhir? do they need to be treated this way to solve skip/reduce conflicts?

Yes, there are shift/reduce and reduce/reduce conflicts. Optional is not the solution. The main idea is to forbid sub-commands with formulae. To have them you have to use braces to delimit sub-commands, but generally they won't be needed. Just a formula for each top level command is more than enough.

where is the NONDET token parsed? is the non deterministic assignment parseable?

Now it is.

there is no parsing of if and while constructs, that are to be translated into nondet choices and star regular commands.

Done.

parsing of existential formulas, the grammar is: exists VARIABLE . FORMULA. You are missing the dot that separates the variable to the formula.

Corrected.

toplevel_command_nof ? what does that even mean? Explicit names would help.

Renamed.

the syntax/code style is not uniform across the same file.

Did my best to solve.

I've been looking at the test file with some grammar, it is really ugly to read formulas side by side to commands. Should we consider forcing the formulas to be on the next line of the command they refer to? Is there a better way to annotate the code?

I don't care too much about the beauty of the language for commands. If you want, you can add a newline. It's not mandatory and there is no reason to force it. It's a language that still has everything necessary for our purposes.

More tests are definitely needed, to assert that we can really parse every construct in the correct way.

We need a volunteer.

We can skip testing for correct positions in both commands' and formulas' annotations.

It's the simplest thing to do, because the parser returns an ast with those info as annotations, so an equal check just does the job. But we can discuss about that.