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-1 and
foo-impl-2. A function, bar, is defined using a macro, mac,
whose expansion depends on which of foo-impl-1 or foo-impl-2 is
attached to foo. If ACL2 were to allow this, then as indicated by the
comments above, (bar) would be defined to be nil on the first pass of
the encapsulate form, where foo is attached to foo-impl-2; but
(bar) would be defined to be t on the second pass, where foo is
attached to foo-impl-1 because the second defattach call is
local. Thus, after execution of the encapsulate form, (bar)
would be provably equal to t even though there would be a theorem,
bar-is-nil -- proved during the first pass of the encapsulate --
saying that (bar) is nil!
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 f2 even though that
defattach is local, because the expansion of the corresponding
make-event is saved during the first pass of certify-book, when
full admissibility checks are done. Then even after including the book, the
definition of f2 will be based on the second (local)
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)))
