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,
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 been disabled after all!
The warning is intended to indicate that expansion of
A similar issue can arise for
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
(defconst *definition-minimal-theory* (list* 'mv-nth 'iff *expandable-boot-strap-non-rec-fns*))
(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
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
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
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
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)