Why attachments are sometimes not used
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
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
issue of local attachments. In particular, for the example below, the
second defattach affects the body of
(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)))