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
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-conswill be disabled, because it was disabled at the time the expression
(current-theory :here)was evaluated when processing the
my-theorywhile including the book. However, if we execute
(in-theory (theory 'my-static-theory)), then the rule
car-conswill be enabled, because the value of the theory
my-static-theorywas 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
nameis a new symbolic name (see name),
termis a term that when evaluated will produce a theory (see theories), and
doc-stringis an optional documentation string (see doc-string). Except for the variable
termmust contain no free variables.
Termis evaluated with
worldbound 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
deftheory, the value returned is the length of the resulting
We conclude with an optional discussion about the implementation of
deftheory-static, for those familiar with
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.