ASCII IO format

This is essentially a linearized textural representation of PRL term data structures, with additional file magic (checksum) mechanics. Used in .prla files.

You can view the PRL term representation by set_dfmode "src".

See refiner/reflib/ascii_io_sig.ml.

Note on design

• According to Nogin:

Only things created in the interactive [proof] editor should be kept in .prlb/.prla (or maybe all interactive rules/rewrites, including the ones that have just the statements that came from .ml and have not yet been touched in the editor in any way) - there is no reason to keep a copy of the parsed .ml in there. (This will preclude a theoretical possibility of editing more than just proofs in the interactive editor, but that is probably reasonable).

• either: Keep current design of ASIIC IO, make one of the prlb file type close to the term format used by Nuprl5. Or redesign the prla format to make it close to RPN style.