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.
