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
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.
(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)))
(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))))