print-objects

(in-package "ACL2")

(set-state-ok t)

(define print-legibly-aux
  :parents (print-legibly print-compressed)
  :short "Wrapper for @(see print-object$) that handles setting up @(see
serialize) compression."
  ((obj "The object to print.") (serialize-okp booleanp)
    (channel (and (symbolp channel)
        (open-output-channel-p channel :object state)))
    state)
  :returns state
  :long "<p>ACL2's @(see 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.</p>

<p>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.</p>"
  :prepwork ((local (in-theory (enable serialize-characterp))))
  (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))))
  (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)))))

(define print-legibly
  :parents (std/io print-object$ serialize)
  :short "Wrapper for @(see print-object$) that ensures @(see serialize)
compression is disabled."
  ((obj "The object to print.") &optional
    ((channel (and (symbolp channel)
         (open-output-channel-p channel :object state))
       "An open @(':output') channel.") 'channel)
    (state 'state))
  :returns state
  :long "<p>When writing to an @(':object') stream, ACL2 can print objects in a
@(see serialize)d format that provides compression when there is a lot of
structure sharing, but which is hard for humans to read.</p>

<p>Using @('print-legibly') ensures that your object will be printed without
this compression.</p>

<p>See also @(see print-compressed).</p>"
  (print-legibly-aux obj nil channel state)
  ///
  (defthm state-p1-of-print-legibly
    (let ((ret (print-legibly obj channel state)))
      (implies (and (state-p1 state)
          (symbolp channel)
          (open-output-channel-p1 channel :object state))
        (state-p1 ret))))
  (defthm open-output-channel-p1-of-print-legibly
    (let ((ret (print-legibly obj channel state)))
      (implies (and (state-p1 state)
          (symbolp channel)
          (open-output-channel-p1 channel :object state))
        (open-output-channel-p1 channel :object ret)))))

(define print-compressed
  :parents (std/io print-object$ serialize)
  :short "Wrapper for @(see print-object$) that ensures @(see serialize)
compression is enabled (if supported)."
  ((obj "The object to print.") &optional
    ((channel (and (symbolp channel)
         (open-output-channel-p channel :object state))
       "An open @(':output') channel.") 'channel)
    (state 'state))
  :returns state
  :long "<p>When writing to an @(':object') stream, ACL2 can print objects in a
@(see serialize)d format that provides compression when there is a lot of
structure sharing, but which is hard for humans to read.</p>

<p>Using @('print-compressed') ensures that, on @(see hons-enabled) versions of
ACL2 (which is all versions), your object will be printed with this compression
enabled.  The resulting object typically looks like @('#Z...') in the file,
where @('...') is a binary blob that makes no sense to humans.  These objects
can later be read back in by ACL2's @(see read-object).</p>"
  (print-legibly-aux obj t channel state)
  ///
  (defthm state-p1-of-print-compressed
    (let ((ret (print-compressed obj channel state)))
      (implies (and (state-p1 state)
          (symbolp channel)
          (open-output-channel-p1 channel :object state))
        (state-p1 ret))))
  (defthm open-output-channel-p1-of-print-compressed
    (let ((ret (print-compressed obj channel state)))
      (implies (and (state-p1 state)
          (symbolp channel)
          (open-output-channel-p1 channel :object state))
        (open-output-channel-p1 channel :object ret)))))