Allowing a name to be introduced ``twice''
Sometimes an event will announce that it is ``redundant'', meaning that the form is not evaluated because ACL2 determines that its effect is already incorporated into the logical world. Thus, when this happens, no change to the logical world takes place. This feature permits two independent books, each of which defines some name, to be included sequentially provided they use exactly the same definition.
Note that by the definition above, a form can have no effect on the logical world yet not be considered to be redundant. Here is an example of such a form.
(value-triple (cw "Hello world.~%"))
When are two logical-name definitions considered ``the same''? It depends upon the kind of event that introduces that name. We consider these below in alphabetical order, followed by ``Note About'' comments. Macros in the community-books may also support redundancy; see their documentation for details, since below we only discuss ACL2 events that are built into ACL2.
A defstobj or defabsstobj is redundant if there is already an identical such event in the logical world.
A defattach event is never redundant. (Reasons are provided in a
comment in the ACL2 sources definition of defattach in the ACL2 logic.) Note
A defaxiom or defthm event is redundant if there is already
an axiom or theorem of the given name and the two events are
syntactically identical. But there is the following more generous criterion:
both the formula (after macroexpansion) and the rule-classes (after
translation and certain ``truncation'') are syntactically identical. This
``truncation'' involves removing the
A defconst is redundant if the name is already defined either with
a syntactically identical
A deflabel event is never redundant. This means that if you have a deflabel in a book and that book has been included (without error), then references to that label denote the point in history at which the book introduced the label. See the note about shifting logical names, below.
A defmacro event is redundant if there is already a macro defined with the same name and syntactically identical arguments, guard, and body.
A defpkg event is redundant if a package of the same name with exactly the same imports has been defined.
A defthm event is redundant according to the criteria given above
in the discussion of
A deftheory event is redundant if keyword argument
(deftheory foo (disable append revappend) :redundant-okp t) (defthm my-car-cons (equal (car (cons x y)) x)) (deftheory foo (disable revappend append) :redundant-okp t)
A defun, defuns, or mutual-recursion event is
redundant if for each function to be introduced, there has already been
introduced a function with the same name, formals, and body (before
macroexpansion), and with the same values declared for the
An encapsulate event is most commonly redundant when a
syntactically identical encapsulate has already been executed under
the same default-defun-mode, default-ruler-extenders, and
default-verify-guards-eagerness. The full criterion for redundancy of
An in-theory event is never redundant by default, though that can be changed; see set-in-theory-redundant-okp. Note that it doesn't define any name.
An include-book event is redundant if the book has already been included.
A call of make-event is never redundant, as its argument is always evaluated to obtain the make-event expansion. However, that expansion may of course be redundant.
A mutual-recursion event is redundant according to the criteria in
the discussion above for the case of a
A progn event is never redundant: its subsidiary events are
always considered. Of course, its sub-events may themselves be redundant. If
all of its sub-events are redundant — or more generally, if none of the
sub-events changes the logical world — then the
A push-untouchable event is redundant if every name supplied is already a member of the corresponding list of untouchable symbols.
A regenerate-tau-database event is never redundant. Note that it doesn't define any name.
A remove-untouchable event is redundant if no name supplied is a member of the corresponding list of untouchable symbols.
A reset-prehistory event is redundant if it does not cause any change.
A set-body event is redundant if the indicated body is already the current body.
A table event not define any name. It is redundant when it sets
the value already associated with a key of the table, or when it sets an
entire table (using keyword
Memoization is carried out using a table,
A verify-guards event is redundant if the function has already had its guards verified.
Note About Built-in (Predefined) Functions and Macros:
Redundancy is restricted for built-in macros and functions that have
special raw Lisp code. Such redundancy is only legal in the context of local. This restriction is needed for soundness, for technical reasons
omitted here (details may be found in a long comment about redundant-events in
Note About Appropriate Modes:
Suppose a function is being redefined and that the formals, guards, types,
user-defined stobjs, and bodies are identical. When are the
Note About Shifting Logical Names:
Suppose a book defines a function
This may adversely affect the user of your book. For example, suppose your book creates a theory via deftheory that is advertised just to contain the names generated by the book. But suppose you compute the theory as the very last event in the book using:
(set-difference-theories (universal-theory :here) (universal-theory fn))
The moral of this is simple: when building books that other people will use, it is best to describe your theories in terms of logical names that will not shift around when the books are included. The best such names are those created by deflabel.
Note About Unfortunate Redundancies.
Notice that our syntactic criterion for redundancy of defun events may not allow redefinition to take effect unless there is a syntactic change in the definition. The following example shows how an attempt to redefine a function can fail to make any change.
(set-ld-redefinition-action '(:warn . :overwrite) state) (defmacro mac (x) x) (defun foo (x) (mac x)) (defmacro mac (x) (list 'car x)) (set-ld-redefinition-action nil state) (defun foo (x) (mac x)) ; redundant, unfortunately; foo does not change (thm (equal (foo 3) 3)) ; succeeds, showing that redef of foo didn't happen
The call of macro
One workaround is first to supply a different definition of
(set-ld-redefinition-action '(:warn . :overwrite) state) (defmacro mac (x) x) (defun foo (x) (mac x)) (defmacro mac (x) (list 'car x)) (defun foo (x) (mac x)) ; no longer redundant (thm (equal (foo 3) 3)) ; fails, as we would like
To summarize: If a defun form is submitted that meets the usual redundancy criteria, then it may be considered redundant even if a macro called in the definition has since been redefined. The analogous problem applies to constants, i.e., symbols defined by defconst that occur in the definition body. However, if redefinition is currently active the problem goes away: that is, the redundancy check is strengthened to check the ``translated'' body, in which macro calls and constants defined by defconst are expanded away.
The above discussion for defun forms applies to defconst forms as well. However, for defmacro forms ACL2 always checks translated bodies, so such bogus redundancy does not occur.
Here is more complex example illustrating the limits of redefinition, based on one supplied by Grant Passmore.
(defun n3 () 0) (defun n4 () 1) (defun n5 () (> (n3) (n4))) ; body is see normalized to nil (thm (equal (n5) nil)) ; succeeds, trivially (set-ld-redefinition-action '(:warn . :overwrite) state) (defun n3 () 2) (thm (equal (n5) nil)) ; still succeeds, sadly
We may expect the final thm call to fail because of the following
A related phenomenon can occur for encapsulate. As explained
(defmacro mac (x) x) (encapsulate () (defun foo (x) (mac x))) (set-ld-redefinition-action '(:warn . :overwrite) state) (defmacro mac (x) (list 'car x)) (encapsulate () (defun foo (x) (mac x)))
A workaround can be to add something trivial to the
(encapsulate () (deflabel try2) ; ``Increment'' to try3 next time, and so on. (defun foo (x) x))