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.

   (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 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:


  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))

(defun body-2 (name formals body)
  (declare (ignore name))
  `(if (acl2-numberp ,(car formals))

(defmacro defun+ (name formals body)
    (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)))