Make sure that what is printed in the smtml format is parseable

[hra687261]

The purpose of this PR is to make reproducing errors/bugs/issues easier, it is related to OCamlPro/owi#631, and the idea is to make sure that when we print smtml queries (in its AST) we can parse back the same thing and rerun it through smtml. It is currently not the case.

This PR:

• Replaces some Formats with Fmts
• Renames Expr.pp_smt to Expr.pp_smtml (since it prints in the smtml format not smt, the name is now less ambiguous and the doc is updated)
• Adds a to-smtml which simply uses Expr.pp_smtml to print the parsed/typed content of a .smtml file, I only added this command for testing purposes, I don't think it would be useful for something else (other than potentially formatting but the current output is not particularly well formatted anyway) so I can remove it if you want me to.
• When signed operations are printed "_s" is added to them, but when they are parsed, they are expected to not have the "_s" eg. < over integers is parsed "int.lt" and printed as "int.ls_s". I made the simplest/laziest change which consists in making it possible to parse both the operation with and without "_s" when it is signed and it seems to work. (I am open to better/cleaner solutions)
• removes commas between printed asserts in the smtml format since they are not used in it.

Can be tested with dune exec -- smtml to-smtml test/cli/smtml/test_lia.smtml > out.smtml and then running smtml on out.smtml, which works with bbd38bf and 85121a3 and doesn't without them.

[filipeom]

Thank you so much for this! I've been kinda neglecting the smtml format as we can parse smt-lib. But since we don't have a Smtml.Expr.t -> smt-lib yet this is very helpful! Thanks!

[hra687261]

For Smtml.Expr.t -> smt-lib, the next version of dolmen will have printers, it might help but I am not sure, we may not want to translate smtml's AST to print it.
Either way, I think it is good to have such printers as a way to to see what smtml's AST actually looks like (although I think with the smart-constructors there are some simplifications that are done but it is still useful), since it is a bit different from smt-lib.

[filipeom]

For Smtml.Expr.t -> smt-lib, the next version of dolmen will have printers, it might help but I am not sure, we may not want to translate smtml's AST to print it.

Yeah, we'll see what is best. I have to do a Smtml.Expr.t -> smt-lib printer in the very near future because of some synthesis work we're doing so I will probably just hammer something to get it to work.

Either way, I think it is good to have such printers as a way to to see what smtml's AST > actually looks like (although I think with the smart-constructors there are some simplifications that are done but it is still useful), since it is a bit different from smt-lib.

Yeah I think so too! Thanks for the patch!

[filipeom]

I still want to do a couple more things in smtml this week, so this will be included in the next week's smtml monday release