Major Section: MISCELLANEOUS
Attachments provide a way to execute constrained functions. But in some cases, ACL2 will not permit such execution. We discuss this issue briefly here. For more information about attachments, see defattach.
We illustrate this issue with the following example, discussed below.
(encapsulate () (defstub foo () t) (defn foo-impl-1 () t) (defattach foo foo-impl-1) (defn foo-impl-2 () nil) (local (defattach foo foo-impl-2)) (defmacro mac () (foo)) ; nil in the first pass, t in the second pass (defun bar () (mac)) ; nil in the first pass, t in the second pass (defthm bar-is-nil (equal (bar) nil)) )
Here, a non-executable function
foo is introduced with no constraints,
and is provided two contradictory implementations,
foo-impl-2. A function,
bar, is defined using a macro,
whose expansion depends on which of
foo. If ACL2 were to allow this, then as indicated by the
(bar) would be defined to be
nil on the first pass of
encapsulate form, where
foo is attached to
(bar) would be defined to be
t on the second pass, where
foo-impl-1 because the second
defattach call is
local. Thus, after execution of the
would be provably equal to
t even though there would be a theorem,
bar-is-nil -- proved during the first pass of the
Fortunately, ACL2 does not permit this to happen. The example above produces the following output.
ACL2 !>>(DEFUN BAR NIL (MAC)) ACL2 Error in ( DEFUN BAR ...): In the attempt to macroexpand the form (MAC), evaluation of the macro body caused the following error: ACL2 cannot ev the call of undefined function FOO on argument list: NIL Note that because of logical considerations, attachments (including FOO-IMPL-2) must not be called in this context.
We see, then, the importance of disallowing evaluation using attachments during macroexpansion. ACL2 is careful to avoid attachments in situations, like this one, where using attachments could be unsound.
We conclude with an example illustrating how
make-event can be used to
work around the refusal of ACL2 to use attachments during macroexpansion.
The idea is that
make-event expansions are stored, and this avoids the
local attachments. In particular, for the example below, the
defattach affects the body of
f2 even though that
local, because the expansion of the corresponding
make-event is saved during the first pass of
full admissibility checks are done. Then even after including the book, the
f2 will be based on the second (
defattach form below.
(in-package "ACL2") (defun body-1 (name formals body) (declare (ignore name)) `(if (consp ,(car formals)) ,body nil)) (defun body-2 (name formals body) (declare (ignore name)) `(if (acl2-numberp ,(car formals)) ,body t)) (defmacro defun+ (name formals body) `(make-event (if (foo) ; attachable stub '(defun ,name ,formals ,(body-1 name formals body)) '(defun ,name ,formals ,(body-2 name formals body))))) ;;; (defun+ f1 (x y) (cons x y)) ; fails because foo has no attachment (defstub foo () t) (defn foo-true () t) (defn foo-false () nil) (defattach foo foo-true) (defun+ f1 (x y) (cons x y)) (local (defattach foo foo-false)) (defun+ f2 (x y) (cons x y)) (assert-event (equal (f1 3 t) nil)) (assert-event (equal (f2 3 t) (cons 3 t)))