		Search-engine friendly clone of the ACL2 documentation.

Theories

Theories-and-primitives

Warnings from disabling or enabling certain built-in functions

When you disable the definition or executable-counterpart of a built-in function, you may see a warning, for example as follows.

ACL2 !>(in-theory (disable mv-nth iff length))

ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)):  The :DEFINITION
rules for the built-in functions MV-NTH and IFF are disabled by the
theory expression (DISABLE MV-NTH IFF LENGTH), but some expansions
of their calls may still occur.  See :DOC theories-and-primitives.

This warning is telling us that the built-in functions mv-nth and iff are given certain special handling, hence their calls may be expanded even when their definitions are disabled. This behavior applies to the functions in the list obtained by evaluating the constant, *definition-minimal-theory*.

These warnings can be eliminated by turning off all theory warnings (see set-inhibit-warnings) or even turning off all warnings (see set-inhibit-output-lst), or simply by evaluating the following form.

(assign verbose-theory-warning nil)

But before you eliminate such theory warnings, you may wish to read the following to gain more understanding of their significance.

First consider the following example, evaluated after the in-theory event displayed above.

ACL2 !>(thm (equal (mv-nth 2 (list a b c d e)) c))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION MV-NTH)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  18

Proof succeeded.
ACL2 !>

Note that even though the definition of mv-nth had been disabled, nevertheless its definition rule was used in proving this theorem. It is as though mv-nth had not been disabled after all! The warning is intended to indicate that expansion of mv-nth calls may be made by the theorem prover even when mv-nth is disabled. Indeed, the prover has special-purpose code for simplifying certain mv-nth calls.

A similar issue can arise for executable-counterpart rules, as the following log illustrates.

ACL2 !>(in-theory (disable (:e symbolp)))

ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)):  The :EXECUTABLE-
COUNTERPART rule for the built-in function SYMBOLP is disabled by the
theory expression (DISABLE (:E SYMBOLP)), but some evaluations of its
calls may still occur.  See :DOC theories-and-primitives.


Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Warnings:  Theory
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 (:NUMBER-OF-ENABLED-RUNES 4268)
ACL2 !>(thm (symbolp 'a))

Q.E.D.

Summary
Form:  ( THM ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 !>

In general, ACL2 warns when in-theory events or hints leave you in a theory where rules for certain built-in functions have just been disabled, yet these rules may be applied in some cases nonetheless, because of special-purpose prover code for handling calls of that function. The built-in function symbols with such definition rules or executable-counterpart rules are those in the following two lists, which are the respective values of built-in constants *definition-minimal-theory* and *built-in-executable-counterparts*.

Definition: *definition-minimal-theory*

(defconst *definition-minimal-theory*
  (list* 'mv-nth
         'iff
         *expandable-boot-strap-non-rec-fns*))

Definition: *built-in-executable-counterparts*

(defconst *built-in-executable-counterparts*
  '(acl2-numberp binary-* binary-+ unary-- unary-/
                 < car cdr char-code characterp code-char
                 complex complex-rationalp coerce
                 cons consp denominator equal if imagpart
                 integerp intern-in-package-of-symbol
                 numerator pkg-witness pkg-imports
                 rationalp realpart stringp symbol-name
                 symbol-package-name symbolp not))

A third class of warnings pertains to primitives that do not have definitions, such as cons. Here is an example of such a warning, for the event (in-theory (disable cons)).

ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)):  There is no effect
from disabling or enabling :DEFINITION rules for primitive functions
(see :DOC primitive).  For the expression (DISABLE CONS), the attempt
to disable CONS will therefore have no effect for its definition.
See :DOC theories-and-primitives.

Unlike the warnings discussed above, warnings about primitives can occur not only when disabling definitions but also when enabling them. Here is what happens when we submit (in-theory (enable cons)) immediately after the event just above.

ACL2 Warning [Theory] in ( IN-THEORY (ENABLE ...)):  There is no effect
from disabling or enabling :DEFINITION rules for primitive functions
(see :DOC primitive).  For the expression (ENABLE CONS), the attempt
to enable CONS will therefore have no effect for its definition.  See
:DOC theories-and-primitives.

If however we submit (in-theory (enable cons)) again, or in a fresh session, there is no warning. To see why, understand that all of these warnings are based on a comparison of the preceding current theory with the new one. If cons is already enabled, then (in-theory (enable cons)) is a no-op; hence, there is no warning.

There is another case in which there is no warning: if all definitions of primitives transition from disabled to enabled, or vice-versa. For example, such a transition occurs for consecutive events (in-theory (current-theory 'ground-zero)) and (in-theory (theory 'minimal-theory)).

We conclude with a note for advanced users only. You can eliminate all special treatment discussed above for expanding the definition of mv-nth (but not for any of the other primitives listed above) by evaluating the following form (also see defattach-system).

(defattach-system simplifiable-mv-nth-p constant-nil-function-arity-0)

That said, this is probably only useful for very specific cases of ``system-level'' programming. You can restore the default behavior as follows.

(defattach-system simplifiable-mv-nth-p constant-t-function-arity-0)