/usr/share/acl2-8.0dfsg/books/hacking/redefun.lisp is in acl2-books-source 8.0dfsg-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 123 124 125 126 | (in-package "ACL2")
;Needed to use, but not needed for certification:
;(include-book "defcode" :load-compiled-file :comp :ttags ((defcode)))
(program)
(set-state-ok t)
; cert_param: (non-acl2r)
(defun chk-acceptable-redefun (def ctx wrld state)
(er-let*
((tuple (chk-acceptable-defuns (list def) ctx wrld state)))
(assert$
(equal (length tuple) 23)
(let* ((name (car def))
(new-wrld (nth 18 tuple))
(old-symbol-class
(getprop name 'symbol-class 0 'current-acl2-world wrld))
(new-symbol-class (nth 15 tuple))
(old-formals
(getprop name 'formals 0 'current-acl2-world wrld))
(new-formals
(getprop name 'formals 0 'current-acl2-world new-wrld))
(old-stobjs-in
(getprop name 'stobjs-in 0 'current-acl2-world wrld))
(new-stobjs-in
(getprop name 'stobjs-in 0 'current-acl2-world new-wrld))
(old-stobjs-out
(getprop name 'stobjs-out 0 'current-acl2-world wrld))
(new-stobjs-out
(getprop name 'stobjs-out 0 'current-acl2-world new-wrld)))
(cond ((eql old-symbol-class 0)
(er soft ctx "No existing definition: ~x0" name))
((nth 19 tuple) ; non-executablep
(er soft ctx
"Please do not redefun a non-executable function. The ~
offending definition is: ~x0."
def))
((not (eq ':program old-symbol-class))
(er soft ctx
"Old definition should have defun-mode :program. Sorry."))
((not (eq ':program new-symbol-class))
(er soft ctx
"New definition should have defun-mode :program. Sorry."))
((not (equal new-formals old-formals))
(er soft ctx
"Please use the same formal parameter list when redefining. ~
Previous formals: ~x0"
old-formals))
((not (equal new-stobjs-in old-stobjs-in))
(er soft ctx
"New definition should have the same stobjs-in.Previously, ~
~x0. Specified, ~x1."
old-stobjs-in new-stobjs-in))
((not (equal new-stobjs-out old-stobjs-out))
(er soft ctx
"New definition should have the same stobjs-out.Previously, ~
~x0. Specified, ~x1."
old-stobjs-out new-stobjs-out))
(t ; okay
(value :invisible)))))))
; this is a safer version of doing defun with redefinition allowed.
;
; only :program mode functions may be used here, because the intent is to
; maintain sound reasoning.
;
; lots of checks are performed and actions are taken to prevent the logic from
; being tainted by the redefinition.
;
(defmacro redefun (name ll &rest decls-and-body)
(declare (xargs :guard (and (symbolp name)
(symbol-listp ll)
(consp decls-and-body))))
(let ((def (list* name ll decls-and-body)))
`(progn+redef
(assert-include-defun-matches-certify-defun ,name)
(defcode
:loop (er-progn
(assert-no-special-raw-definition ,name)
(chk-acceptable-redefun ',def
'redefun
(w state)
state)
(ensure-program-only-flag ,name)
(defun . ,def))
:extend
(in-raw-mode
(defun-*1* ,name ,ll
(if (f-get-global 'safe-mode *the-live-state*)
(throw-raw-ev-fncall (list 'program-only-er ',name
(list . ,ll) 't '(nil) t))
(,name . ,ll))))
:compile
(defun . ,def)))))
; this uses redefun and our code rewrite stuff (see rewrite-code.lisp,
; especially compute-copy-defun+rewrite) to redefine a :program mode
; function in terms of its existing definition.
;
(defmacro redefun+rewrite (name &rest rewrite-spec)
(declare (xargs :guard (symbolp name)))
`(make-event
(compute-copy-defun+rewrite
',name ',name ',rewrite-spec 'redefun state)))
; tests and stuff
#|
(include-book
"defcode" :ttags ((defcode)))
(defttag t)
(redefun deflabel-fn (name state doc event-form)
(declare (ignore doc event-form))
(value name))
(set-guard-checking :none)
(deflabel moo)
(deflabel moo)
|#
|