With-serialize-character
Control output mode for print-object$
See serialize for a discussion of ``serialization''
routines, contributed by Jared Davis for saving ACL2 objects in files for
later loading.
NOTE: To control the use of the serialize writer by the system, rather than
by the user (as discussed below), see set-serialize-character-system.
The expression (with-serialize-character char form) evaluates to the
value of form, but with the serialize-character of the state
assigned to char, which should be one of nil, #\Y, or
#\Z. We describe the effect of that assignment below. But note that if
you are doing this because of one or more specific calls of
print-object$, such as (print-object$ x channel state), then you may
wish instead to evaluate (print-object$-fn x serialize-character channel
state), in which case you will not need to use
with-serialize-character.
General forms:
(with-serialize-character nil form)
(with-serialize-character #Y form)
(with-serialize-character #Z form)
where form should evaluate to an error-triple.
You can get the current serialize-character as follows.
(get-serialize-character state)
Note that if you prefer to obtain the same behavior (as described below)
globally, rather than only within the scope of with-serialize-character,
then use set-serialize-character in a corresponding manner:
(set-serialize-character nil state)
(set-serialize-character #\Y state)
(set-serialize-character #\Z state)
In each case above, calls of print-object$ (see io) in
form will produce a readable object. In the first case, that object is
printed as one might expect at the terminal, as an ordinary Lisp s-expression.
But in the other cases, the object is printed by first laying down either
#Y or #Z (respectively) and then calling serialize-write (or
more precisely, the underlying function called by serialize-write that
prints to a stream).
Consider what happens when the ACL2 reader encounters an object produced as
described above (in the #Y or #Z case). When the object was
written, information was recorded on whether that object was a hons.
In the case of #Z, the object will be read as a hons if and only if it
was originally written as a hons. But in the case of #Y, it will never
be read as a hons. Thus, #Y and #Z will behave the same if the
original written object was not a hons, creating an object that is not a hons.
For an equivalent explanation and a bit more discussion, see serialize-read, in particular the discussion of the hons-mode. The value
:smart described there corresponds to #Z, while :never
corresponds to #Y.
