Deftheory-static
Define a `static' theory (to enable or disable a set of rules)
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)
The arguments are handled the same as for deftheory. Thus,
name is a new symbolic name (see name), and term is a term
that when evaluated will produce a theory (see theories). 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.
