Major Section: EVENTS
Example: (theory-invariant (not (and (member-equal '(:rewrite left-to-right) theory) (member-equal '(:rewrite right-to-left) theory))))where
General Forms: (theory-invariant term) ; conjoin a new invariant term or (theory-invariant term key) ; change an existing invariant term
termis a term that uses no variables other than
keyis an arbitrary ``name'' for this invariant. If
keyis omitted, an integer is generated and used.
Theory-invariantis 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
table event. More general access to the
table is provided by
table itself. For example, the table can be
inspected or cleared (setting the invariant to
Theory-invariant-table maps arbitrary keys to terms mentioning, at
most, the variables
world. Every time an alleged theory
expression is evaluated, e.g., in the
in-theory event or
hint, each of the terms in
theory-invariant-table is evaluated with
theory bound to the runic theory (see theories) obtained from
the theory expression and
world bound to the current ACL2 world
(see world). If the result is
nil, a warning message is
printed. Thus, the table can be thought of as a list of conjuncts.
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
theory-invariant with a new term but the same name, you can
overwrite that conjunct of the 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 when they are violated the user is warned.
Since theory invariants are arbitrary terms, macros may be used to express commonly used restrictions. Because theory invariants are a new idea in ACL2, we have only defined one such macro for illustrative purposes. Executing the event
(theory-invariant (incompatible (:rewrite left-to-right) (:rewrite right-to-left)))would subsequently cause a warning message 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
Note: If the table event is used directly to
:put a term into the
theory invariant table, be aware that the term must be in translated
form. This is enforced by the
value invariant for
theory-invariant-table. But the upshot of this is that you will be
unable to use macros in theory invariants stored directly with the
:put table event.