Add language extensions in the parsing of smtlib2

[Gbury]

This PR adds a new concept to the smtlib2 parser: extensions. Basically, extensions are sets of new statements that are allowed. For instance the maxsmt extension allows statements such as minimize and maximize. By default, no extension is active/allowed, and the dolmen binary will (at least for now) discourage the use of extensions, however, users of the library will be able to accept any new statement they might want to try.

Statements accepted as part of an extension basically take a list of s-expr as payload, and it is up to the users to decide what to do with them. There are two points of control of extensions for users:

• the simplest one is to define a new extension using Dolmen_std.Extensions.Smtlib2.create. Once active, such an extension will make the parser accept the corresponding statements, and these statements will appear as plain statements, annotated with a term that stores the name of the original statement, and with a single s-expr as payload (that single s-exprs wraps the list of s-exprs into a single term)
• alternatively, one can provide their own Ext module when instantiating the parser. This basically means writing a function f : string -> (term list -> statement) option. That function f is first called when the parser sees a statement (foo ...) where foo is not one of the official smtlib2 statement. If f returns None, then everything proceeds as "normal", i.e. the statement is rejected with a syntax error. If f returns Some g then g is then called with the list of parsed s-exprs as arguments. This makes it so that the parser can still generate parsing errors as early as possible on non-allowed statements.

Note: the payloads of Plain statements for extensions are s-expr, and not smtlib2 terms of sorts. The functions sexpr_as_term and sexpr_as_sort from the Dolmen_type.Core.Smtlib2 module may be used to easily recover parsed expressions that can then easily be typechecked.

cc @bclement-ocp

[bclement-ocp]

This looks reasonable and fits the needs of the Alt-Ergo team, thanks @Gbury!

The only thing I am not sure about is the Plain arg containing an s-expr of the arguments with the command name stashed away in an attribute. I would have expected the Plain arg to be the full command, because that is a term that actually appears as-is in the source.

I guess the reason you do this is so that users can distinguish statements coming from SMT extensions from other statements, but this could be done by having an attribute for the SMT extension that parsed the statement originally — this could even be useful for dispatch e.g. during typing.

[Gbury]

Okay so, I replaced the Plain statement with an Other statement which is a bit more general and should make it easier to access the original name of the statement.

Note that originally/before this PR, the only producer of Plain statements was the TPTP parser. With this PR, smtlib extensions can also produce such statements (well now it's called Other).