DEFTHEORY-STATIC

define a `static' theory (to enable or disable a set of rules)
Major Section:  EVENTS

This macro provides a variant of deftheory, such that the resulting theory is the same at include-book time as it was at certify-book time.

We assume that the reader is familiar with theories; see deftheory. We begin here by illustrating how deftheory-static differs from deftheory. Suppose for example that the following events are the first two events in a book, where that book is certified in the initial ACL2 world (see ground-zero).

(deftheory my-theory
  (current-theory :here))
(deftheory-static my-static-theory
  (current-theory :here))
Now suppose we include that book after executing the following event.
(in-theory (disable car-cons))
Suppose that later we execute (in-theory (theory 'my-theory)). Then the rule car-cons will be disabled, because it was disabled at the time the expression (current-theory :here) was evaluated when processing the deftheory of my-theory while including the book. However, if we execute (in-theory (theory 'my-static-theory)), then the rule car-cons will be enabled, because the value of the theory my-static-theory was saved at the time the book was certified.

General Form:
(deftheory-static name term :doc doc-string)
The arguments are handled the same as for deftheory. Thus, name is a new symbolic name (see name), term is a term that when evaluated will produce a theory (see theories), and doc-string is an optional documentation string (see doc-string). Except for the variable world, term must contain no free variables. Term is evaluated with world bound to the current world (see world) and the resulting theory is then converted to a runic theory (see theories) and associated with name. Henceforth, this runic theory is returned as the value of the theory expression (theory name).

As for deftheory, the value returned is the length of the resulting theory.

We conclude with an optional discussion about the implementation of deftheory-static, for those familiar with make-event. The following macroexpansion of the deftheory-static form above shows how this works (see trans1).

ACL2 !>:trans1 (deftheory-static my-static-theory
                 (current-theory :here))
 (MAKE-EVENT (LET ((WORLD (W STATE)))
                  (LIST 'DEFTHEORY
                        'MY-STATIC-THEORY
                        (LIST 'QUOTE (CURRENT-THEORY :HERE)))))
ACL2 !>

The idea is that upon evaluation of this make-event form, the first step is to evaluate the indicated LET expression to obtain a form (deftheory my-theory '(...)), where ``(...)'' is a list of all runes in current theory. If this form is in a book being certified, then the resulting deftheory form is stored in the book's certificate, and is used when the book is included later.