Theory-invariant
User-specified invariants on theories
Examples:
(theory-invariant (not (and (active-runep '(:rewrite left-to-right))
(active-runep '(:rewrite right-to-left))))
:key my-invariant
:error nil)
; Equivalent to the above:
(theory-invariant (incompatible (:rewrite left-to-right)
(:rewrite right-to-left))
:key my-invariant
:error nil)
; As above, but cause an error for non-runes:
(theory-invariant (incompatible! (:rewrite left-to-right)
(:rewrite right-to-left))
:key my-invariant
:error nil)
General Form:
(theory-invariant term &key key error)
where:
- term is a term that uses no variables other than ens and state;
- key is an arbitrary ``name'' for this invariant (if omitted, an
integer is generated and used); and
- :error specifies the action to be taken when an invariant is
violated — either nil if a warning is to be printed, else t
(the default) if an error is to be caused.
Theory-invariant is an event that adds to or modifies the table
of user-supplied theory invariants that are checked each time a theory
expression is evaluated.
The theory invariant mechanism is provided via a table (see table)
named theory-invariant-table. In fact, the theory-invariant
``event'' is just a macro that expands into a use of the table event.
More general access to the theory-invariant table is provided by
table itself. For example, the table can be inspected or
cleared with table; you can clear an individual theory invariant by
setting the invariant to t, or eliminate all theory invariants with the
command (table theory-invariant-table nil nil :clear).
Theory-invariant-table maps arbitrary keys to records containing terms
that mention, at most, the variables ens and state. Every time
an alleged theory expression is evaluated, e.g., in the in-theory
event or :in-theory hint, each of the terms in
theory-invariant-table is evaluated with ens bound to a so-called
``enabled structure'' obtained from the theory expression and state
bound to the current ACL2 state (see state). Users generally need not
know about the enabled structure, other than that it can be accessed using the
macros active-runep and incompatible; see active-runep and
see incompatible. (Also see variants active-or-non-runep and
incompatible!, whose use by the theory-invariant mechanism will cause
an error any time either ``rune'' is not truly a rune.) If the result is
nil, a message is printed and an error occurs (except, only a warning
occurs if :error nil is specified). Thus, the table can be
thought of as a list of conjuncts. Each term in the table has a
``name,'' which is just the key under which the term is stored. When a theory
violates the restrictions specified by some term, both the name and the term
are printed. By calling theory-invariant with a new term but the same
name, you can overwrite that conjunct of the theory invariant; but see the
Local Redefinition Caveat at the end of this note. You may want to avoid
using explicit names, since otherwise the subsequent inclusion of another book
that defines a theory invariant with the same name will override your theory
invariant.
Theory invariants are particularly useful in the context of large rule sets
intended for re-use. Such sets often contain conflicting rules, e.g., rules
that are to be enabled when certain function symbols are disabled, rules that rewrite in opposite directions and thus loop if
simultaneously enabled, groups of rules which should be enabled
in concert, etc. The developer of such rule sets understands these
restrictions and probably documents them. The theory invariant mechanism
allows the developer to codify his restrictions so that the user is alerted
when they are violated.
Since theory invariants are arbitrary terms, macros may be used to express
commonly used restrictions. For example, executing the event
(theory-invariant (incompatible (:rewrite left-to-right)
(:rewrite right-to-left)))
would subsequently cause an error any time the current theory contained
both of the two runes shown. Of course, incompatible is just
defined as a macro. Its definition may be inspected with :pe
incompatible.
In order for a theory-invariant event to be accepted, the proposed
theory invariant must be satisfied by the current theory (see current-theory). The value returned upon successful execution of the event
is the key (whether user-supplied or generated).
Local Redefinition Caveat. Care needs to be taken when redefining a theory
invariant in a local context. Consider the following example.
(theory-invariant
(active-runep '(:definition binary-append))
:key app-inv)
(encapsulate
()
(local (theory-invariant t :key app-inv))
(in-theory (disable binary-append))
(defthm ...))
The second pass of the encapsulate will fail, because the in-theory event violates the original theory-invariant and the local theory-invariant is skipped in the second pass of the encapsulate. Of course, local theory-invariants in books can cause the analogous problem in the second (include-book)
pass of a certify-book. In both cases, though, the theory invariants
are only checked at the conclusion of the (include-book or
encapsulate) event. Indeed, theory invariants are checked at the end of
every event related to theories, including defun, defthm, in-theory, encapsulate, and include-book,
except for events executed on behalf of an include-book or the second
pass of an encapsulate.
