THEORY-INVARIANT

Major Section:  EVENTS

Example:
(theory-invariant (not (and (member-equal '(:rewrite left-to-right)
                                           theory)
                            (member-equal '(:rewrite right-to-left)
                                          theory)))
                  :key my-invariant
                  :error nil)

General Form:
(theory-invariant term &key key error)

o term is a term that uses no variables other than theory and world;

o key is an arbitrary ``name'' for this invariant (if omitted, an integer is generated and used); and

o :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.

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 (setting the invariant to t) with table.

Theory-invariant-table maps arbitrary keys to terms mentioning, at most, the variables theory and world. 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 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 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.

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. 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)))

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).

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.