/usr/share/acl2-8.0dfsg/books/hacking/dynamic-make-event.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 | (in-package "ACL2")
#|
dynamic-make-event.lisp
-----------------------
By Peter Dillinger, ca. 2006-2009
If you modify the code for an event (such as defun) to call
DYNAMIC-MAKE-EVENT-FN, then that event can have a make-event expansion,
just as a MAKE-EVENT would, meaning that at include-book time, the
expansion is the only part that is seen.
This functionality used to require a hack, but in latest ACL2 versions,
it does not.
The code here is trivial, but we want this functionality to remain in
ACL2, so it should be in the regression suite. See
dynamic-make-event-test.lisp
|#
(program)
(set-state-ok t)
; body is the new form to replace this one
; event-form is the original (if available?)
(defun dynamic-make-event-fn (body event-form state)
(make-event-fn `',body
nil
nil
nil
event-form
state))
#| used to be needed for events other than MAKE-EVENT to have expansion:
(progn+touchable
:all
(redefun+rewrite
make-event-fn
(:pat (mv-let (wrappers base)
%1%
(cond ((member-eq (car base) %2%) %stuff%)
. %3%))
:repl (mv-let (wrappers base)
%1%
(declare (ignorable base))
%stuff%)
:vars (%1% %2% %3% %stuff%)
:mult 1)))
|#
|