/usr/share/acl2-6.3/books/tools/clone-stobj.lisp is in acl2-books-source 6.3-5.
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 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 | ; Tool for defining stobj/absstobjs congruent to existing ones
; Copyright (C) 2013 Centaur Technology
;
; Contact:
; Centaur Technology Formal Verification Group
; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
; http://www.centtech.com/
;
; This program is free software; you can redistribute it and/or modify it under
; the terms of the GNU General Public License as published by the Free Software
; Foundation; either version 2 of the License, or (at your option) any later
; version. 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 GNU General Public License for
; more details. You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free Software
; Foundation, Inc., 51 Franklin Street, Suite 500, Boston, MA 02110-1335, USA.
;
; Original author: Sol Swords <sswords@centtech.com>
(in-package "ACL2")
(include-book "bstar")
(include-book "rulesets")
(include-book "templates")
(include-book "xdoc/top" :dir :system)
(program)
(defun clone-stobj-change-symbol (sym renaming)
(if renaming
(b* (((list prefix suffix strsubst pkg) renaming)
((mv sub pkg?) (tmpl-str-sublis strsubst (symbol-name sym))))
(intern-in-package-of-symbol
(concatenate 'string prefix sub suffix)
(or pkg? pkg)))
sym))
(defun clone-stobj-process-rename-alist (rename-alist renaming)
(if (atom rename-alist)
nil
(cons (cons (clone-stobj-change-symbol (caar rename-alist) renaming)
(clone-stobj-change-symbol (cdar rename-alist) renaming))
(clone-stobj-process-rename-alist (cdr rename-alist) renaming))))
(defun clone-stobj-process-fields (fields renaming)
(if (atom fields)
nil
(cons (if (consp (car fields))
(cons (clone-stobj-change-symbol (caar fields) renaming)
(cdar fields))
(clone-stobj-change-symbol (car fields) renaming))
(clone-stobj-process-fields (cdr fields) renaming))))
(defun keep-nonbool-symbols (x)
(if (atom x)
nil
(let* ((k (car x)))
(if (and k (not (eq k t)) (symbolp k))
(cons k (keep-nonbool-symbols (cdr x)))
(keep-nonbool-symbols (cdr x))))))
;; each field is: (fieldp type initial-val others)
;; and others are all either function names, NIL when the functions aren't
;; applicable, and a resizable flag (boolean).
(defun stobj-field-template-fnnames (field-templates)
(if (atom field-templates)
nil
(cons (caar field-templates)
(append
(keep-nonbool-symbols (cdddar field-templates))
(stobj-field-template-fnnames (cdr field-templates))))))
(defun stobj-template-fnnames (template)
(list* (car template) ;; stobjp
(cadr template) ;; create-stobj
;; field fns
(stobj-field-template-fnnames (caddr template))))
(defun clone-stobj-process-args (stobjname args renaming)
(b* (((mv erp field-descriptors key-alist)
(partition-rest-and-keyword-args args *defstobj-keywords*))
((when erp)
(er hard? 'defstobj-clone
"The stobj to be cloned had bad keyword args~%"))
(rename-alist (cdr (assoc-eq :renaming key-alist)))
(new-renaming (clone-stobj-process-rename-alist rename-alist renaming))
(inline (assoc-eq :inline key-alist))
(fields (clone-stobj-process-fields field-descriptors renaming)))
(append fields
(and renaming (list :renaming new-renaming))
(and inline (list :inline (cdr inline)))
(list :doc
(concatenate 'string "Clone of stobj "
(symbol-name stobjname))
:congruent-to stobjname))))
(defun clone-stobj-rewrite (newfn oldfn formals)
(let ((thmname (intern-in-package-of-symbol
(concatenate 'string (symbol-name newfn) "-IS-" (symbol-name oldfn))
newfn)))
`((defthm ,thmname
(equal (,newfn . ,formals)
(,oldfn . ,formals))
:hints (("goal" :in-theory '(,newfn ,oldfn))
(and stable-under-simplificationp
'(:in-theory (e/d** (clone-stobj-tmp-rules))))
(and stable-under-simplificationp
'(:in-theory '(,newfn ,oldfn (:induction ,newfn))))))
(local (add-to-ruleset! clone-stobj-tmp-rules ,thmname)))))
;; new and old are the lists of axiomatic defs
(defun clone-stobj-rewrites (new old)
(b* (((when (atom new)) nil)
(newfn (caar new))
(formals (cadar new))
(oldfn (caar old)))
(append (clone-stobj-rewrite newfn oldfn formals)
(clone-stobj-rewrites (cdr new) (cdr old)))))
(defun clone-base-stobj-fn (stobjname name renaming wrld)
(b* ((ev-wrld (decode-logical-name stobjname wrld))
((when (null ev-wrld))
(er hard? 'defstobj-clone
"Unrecognized stobjname: ~x0~%" stobjname))
(event (access-event-tuple-form (cddar ev-wrld)))
((when (not (eq (car event) 'defstobj)))
(er hard? 'defstobj-clone
"The event named ~x0 is not a defstobj event~%" stobjname))
((list* & ;; defstobj
& ;; stobjname
args) event)
(name (or name (clone-stobj-change-symbol stobjname renaming)))
(new-args (clone-stobj-process-args stobjname args renaming))
(old-template (defstobj-template stobjname args wrld))
(new-template (defstobj-template name new-args wrld))
(old-defs (defstobj-axiomatic-defs stobjname old-template wrld))
(new-defs (defstobj-axiomatic-defs name new-template wrld)))
(list* 'encapsulate nil `(defstobj ,name . ,new-args)
'(local (def-ruleset! clone-stobj-tmp-rules nil))
(clone-stobj-rewrites new-defs old-defs))))
(defun clone-absstobj-exports (exports logic-exec renaming concrete world)
(b* (((when (atom exports)) nil)
((cons logic exec) (car logic-exec))
(new-sym (clone-stobj-change-symbol (car exports) renaming))
(protect (unprotected-export-p concrete exec world)))
(cons `(,new-sym :logic ,logic :exec ,exec :protect ,protect)
(clone-absstobj-exports
(cdr exports) (cdr logic-exec) renaming concrete world))))
(defun clone-absstobj-fn (stobjname name renaming user-exports world)
(b* ((abs-info (fgetprop stobjname 'absstobj-info nil world))
(stobj-info (fgetprop stobjname 'stobj nil world))
(`(,concrete
(,recog-logic . ,recog-exec)
(,create-logic . ,create-exec)
. ,export-logic-exec)
abs-info)
(`(,& ,?pred ,?create . ,exports) stobj-info)
(exports (or user-exports exports))
(creator (defstobj-fnname name :creator :top nil))
(recognizer (defstobj-fnname name :recognizer :top nil)))
`(defabsstobj ,name
:concrete ,concrete
:recognizer (,recognizer :logic ,recog-logic :exec ,recog-exec)
:creator (,creator :logic ,create-logic :exec ,create-exec)
:exports ,(clone-absstobj-exports exports export-logic-exec renaming
;; needed for computing :protect args
concrete world)
:congruent-to ,stobjname)))
(defun clone-stobj-fn (stobjname name prefix suffix strsubst pkg exports world)
(declare (xargs :guard (and (stringp prefix)
(stringp suffix)
(alistp strsubst)
(string-listp (strip-cars strsubst))
(string-listp (strip-cdrs strsubst))
(symbol-listp exports)
(not (and (equal prefix "")
(equal suffix "")
(not strsubst)
(not exports))))))
(b* ((stobjp (fgetprop stobjname 'stobj nil world))
(absstobjp (fgetprop stobjname 'absstobj-info nil world))
(pkg (or pkg name))
;; don't rename if exports are provided
(renaming (and (not exports)
(list prefix suffix strsubst pkg)))
((unless stobjp)
(er hard? 'defstobj-clone
"~x0 is not a stobj~%" stobjname)))
(if absstobjp
(clone-absstobj-fn stobjname name renaming exports world)
(if exports
(er hard? 'defstobj-clone
":Exports is not supported for concrete stobjs")
(clone-base-stobj-fn stobjname name renaming world)))))
(defmacro defstobj-clone (newname origname &key
strsubst
(prefix '"")
(suffix '"")
pkg
exports)
`(make-event (clone-stobj-fn ',origname ',newname ',prefix ',suffix
',strsubst ',pkg ',exports (w state))))
(defxdoc defstobj-clone
:parents (stobjs)
:short "Create a new stobj that is congruent to an existing (concrete or
abstract) stobj"
:long "
<h2>Usage:</h2>
@({
(defstobj-clone new-stobj orig-stobj
:strsubst ((\"OLDSTR\" . \"NEWSTR\")
(\"ETC\" . \"ANDSOON\"))
:prefix \"NEW\"
:suffix \"++\"
:pkg mypkg::some-symbol
;; Only supported for abstract stobjs
:exports (new-get new-set new-acc new-upd))
})
<p>This defines a new stobj called @('NEW-STOBJ') that is congruent to the
existing stobj @('ORIG-STOBJ'). The keyword arguments all have to do with the
way the fields and accessor/updater functions of stobjs are renamed (they must
be given new names in the new stobj).</p>
<p>For an abstract stobj, the accessors/updaters are known as \"exports\". One
option for specifying their names in the new stobj is to provide the
@(':exports') argument, which should be a list of symbols corresponding to the
exported functions from the original abstract stobj. When this is provided,
the other keyword arguments are unused.</p>
<p>If @(':exports') is not used (which it can't be in cloning a concrete
stobj), then one or more of @(':strsubst'), @(':prefix'), and @(':suffix') must
be given. Prefix and suffix should be strings, and strsubst should be an alist
with string keys and values. The @(':pkg') symbol is optional and determines
into what package new symbols are interned; by default, it is the package of
the new stobj name.</p>")
|