WITH-SERIALIZE-CHARACTER

Major Section:  SERIALIZE

This documentation topic relates to an experimental extension of ACL2 that supports hons, memoization, and fast alists. See hons-and-memoization. See serialize for a discussion of ``serialization'' routines, contributed by Jared Davis for saving ACL2 objects in files for later loading.

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$-ser x serialize-character channel state), in which case you will not need to use with-serialize-character. (Note however that serialize-character is treated as nil for other than a HONS version.)

General forms:
(with-serialize-character nil form)
(with-serialize-character #Y form)
(with-serialize-character #Z form)

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 an object that can be read by the HONS version of ACL2. 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 (as indicated) 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.