With-supporters
Automatically define necessary redundant definitions from locally included books
When local include-book forms are used in support of
definitions and theorems, the resulting book or encapsulate event may
be ill-formed because of missing definitions. The macro,
with-supporters, is intended to avoid this problem. See also with-supporters-after for a related utility.
General forms:
(with-supporters local-event event-1 ... event-k)
(with-supporters local-event
:names (name-1 ... name-m)
event-1 ... event-k)
where local-event and each event event-i and (if supplied)
name-i are events and local-event is of the form (local
<event>). The effect is the same as
((encapsulate () local-event EXTRA event-1 ... event-k)
where EXTRA is a sequence of events that includes the following, in
an attempt to re-create the environment produced by local-event in order
to process each event-i during the second pass of the encapsulate event.
- function definitions
- definitions of macros that are aliases for additional functions being
defined; see macro-aliases-table
- in-theory events so that the rules introduced by the EXTRA
definitions are suitably enable or disabled
- If :names is supplied, then the first events in EXTRA are the
events named by the name-i, in order.
We now illustrate with examples, starting with one that does not use the
:names keyword.
Consider the following event.
(encapsulate
()
(local (include-book "std/lists/duplicity" :dir :system))
(defthm duplicity-append
(equal (duplicity a (append x y))
(+ (duplicity a x) (duplicity a y)))))
This event fails because the function duplicity is defined in the
locally included book, and hence that function is undefined when the above
defthm form is processed during the second pass of the encapsulate event. (Recall that local events are skipped during that
pass; see encapsulate.)
One solution is to move the include-book form so that it appears
non-locally in front of the encapsulate event. But we may not want to
include other events from that book, out of concern that rules defined
in that book could affect our proof development.
A more suitable solution may thus be to use the macro,
with-supporters, in place of encapsulate, as follows.
(with-supporters
(local (include-book "std/lists/duplicity" :dir :system))
(defthm duplicity-append
(equal (duplicity a (append x y))
(+ (duplicity a x) (duplicity a y)))))
That macro determines automatically that the function duplicity needs
to be defined, so it generates an encapsulate event like the original
one above but with the definition of duplicity added non-locally. In
this example, duplicity is actually defined in terms of another
function, duplicity-exec, so its definition is needed as well. The
generated event is initially as follows.
(encapsulate
()
(local (include-book "std/lists/duplicity"
:dir :system))
(std::defredundant
:names (duplicity-exec duplicity))
(defthm duplicity-append
(equal (duplicity a (append x y))
(+ (duplicity a x) (duplicity a y)))))
Notice that with-supporters is implemented using the macro std::defredundant. (Also see redundant-events.) When the call above
of std::defredundant is expanded, the result is essentially as follows.
Note that in-theory events are generated in an attempt to set the
enable/disable status of each rule introduced by each function to match the
status after the original include-book event.
(encapsulate
()
(set-enforce-redundancy t)
(defun duplicity-exec (a x n)
(declare (xargs :mode :logic :verify-guards t))
(declare (xargs :measure (:? x)))
(declare (xargs :guard (natp n)))
(if (atom x)
n
(duplicity-exec a (cdr x)
(if (equal (car x) a) (+ 1 n) n))))
(in-theory (e/d ((:type-prescription duplicity-exec)
(:executable-counterpart duplicity-exec))
((:induction duplicity-exec)
(:definition duplicity-exec))))
(defun duplicity (a x)
(declare (xargs :mode :logic :verify-guards t))
(declare (xargs :measure (:? x)))
(declare (xargs :guard t))
(mbe :logic (cond ((atom x) 0)
((equal (car x) a)
(+ 1 (duplicity a (cdr x))))
(t (duplicity a (cdr x))))
:exec (duplicity-exec a x 0)))
(in-theory (e/d ((:type-prescription duplicity)
(:executable-counterpart duplicity))
((:induction duplicity)
(:definition duplicity)))))
For a second example, consider the following form from the community-books, file tools/with-supporters-test-top.lisp.
(with-supporters
(local (include-book "with-supporters-test-sub"))
:names (mac1 mac1-fn)
(defun h2 (x)
(g3 x)))
Here are the events in the locally included book.
(defun mac1-fn (x)
x)
(defmacro mac1 (x)
(mac1-fn x))
(defun g1 (x)
(declare (xargs :guard t))
(mac1 x))
(defun mac2-fn-b (x)
x)
(defun mac2-fn (x)
(mac2-fn-b x))
(defmacro mac2 (x)
(mac2-fn x))
(add-macro-alias mac2 g2)
(defun g2 (x)
(declare (xargs :guard (g1 x)))
(mac2 x))
(defun g3 (x)
(g2 x))
Notice that g3 in the top-level book calls g2, whose guard mentions g1. Now although g1 calls the macro mac1,
with-supporters is not clever enough to notice this, because it tracks
dependencies using translated terms (see term), for which macros have
been expanded away. Thus, macros like mac1, as well as functions used
in their definitions (like mac1-fn), must be specified explicitly.
This specification is made with :names (mac1 mac1-fn) in the call of
with-supporters above.
There is an exception to this required use of the :names keyword
argument: macros that are aliases for functions that support the events.
Returning to our example, notice that g3 is defined using the function
g2, which in turn calls the macro, mac2. So we might expect, as
described for mac1 above, that mac2 must be included in
:names. But fortunately, mac2 is a macro alias for a function that
supports the definition of h2 specified in the call of
with-supporters: g2 supports that definition and mac2 is a
macro alias for g2. Thus mac2 and its supporting function
mac2-fn are added to the list of generated events (called EXTRA,
above).
In summary, the above call of with-supporters generates the following
event.
(ENCAPSULATE NIL
(LOCAL (INCLUDE-BOOK "with-supporters-test-sub"))
(DEFUN MAC1-FN (X) X)
(DEFMACRO MAC1 (X) (MAC1-FN X))
(STD::DEFREDUNDANT G1 MAC2-FN-B MAC2-FN MAC2 G2 G3)
(DEFUN H2 (X) (G3 X)))
As in the first example, std::defredundant generates definitions for
the indicated names.
