Write a pretty-printing library

[xrchz]

This issue is to:

• create a library for the CakeML basis above which one can write pretty-printing functions for datatypes, and,
• include some default pretty-printers for built-in datatypes (lists, options, unit/tuples, base types).

It should be possible to obtain a string from a pretty-printer, but this may not be the best underlying representation. It should also be possible to efficiently print the output of a pretty-printer (using TextIO).

[zapashcanon]

@xrchz, I can't assign myself, but I'm working on this as part of my internship.

[myreen]

@zapashcanon glad to hear that you are looking into this. I suggest you join the slack channel or IRC, if you haven't done so already.

As @xrchz mentions above, having the pretty printer produce a single string might be bad for performance (I agree). A solution could be to produce an app_list of strings, i.e. type mlstring app_list. The app_list type is defined here: https://github.com/CakeML/cakeml/blob/master/misc/miscScript.sml#L143 Such app_lists can be efficiently flattened (using the append function) and then handed to print_list: https://github.com/CakeML/cakeml/blob/master/basis/TextIOProgScript.sml#L91 Alternatively, one could define a new print_app_list function in TextIO to avoid building the intermediate list.

[xrchz]

print_app_list already exists in the basis library https://github.com/CakeML/cakeml/blob/master/basis/basisProgScript.sml#L14

[zapashcanon]

As advised in #477, I switched everything to basis/pure and used translate in basis. See this commit. (@myreen, that's why I opened a PR, it's really easier to have the code directly linked to the discussion rather than having to link it manually :-)).

Is this the correct way to go ?

EDIT:

@myreen

The functions you propose sound good in general, but I don't see the benefit of the more advanced stuff (i.e. CPS versions or balanced app_lists). If you can demonstrate a clear performance benefit, sure. If not, then keep the code simple and small.

There's no performance benefit. It will actually slow things down. The fact is that printing e.g. a big list will lead to a stack overflow. For lists this can be prevented by using a CPS. For arrays and vectors, by balancing the app_list. When I get something working, I'll write an example and try to find how big the list has to be to reach a stack overflow and how much the CPS version is slower.