Term printers

[Gbury]

Implement printers for terms in each language.

• dimacs
• iCNF
• TPTP
• Smtlib
• zf

This brings some questions that need answers:

• what to do when the term uses features not available in the output languages (higher-order terms printed in smtlib, first-order terms printed in dimacs/iCNF, ...) ?
• particularly, dimacs and iCNF are not easy to print, since they have quite a loose relation with the terms: propositional atoms expressed as integers in dimacs and iCNF are encoded using constants named #1, #2, etc... So should we just not give printer for them, or have the printer maintain a map of terms to numbered propositional atoms ?
• escaping of identifiers: constants/variables that do not respect the lexical conventions of the output language should be escaped (failing on those would be annoying). I currently have some code to do so in another project (cf https://github.com/Gbury/archsat/blob/master/src/util/escape.ml and https://github.com/Gbury/archsat/blob/master/src/output/tptp.ml#L45 ), however that code depends on unicode handling libraries (because it also escapes identifers for Coq). Currently, all languages (except maybe zf) are pretty much all-ascii, so escaping could probably be done in ascii, but that would make it difficult to add non-ascii languages (such as coq). In case unicode escaping is required, it would probably means shipping the printers in a sub-package (in which case, the build system should probably switch to dune).
• should statements also be printable ?

cc @anmaped
cc @c-cube for the unicode-related escaping question

[c-cube]

I'd say printing unicode in languages not designed for it is going to be tough. You can try "u1234" instead of the corresponding codepoint, though.

[Gbury]

To be clear, the point of escaping was precisely to not print unicode in languages that don't support it.

Basically, the idea of escaping would be to map every unicode character to a list of unicode character (kind of like a flat_map : (char -> string) -> string -> string function but unicode-aware) so that all printed identifiers exactly respect the lexical conventions of the target language.
For instance, as shown in https://github.com/Gbury/archsat/blob/master/src/output/tptp.ml#L51 , for tptp, all non ASCII alphanumeric characters would be substituted with an arbitrary allowed character, e.g. '_'.

I asked about that because, as I recall you objected to adding dependencies such as uutf and uucp, which means the printer would have to be part of a sub-package with additional dependencies.

[anmaped]

Regarding the question "should statements also be printable ?" I would say, Yes.

what to do when the term uses features not available in the output languages (higher-order terms printed in smtlib, first-order terms printed in dimacs/iCNF, ...)

To be safe, I think we should't do this translations yet unless we know that it is safe to do. If you try to prety print features in one language that are not supported you should tell to the user exactly that.

particularly, dimacs and iCNF are not easy to print, since they have quite a loose relation with the terms: propositional atoms expressed as integers in dimacs and iCNF are encoded using constants named #1, #2, etc... So should we just not give printer for them, or have the printer maintain a map of terms to numbered propositional atoms ?

For now, we may skip the print of the terms for iCNF and dimacs. Later on we may use a map as you sugested.

[anmaped]

@Gbury I will start with the pretty-printers. Do you want to provide some skeleton?

[Gbury]

I already started some work on branch printer, where there is some skeleton you can start from.

[Gbury]

This will be greatly benefit from the typed terms now that there is a type-checker. I'll upstream some code from archsat soon to cover this feature.

[Gbury]

See #211 for an implementation of printers for smtlib v2.6.