• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
        • Fmt
        • Msg
        • Cw
        • Set-evisc-tuple
        • Set-iprint
        • Print-control
        • Read-file-into-string
        • Msgp
        • Std/io
        • Printing-to-strings
        • Evisc-tuple
        • Output-controls
        • Observation
        • *standard-co*
        • Pp-special-syms
        • Standard-oi
        • Standard-co
        • Without-evisc
        • Serialize
          • With-serialize-character
            • Unsound-read
            • Serialize-read
            • Serialize-in-books
            • Print-compressed
            • Print-legibly
            • Serialize-write
            • Set-serialize-character-system
            • Serialize-alternatives
          • Output-to-file
          • Fmt-to-comment-window
          • Character-encoding
          • Princ$
          • Open-output-channel!
          • Cw-print-base-radix
          • Set-print-case
          • Set-print-base
          • Print-object$
          • Fmx-cw
          • Print-object$+
          • Set-print-radix
          • Extend-pathname
          • Set-fmt-hard-right-margin
          • Proofs-co
          • File-write-date$
          • Set-print-base-radix
          • Print-base-p
          • *standard-oi*
          • Wof
          • File-length$
          • Fms!-lst
          • *standard-ci*
          • Write-list
          • Fmt!
          • Fms
          • Delete-file$
          • Cw!
          • Fmt-to-comment-window!
          • Fms!
          • Eviscerate-hide-terms
          • Fmt1!
          • Fmt-to-comment-window!+
          • Read-file-into-byte-array-stobj
          • Fmt1
          • Fmt-to-comment-window+
          • Cw-print-base-radix!
          • Read-file-into-character-array-stobj
          • Cw!+
          • Newline
          • Fmx
          • Cw+
          • Read-object-from-file
          • Set-fmt-soft-right-margin
          • Read-objects-from-file
          • Read-file-into-byte-list
          • Read-file-into-character-list
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Oslib
        • Std/io
        • Bridge
        • Clex
        • Tshell
        • Unsound-eval
        • Hacker
        • Startup-banner
        • Command-line
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Serialize
    • ACL2-built-ins

    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.