Fix syntax error on Rocq output by using a better printing system

[jrosain]

Bug fix

Closes: #52

Description

In this PR, I got rid of the non-understandable gibberish that was MappableString (and besides, that was not mappable) and replaced it with a modular & composable Printer system.

A Printer takes a PrinterConnectives (that specify how to print all possible connectives) that always has a fallback on a specified PrinterConnective (or, if unspecified, the default one). It means that a PrinterConnective can avoid defining all the connectives, and only the ones that are relevant to it.

A Printer is also composed of a PrinterAction, that defines a bunch of functions, one that is always called for every string it returns, one that is called for IDs, for bound variables, for meta variables and for types. In particular, it makes it possible to define general-purpose PrinterAction and compose it through others actions. I've added the PrinterAction that gets rid of irrelevant parentheses. I've also gotten rid of the printing of ids by default (because a PrinterAction is additive and not subtractive: it's difficult to undo something already done like printing unique indices of ids). I've still left the option with -print-id. Anyway, I think it's better this way. I've also defined the PrettyPrinter and the printer action that quotes functional names if needed.

I've also reworked Rocq's printer so that it gets rid of unwanted characters (like the @ in skolem symbols) and replaces defined constants with $... to the value we want them to have in Rocq. I've integrated Rocq compilation inside the test-suite workflow: an eligible problem gets its proof compiled in Rocq. By eligible, I mean every problem that returns valid and doesn't already outputs something. Some problems got in the no_chk folder (/ bugs_no_chk) because the proof wasn't compiling (see #56).

Typed proofs are not available through GS3, so I've designed a test but put it in the bugs_no_chk for now but it should be moved later.

I'm also pretty sure I've broken Lambdapi's output but this is work for another PR.

PR dependencies

• Fix outdated option -ocoq and modernize presearch information messages #51
• Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API #53

Test-suite update

• Added bugs/bug_52-1.p which is the original bug file of Syntax error in Rocq output due to illegal character in skolem symbols / types #52.
• Added bugs_no_chk/bug_52-2.p which has type informations.
• Added bugs/bug_52-3.p which tests for the presence of meta variables in the proof.
• Updated output of proofs/ files (less parentheses + small changes on the printing of skolemized terms).

I've also updated the run-test-suite file to rocq compile the proofs and to make its output clearer, and updated the CI script that runs the test suite to install Rocq.

[jcailler]

The following problems produces an error when trying to export the Rocq proof in inner skolemization:

• SYN325
• SYN340
• SYN341
• SYN369
• SYN947

[jrosain]

The following problems produces an error when trying to export the Rocq proof in inner skolemization:

* `SYN325`
* `SYN340`
* `SYN341`
* `SYN369`
* `SYN947`

This is actually a bug introduced by #46, but nice catch!