serialize - ACL2 Book

other

(in-package "ACL2")

serialize-writemacro

(defmacro serialize-write
  (filename obj &key verbosep)
  `(serialize-write-fn ,FILENAME ,OBJ ,VERBOSEP state))

serialize-write-fnfunction

(defun serialize-write-fn
  (filename obj verbosep state)
  (declare (xargs :guard (and (stringp filename) (booleanp verbosep))
      :stobjs state)
    (ignorable filename obj verbosep))
  (mv-let (erp val state)
    (read-acl2-oracle state)
    (declare (ignore erp val))
    state))

serialize-readmacro

(defmacro serialize-read
  (filename &key (hons-mode ':smart) verbosep)
  `(serialize-read-fn ,FILENAME ,HONS-MODE ,VERBOSEP state))

serialize-read-fnfunction

(defun serialize-read-fn
  (filename hons-mode verbosep state)
  (declare (xargs :guard (and (stringp filename)
        (member hons-mode '(:never :always :smart))
        (booleanp verbosep))
      :stobjs state)
    (ignorable filename hons-mode verbosep))
  (mv-let (erp val state)
    (read-acl2-oracle state)
    (declare (ignore erp))
    (mv val state)))

with-serialize-charactermacro

(defmacro with-serialize-character
  (val form)
  (declare (xargs :guard (member val '(nil #\Y #\Z))))
  `(state-global-let* ((serialize-character ,VAL set-serialize-character))
    ,FORM))