/usr/share/acl2-7.1/serialize.lisp is in acl2-source 7.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 | ; ACL2 Version 7.1 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2015, Regents of the University of Texas
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTE-2-0.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the LICENSE file distributed with ACL2.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; LICENSE for more details.
; Regarding authorship of ACL2 in general:
; Written by: Matt Kaufmann and J Strother Moore
; email: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
; serialize.lisp -- logical definitions for "serialization" routines,
; i.e., saving ACL2 objects in files for later loading
; This file was developed and contributed by Jared Davis on behalf of
; Centaur Technology.
; Note: The serialization routines are restricted to work only in
; ACL2(h). However, they are independent of the remainder of the HONS
; extension and might some day become part of ordinary ACL2.
; Please direct correspondence about this file to Jared Davis
; <jared@centtech.com>.
(in-package "ACL2")
(defmacro serialize-write (filename obj &key verbosep)
`(serialize-write-fn ,filename ,obj ,verbosep state))
(defun serialize-write-fn (filename obj verbosep state)
(declare (xargs :guard (and (stringp filename)
(booleanp verbosep)
(state-p state))
:stobjs state)
(ignorable filename obj verbosep))
#-acl2-loop-only
(cond
((live-state-p state)
#-hons
(er hard? 'serialize-write-fn
"Serialization routines are currently only available in the HONS ~
version of ACL2.")
#+hons
(with-open-file
(stream filename
:direction :output
:if-exists :supersede)
(let* ((*ser-verbose* verbosep))
(ser-encode-to-stream obj stream)))
(return-from serialize-write-fn state))
(t
; We fall through to the logic code if we are doing a proof, where
; *hard-error-returns-nilp* is true. Otherwise, we throw here with an error
; message.
(er hard? 'serialize-write-fn "Serialization requires a live state.")))
(mv-let (erp val state)
(read-acl2-oracle state)
(declare (ignore erp val))
state))
(defmacro serialize-read (filename &key
(hons-mode ':smart)
verbosep)
`(serialize-read-fn ,filename ,hons-mode ,verbosep state))
(defun serialize-read-fn (filename hons-mode verbosep state)
; This function returns a single object.
(declare (xargs :guard (and (stringp filename)
(member hons-mode '(:never :always :smart))
(booleanp verbosep)
(state-p state))
:stobjs state)
(ignorable filename hons-mode verbosep))
#-acl2-loop-only
(cond
((live-state-p state)
(return-from
serialize-read-fn
#-hons
(progn (er hard? 'serialize-read-fn
"Serialization routines are currently only available in the ~
HONS version of ACL2.")
(mv nil state))
#+hons
(with-open-file
(stream filename :direction :input)
(let* ((*ser-verbose* verbosep)
(val (ser-decode-from-stream t hons-mode stream)))
(mv val state)))))
(t
; We fall through to the logic code if we are doing a proof, where
; *hard-error-returns-nilp* is true. Otherwise, we throw here with an error
; message.
(er hard? 'serialize-read-fn "Serialization requires a live state.")))
(mv-let (erp val state)
(read-acl2-oracle state)
(declare (ignore erp))
(mv val state)))
(defmacro with-serialize-character (val form)
(declare (xargs :guard (member val '(nil #\Y #\Z))))
`(state-global-let*
((serialize-character ,val set-serialize-character))
,form))
|