Missing-functionality
Notes about some ACL2 pretty-printer settings that are not
implemented in our printconfig-p objects.
print-escape and print-readably
ACL2's take on print-readably:
- it binds print-readably to nil by default
- it offers set-print-readably
- it binds it to nil in princ$
- it consults it in needs-slashes -- along with print-escape
- it formerly marked it as untouchable
ACL2's take on print-escape
- PROVE binds it to T when #+write-arithmetic-goals... er, wtf?
- bound to t by default
- controllable with set-print-escape
- potentially important for princ$ that it be bound to nil
- consulted by needs-slashes -- along with print-readably
- bound in prin1$ to put |s on symbols
CLHS regarding print-escape:
- If false, escape characters and package prefixes are not
output when expressions are printed
- if true, an attempt is made to print an expression in such a way
that it can be read back in to produce an equal expression.
but this is only a guideline.
CLHS regarding print-readably:
- when true, special rules go into effect:
- printing any object O1 produces a printed representation that,
when seen by the Lisp reader with the standard readtable in
effect, will produce an object O2 that is SIMILAR to O1.
- printing proceeds as if *print-escape*, *print-array* and
*print-gensym* are true and as if *print-length*, *print-level*,
and *print-lines* are false.
After a lot of investigation and consideration, I don't think any of this is
anything we should care about. I can't imagine why someone would want to hide
the package names for symbols from other packages. The two options seem
perhaps entirely redundant in the context of ACL2 where there aren't arrays and
gensyms, so I don't know why ACL2 provides both. At any rate, it seems much
better to just drop this complicated nonsense and have the printer do something
reasonable by default.
write-for-read
ACL2 also has another parameter named write-for-read, which is somewhat
similar to print-readably but affects different things.
It is used in fmt-tilde-s1 to decide whether to split up symbols after
the soft margin. This can be nice for keeping the proof long word wrapped in a
nice style. However, it can be troublesome for trying to copy/paste rule
names. It's also consulted in maybe-newline, which is used in fmt code.
Functions like fmt1! and fmt! and fms! bind it to true.
None of that matters yet because, at least at the moment, I am only
implementing PPR, not FMT, and all of that is FMT-level stuff.
write-for-read also influences ACL2's spaces1 function. When
write-for-read is disabled, it prints <newline> sequences and then
continues printing spaces on the next line. I don't think this is a
"feature" that I will miss, so I am not going to implement it.
