Quoted identifiers

[Stevendeo]

Tackles #806

[bclement-ocp]

• The list to use is: ~ ! @ $ % ^ & * _ - + = < > . ? / according to the SMT-LIB standard.
• Names that start with a digit must always be quoted
• SMT-LIB keywords must always be quoted

[Halbaroth]

We may add @Gbury to add a tag on quoted name. It makes sense that Dolmen outputs this information.

[Stevendeo]

SMT-LIB keywords must always be quoted

It does not make sens for alt-ergo to maintain the list of reserved SMTLib2 keywords for the only purpose of printing identifiers, I agree with @Halbaroth

[bclement-ocp]

To be fair we can probably just ignore the SMT-LIB keywords case, but the others are important

[Gbury]

It does not make sens for alt-ergo to maintain the list of reserved SMTLib2 keywords for the only purpose of printing identifiers, I agree with @Halbaroth

Actually yes it does, at least in my opinion, and for a few reasons, that also explain why simply tagging quoted identifiers from the source is not a good solution:

• alt-ergo can create new identifiers that it will later want to print: for those, alt-ergo must decide how to print them anyway since there can be no info coming from the source (since these do not appear in the source)
• since the function that determines how to print an identifier must exist, then why not use it for all identifiers, and save ourselves the trouble ?
• what happens when/if we one day want to have cross-formatting, for instance read a problem in tptp, and output a model in smtlib format ? Any annotation from parsing in dolmen will be useless as the lexical requirements are different. Same problem if/when we want to add a new format for models. In that case, we need the list of reserved keywords for the language in which we want to print (which may be different from the input format).
• at one point we may expect to have users of the alt-ergo library (e.g. opam ?), in which case alt-ergo might have to deal with terms that do not necessarily come from the dolmen frontend, so again, dolmen annotations on quoted identifiers would be useless.

Basically, the summary of those points is that correctly printing terms is not that easy. At one point in the future, dolmen will have printers that will abstract away most of the complexity, and that alt-ergo may or may not use (but as shown here, it's not trivial to have a correct printer). In the meantime, doing what @bclement-ocp suggests in his comment above seems like the best solution.

[Stevendeo]

I don't really want to argue about this minor issue, I just regret there is no link between the actual user input and the printable expressions. Let's go for this last solution.