		Search-engine friendly clone of the ACL2 documentation.

Print-legibly-aux

Wrapper for print-object$ that handles setting up serialize compression.

Signature
(print-legibly-aux obj serialize-okp channel state) → state
Arguments: obj — The object to print.; serialize-okp — Guard (booleanp serialize-okp).; channel — Guard (and (symbolp channel) (open-output-channel-p channel :object state)) .

ACL2's print-object$ is hard to use directly in logic mode because the serialize-character interface is pretty baroque. We can only set the serialize character to particular good values. But nothing tells us it's a good value to begin with, and the with-serialize-character macro tries to restore it to whatever it was, which might be a bad value.

At any rate, this is a wrapper that works around these issues by setting the serialize character to something sensible if it's invalid to begin with, and by not trying to serialize in a non-hons enabled image.

Definitions and Theorems

Function: print-legibly-aux

(defun print-legibly-aux (obj serialize-okp channel state)
 (declare (xargs :stobjs (state)))
 (declare
   (xargs :guard (and (booleanp serialize-okp)
                      (and (symbolp channel)
                           (open-output-channel-p channel
                                                  :object state)))))
 (let ((__function__ 'print-legibly-aux))
  (declare (ignorable __function__))
  (b*
   ((state
      (if
        (and (boundp-global 'serialize-character
                            state)
             (serialize-characterp (get-serialize-character state)))
        state
        (set-serialize-character nil state)))
    ((mv err ?val state)
     (if serialize-okp
         (with-serialize-character
              #\Z
              (let ((state (print-object$ obj channel state)))
                (mv nil nil state)))
       (with-serialize-character
            nil
            (let ((state (print-object$ obj channel state)))
              (mv nil nil state)))))
    ((when err) (impossible) state))
   state)))

Theorem: state-p1-of-print-legibly-aux

(defthm state-p1-of-print-legibly-aux
  (let ((ret (print-legibly-aux obj serialize-okp channel state)))
    (implies (and (state-p1 state)
                  (symbolp channel)
                  (open-output-channel-p1 channel
                                          :object state))
             (state-p1 ret))))

Theorem: open-output-channel-p1-of-print-legibly-aux

(defthm open-output-channel-p1-of-print-legibly-aux
  (let ((ret (print-legibly-aux obj serialize-okp channel state)))
    (implies (and (state-p1 state)
                  (symbolp channel)
                  (open-output-channel-p1 channel
                                          :object state))
             (open-output-channel-p1 channel
                                     :object ret))))