Redundant-encapsulate
Redundancy of encapsulate events
For this documentation topic we assume familiarity with
encapsulate events and the notion of redundancy for events; see
encapsulate and see redundant-events. Until the final remark,
we also assume that redefinition is off (see ld-redefinition-action).
The typical way for an encapsulate event to be redundant is when a
syntactically identical encapsulate has already been executed under the
same default-defun-mode, default-ruler-extenders, and default-verify-guards-eagerness. But more generally, the encapsulate
events need not be syntactically identical; for example, it suffices that they
agree when the contents of local sub-events are ignored. Detailed
criteria for redundancy are given below, but let us first look at a
consequence of the point just made about ignoring the contents of local sub-events. Consider the following sequence of two events.
(encapsulate
()
(defun f (x) x)
(local (defthm f-identity
(equal (f x) x))))
(encapsulate
()
(defun f (x) x)
(local (defthm false-claim
(equal (f x) (not x)))))
You might be surprised to learn that the second is actually redundant, even
though false-claim is clearly not a theorem; indeed, its negation is a
theorem! The following two points may soften the blow. First, this behavior
is as specified above (and is specified more precisely below): the contents of
local events are ignored when checking redundancy of encapsulate events. Second, this behavior is sound, because the logical
meaning of an encapsulate event is taken from the events that it
exports, which do not include events that are local to the
encapsulate event.
Some users, however, want to use encapsulate events for testing in
a way that is thwarted by this ignoring of local sub-events. Consider
the following sort of example.
(encapsulate ()
(local (defthm test1 ...)))
(encapsulate ()
(local (defthm test2 ...)))
Fortunately, in this case both test1 and test2 will be evaluated.
To see why, first note that when a completed encapsulate event with
empty signature has introduced no sub-events, then it has no
effect at all on the logical world. Thus, the first encapsulate
event is not stored in the world; so, the second encapsulate event is not
redundant, since it is executed in a world that contains no trace of the first
encapsulate event.
Also see community books std/testing/eval.lisp,
make-event/eval-check.lisp, and make-event/eval-tests.lisp for more
ways to test in books.
Here are detailed criteria for redundancy of encapsulate events. First, based on a heuristic (but rather thorough) check, the
proposed (new) encapsulate event must be seen as possibly
introducing a new name, for example because one of its sub-events, perhaps
after some macroexpansion, is an invocation of defun, of defthm, or of certain other events that might introduce a name,
including make-event. Second, the two worlds in which each
encapsulate event is evaluated must have the same default-defun-modes, the same default-ruler-extenders, and the same
default-verify-guards-eagerness. Third, the existing and proposed
encapsulate events must contain the same signatures and the
same number of top-level sub-events; let k be that number. Finally: for
each i < k, the ith top-level events E1 and E2 from the
earlier and proposed encapsulates must be related in one of the following
ways.
- E1 and E2 are equal; or
- E1 is of the form (record-expansion E2 ...), with the exception
noted below; or else
- E1 and E2 are equal after replacing each sub-event of E1
with its make-event expansion and replacing each local
sub-event of E1 or E2 by (local (value-triple :elided)). Here,
a sub-event of an event E is defined to be either E itself, or a
sub-event of a constituent event of E in the case that E is a call
of skip-proofs, with-output, with-prover-time-limit,
with-prover-step-limit, record-expansion, time$, progn, progn!, or encapsulate itself.
The second condition has the following exception: it does not apply when
the new encapsulate event takes place within an include-book
event. (Allowing that would be unsound, as explained in a comment in ACL2
source function corresponding-encaps.)
Remark. We conclude with some discussion of redundancy of
encapsulate events in the presence of redefinition (see ld-redefinition-action). Consider the following sequence of events.
(encapsulate () (defun foo (x) x))
(redef!) ; Turn on redefinition.
; not redundant
(encapsulate () (defun foo (x) (cons x x)))
; not redundant
(encapsulate () (defun foo (x) x))
Note that the last encapsulate call is identical to an earlier event,
namely the first one. However, ACL2 never sees that first event when
determining whether the last event is redundant. The reason is that when ACL2
searches the world for a corresponding encapsulate event, it does not
look back past the most recent definition of foo.
By contrast, consider what happens when, in a fresh ACL2 session, we
evaluate the following sequence instead, obtained by wrapping a make-event call around each defun event.
(encapsulate () (make-event '(defun foo (x) x)))
(redef!) ; Turn on redefinition.
; not redundant
(encapsulate () (make-event '(defun foo (x) (cons x x))))
; redundant!
(encapsulate () (make-event '(defun foo (x) x)))
It may be surprising that the last encapsulate call is redundant. The
reason is that it is identical to an earlier encapsulate event. Because
of the use of make-event in the final event, ACL2 does not determine that
the last event is attempting to define foo, so ACL2 does not limit its
search backward through the world as it did in the previous example (where
there were no uses of make-event). The moral of the story: when
redefinition is involved, it may be best not to rely on one's intuition about
redundancy for encapsulate events.
