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.2 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2016, 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))
|
