/usr/share/acl2-7.2dfsg/books/misc/redef-pkg.lisp is in acl2-books-source 7.2dfsg-3.
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 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 | ; Redef-pkg: UNSOUND Support for package redefinition.
; Matt Kaufmann and Jun Sawada, November, 2009
; While unsound in principle, redef-pkg can be useful during interactive
; sessions. Usage is just defpkg usage -- defpkg is modified by including
; this book, or in raw-mode you can submit
; (redef-pkg name imports &optional doc book-path)
; where doc and book-path are ignored.
; Certify with:
; (certify-book "redef-pkg" 0 t :ttags (:redef-pkg))
; KNOWN FLAWS:
; - During the redefinition of the package, each imported symbol whose name was
; already interned into the package must first be uninterned, so that the
; imported symbol and the symbol with that name in the package can become one
; and the same. This can cause an ugly error message when printing the
; function definitions using the uninterned symbols. A warning will alert
; the user to most cases of this, but it's still unfortunate. Example log:
; ACL2 !>(defpkg "TEST" '(cons car defun))
;
; Summary
; Form: ( DEFPKG "TEST" ...)
; Rules: NIL
; Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
; "TEST"
; ACL2 !>(in-package "TEST")
; "TEST"
; TEST !>(defun foo (x) (cons x x))
;
; Since FOO is non-recursive, its admission is trivial. We observe that
; the type of FOO is described by the theorem (COMMON-LISP::CONSP (FOO X)).
; We used primitive type reasoning.
;
; Summary
; Form: ( DEFUN FOO ...)
; Rules: ((:FAKE-RUNE-FOR-TYPE-SET COMMON-LISP::NIL))
; Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
; FOO
; TEST !>(acl2::in-package "ACL2")
; "ACL2"
; ACL2 !>(include-book "misc/redef-pkg" :dir :system)
;
; TTAG NOTE (for included book): Adding ttag :REDEF-PKG from book /Users/kaufmann/acl2/devel/books/misc/redef-pkg.
;
; ACL2 Warning [Ttags] in ( INCLUDE-BOOK "misc/redef-pkg" ...): The
; ttag note just printed to the terminal indicates a modification to
; ACL2. To avoid this warning, supply an explicit :TTAGS argument when
; including the book "/Users/kaufmann/acl2/devel/books/misc/redef-pkg".
;
;
; Summary
; Form: ( INCLUDE-BOOK "misc/redef-pkg" ...)
; Rules: NIL
; Warnings: Ttags
; Time: 0.06 seconds (prove: 0.00, print: 0.00, other: 0.06)
; "/Users/kaufmann/acl2/devel/books/misc/redef-pkg.lisp"
; ACL2 !>(defpkg "TEST" '(cons car defun foo))
;
; Executing the redefined chk-acceptable-defpkg
;
; NOTE: Added the following list of symbols to package "TEST":
; (FOO)
; and deleted the following list of symbols:
; NIL
;
;
; ACL2 Warning [Package] in SET-IMPORTED-SYMBOLS-TO-PKG: The symbol
; with name "FOO" imported into the "TEST" package may cause problems,
; since it already has properties in the ACL2 world.
;
;
; The event ( DEFPKG "TEST" ...) is redundant. See :DOC redundant-events.
;
; Summary
; Form: ( DEFPKG "TEST" ...)
; Rules: NIL
; Warnings: Package
; Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
; :REDUNDANT
; ACL2 !>:pbt 0
; 0 (EXIT-BOOT-STRAP-MODE)
; 1 (DEFPKG "TEST" '#)
; L 2
; ***********************************************
; ************ ABORTING from raw Lisp ***********
; Error: The symbol FOO, which has no package, was encountered
; by ACL2. This is an inconsistent state of affairs, one that
; may have arisen by undoing a defpkg but holding onto a symbol
; in the package being flushed, contrary to warnings printed.
;
; ***********************************************
;
; The message above might explain the error. If not, and
; if you didn't cause an explicit interrupt (Control-C),
; then the root cause may be call of a :program mode
; function that has the wrong guard specified, or even no
; guard specified (i.e., an implicit guard of t).
; See :DOC guards.
;
; To enable breaks into the debugger (also see :DOC acl2-customization):
; (SET-DEBUGGER-ENABLE T)
; ACL2 !>
(in-package "ACL2")
(defttag :redef-pkg)
; Don't use this in a theorem! See setting of program-fns-with-raw-code,
; below.
(defun set-imported-symbols-to-pkg (imports name)
(declare (ignore imports name)
(xargs :guard t :mode :program))
nil)
(defmacro redef-pkg (name imports &optional doc book-path)
(declare (ignore doc book-path))
`(set-imported-symbols-to-pkg ,imports ,name))
(progn!
(set-raw-mode-on state)
(f-put-global 'program-fns-with-raw-code
(add-to-set-eq 'set-imported-symbols-to-pkg
(f-get-global 'program-fns-with-raw-code
*the-live-state*))
*the-live-state*)
; Redefine set-imported-symbols-to-pkg.
(defun set-imported-symbols-to-pkg (syms pkg &aux (state *the-live-state*))
(let ((pkg-entry0 (assoc-equal pkg *ever-known-package-alist*))
(pkg-entry1 (assoc-equal pkg (known-package-alist *the-live-state*)))
(syms (if (symbolp syms) (list syms) syms)))
(when (or (null pkg-entry0)
(null pkg-entry1))
(error "Uknown pkg, ~s" pkg))
(when (not (symbol-listp syms))
(error "Not a symbol-listp: ~s" syms))
(let ((imports0 (package-entry-imports pkg-entry0))
(imports1 (package-entry-imports pkg-entry1))
ans)
(when (not (or (equal imports0 imports1)
(and (subsetp-eq imports0 imports1)
(subsetp-eq imports1 imports0))))
(error "SURPRISE! Different import lists. Hmmmm......"))
(let* ((new (set-difference-eq syms imports0))
(deleted (set-difference-eq imports0 syms))
(sorted-symbols (sort-symbol-listp syms)))
(setf (package-entry-imports
(assoc-equal pkg *ever-known-package-alist*))
sorted-symbols)
(setf (package-entry-imports
(assoc-equal pkg (known-package-alist *the-live-state*)))
sorted-symbols)
(dolist (sym new)
(let ((temp (find-symbol (symbol-name sym) pkg)))
(when temp
(when (get temp *current-acl2-world-key*)
(push (symbol-name temp) ans))
(unintern temp pkg))))
(fms "NOTE: Added this list of symbols to the imports of package ~
~x0:~| ~x1~|and deleted this list of symbols from the imports ~
of package ~x0:~| ~x2~|~%"
(list (cons #\0 pkg)
(cons #\1 new)
(cons #\2 deleted))
(standard-co state) state nil)
(when ans
(warning$ 'set-imported-symbols-to-pkg "Package"
"The symbol~#0~[ with name~/s with names~] ~&0 imported ~
into the ~x1 package may cause problems, since ~#0~[it ~
already has~/they already have~] properties in the ~
ACL2 world."
ans pkg))
(import new pkg)
(dolist (sym deleted)
(unintern sym pkg))))))
; WARNING! Update this if ACL2's def. of the following changes.
; (books/hacking/ has some sort of pattern-matching way to redefine functions
; that might be more robust.)
(defun chk-acceptable-defpkg (name form defpkg-book-path hidden-p ctx w state)
; We return an error triple. The non-error value is either 'redundant or a
; triple (tform value . package-entry), where tform and value are a translated
; form and its value, and either package-entry is nil in the case that no
; package with name name has been seen, or else is an existing entry for name
; in known-package-alist with field hidden-p=t (see the Essay on Hidden
; Packages).
;;; Start new code
(fms "Executing the redefined chk-acceptable-defpkg~%" nil
(standard-co state) state nil)
;;; End new code
(let ((package-entry
(and (not (global-val 'boot-strap-flg w))
(find-package-entry
name
(global-val 'known-package-alist w)))))
;;; Begin code deletion
; I removed the case with the same `form' from the previous defpkg call,
; because the evaluation of `form' may results in a list with different
; symbols. The case in which form is evaluated to the same imported
; symbol list is processed as redundant at the end of the function.
#||
(cond
((and package-entry
(or hidden-p
(not (package-entry-hidden-p package-entry)))
(equal (caddr (package-entry-defpkg-event-form package-entry))
form))
(value 'redundant))
(t
||#
;;; End code deletion
(er-progn
(cond
((or package-entry
(eq (ld-skip-proofsp state) 'include-book))
(value nil))
((not (stringp name))
(er soft ctx
"Package names must be string constants and ~x0 is not. See ~
:DOC defpkg."
name))
((equal name "")
; In Allegro CL, "" is prohibited because it is already a nickname for the
; KEYWORD package. But in GCL we could prove nil up through v2-7 by certifying
; the following book with the indicated portcullis:
; (in-package "ACL2")
;
; Portcullis:
; (defpkg "" nil)
;
; (defthm bug
; nil
; :hints (("Goal" :use ((:instance intern-in-package-of-symbol-symbol-name
; (x '::abc) (y 17)))))
; :rule-classes nil)
(er soft ctx
"The empty string is not a legal package name for defpkg."
name))
((not (standard-char-listp (coerce name 'list)))
(er soft ctx
"~x0 is not a legal package name for defpkg, which requires the ~
name to contain only standard characters."
name))
((not (equal (string-upcase name) name))
(er soft ctx
"~x0 is not a legal package name for defpkg, which disallows ~
lower case characters in the name."
name))
((equal name "LISP")
(er soft ctx
"~x0 is disallowed as a a package name for defpkg, because this ~
package name is used under the hood in some Common Lisp ~
implementations."
name))
((let ((len (length *1*-pkg-prefix*)))
(and (<= len (length name))
(string-equal (subseq name 0 len) *1*-pkg-prefix*)))
; The use of string-equal could be considered overkill; probably equal provides
; enough of a check. But we prefer not to consider the possibility that some
; Lisp has case-insensitive package names. Probably we should similarly use
; member-string-equal instead of member-equal below.
(er soft ctx
"It is illegal for a package name to start (even ignoring case) ~
with the string \"~@0\". ACL2 makes internal use of package ~
names starting with that string."
*1*-pkg-prefix*))
((not (true-listp defpkg-book-path))
(er soft ctx
"The book-path argument to defpkg, if supplied, must be a ~
true-listp. It is not recommended to supply this argument, ~
since the system makes use of it for producing useful error ~
messages. The defpkg of ~x0 is thus illegal."
name))
(t (value nil)))
; At one time we checked that if the package exists, i.e. (member-equal name
; all-names), and we are not in the boot-strap, then name must previously have
; been introduced by defpkg. But name may have been introduced by
; maybe-introduce-empty-pkg, or even by a defpkg form evaluated in raw Lisp
; when loading a compiled file before processing events on behalf of an
; include-book. So we leave it to defpkg-raw1 to check that a proposed package
; is either new, is among *defpkg-virgins*, or is consistent with an existing
; entry in *ever-known-package-alist*.
(state-global-let*
((safe-mode
; Warning: If you are tempted to bind safe-mode to nil outside the boot-strap,
; then revisit the binding of *safe-mode-verified-p* to t in the
; #-acl2-loop-only definition of defpkg-raw. See the defparameter for
; *safe-mode-verified-p*.
; In order to build a profiling image for GCL, we have observed a need to avoid
; going into safe-mode when building the system.
(not (global-val 'boot-strap-flg w))))
(er-let*
((pair (simple-translate-and-eval form nil nil
"The second argument to defpkg"
ctx w state
;;; Begin code replacement
; We may as well allow attachments, since we are taking such drastic action
; anyhow.
#||
nil
||#
t
;;; End code replacement
)))
(let ((tform (car pair))
(imports (cdr pair)))
(cond
((not (symbol-listp imports))
(er soft ctx
"The second argument of defpkg must eval to a list of ~
symbols. See :DOC defpkg."))
(t (let* ((imports (sort-symbol-listp imports))
(conflict (conflicting-imports imports))
(base-symbol (packn (cons name '("-PACKAGE")))))
; Base-symbol is the the base symbol of the rune for the rule added by
; defpkg describing the properties of symbol-package-name on interns
; with the new package.
(cond
((member-symbol-name *pkg-witness-name* imports)
(er soft ctx
"It is illegal to import symbol ~x0 because its name ~
has been reserved for a symbol in the package being ~
defined."
(car (member-symbol-name *pkg-witness-name*
imports))))
(conflict
(er soft ctx
"The value of the second (imports) argument of defpkg ~
may not contain two symbols with the same symbol ~
name, e.g. ~&0. See :DOC defpkg."
conflict))
(t (cond
((and package-entry
(not (equal imports
(package-entry-imports
package-entry))))
;;; Begin code deletion
#||
(er soft ctx
"~@0"
(tilde-@-defpkg-error-phrase
name package-entry
(set-difference-eq
imports
(package-entry-imports package-entry))
(set-difference-eq
(package-entry-imports package-entry)
imports)
(package-entry-book-path package-entry)
defpkg-book-path
w
(f-get-global 'system-books-dir state)))
||#
;;; End code deletion
;;; Begin code addition
(progn
; (fms "Debug: imports and ~
; package-entry-imports are ~
; different.~|imports: ~
; ~x0~|%package-entry-imports: ~x1~|"
; (list (cons #\0 imports)
; (cons #\1 (package-entry-imports
; package-entry)))
; (standard-co state) state nil)
(set-imported-symbols-to-pkg imports name)
(value 'redundant)))
;;; End code addition
((and package-entry
(or hidden-p
(not (package-entry-hidden-p package-entry))))
(prog2$
(chk-package-reincarnation-import-restrictions
name imports)
(value 'redundant)))
(t (er-progn
(chk-new-stringp-name 'defpkg name ctx w state)
(chk-all-but-new-name base-symbol ctx nil w state)
; Note: Chk-just-new-name below returns a world which we ignore because
; we know redefinition of 'package base-symbols is disallowed, so the
; world returned is w when an error isn't caused.
; Warning: In maybe-push-undo-stack and maybe-pop-undo-stack we rely
; on the fact that the symbol name-PACKAGE is new!
(chk-just-new-name base-symbol
'theorem nil ctx w state)
(prog2$
(chk-package-reincarnation-import-restrictions
name imports)
(value (list* tform
imports
package-entry ; hidden-p is true
))))))))))))))))))
|