Major Section: MISCELLANEOUS
Examples: (defun hd (x) (if (consp x) (car x) 0)) (local (defthm lemma23 ...)) (progn (defun fn1 ...) (local (defun fn2 ...)) ...)An exception: an embedded event form may not set the
General Form: An embedded event form is a term, x, such that
x is a call of an event function other than DEFPKG (see the documentation for events for a listing of the event functions);
x is of the form (LOCAL x1) where x1 is an embedded event form;
x is of the form (PROGN x1 ... xn), where each xi is an embedded event form;
x is of the form (VALUE &), where & is any term;
x macroexpands to one of the forms above.
acl2-defaults-tablewhen in the context of
local. Thus for example, the form
(local (table acl2-defaults-table :defun-mode :program))is not an embedded event form, nor is the form
(local (program)), since the latter sets the
acl2-defaults-tableimplicitly. An example at the end of the discussion below illustrates why there is this restriction.
When an embedded event is executed while
include-book, those parts of it inside
local forms are ignored.
(progn (defun f1 () 1) (local (defun f2 () 2)) (defun f3 () 3))will define
nilbut will define only
include-book place restrictions on the kinds of
forms that may be processed. These restrictions ensure that the
non-local events (which will ultimately be processed with
t) are indeed admissible provided that the sequence
of local and non-local events is admissible when
Local permits the hiding of an event or group of events in the sense
that local events are processed when we are trying to establish the
admissibility of a sequence of embedded events but are ignored when
we are constructing the world produced by assuming that sequence.
Thus, for example, a particularly ugly and inefficient
might be made local to an encapsulate that ``exports'' a desirable
theorem whose proof requires the ugly lemma.
To see why we can't allow just anything in as an embedded event, consider allowing the form
(if (ld-skip-proofsp state) (defun foo () 2) (defun foo () 1))followed by
(defthm foo-is-1 (equal (foo) 1)).When we process the events with
defunis executed and the
defthmsucceeds. But when we process the events with
include-book, the second
defunis executed, so that
foono longer has the same definition it did when we proved
foo-is-1. Thus, an invalid formula is assumed when we process the
defthmwhile skipping proofs. Thus, the first form above is not a legal embedded event form.
Defpkg is not allowed because it affects how things are read after
it is executed. But all the forms embedded in an event are read
before any are executed. That is,
(encapsulate nil (defpkg "MY-PKG" nil) (defun foo () 'my-pkg::bar))makes no sense since
my-pkg::barmust have been read before the
Finally, let us elaborate on the restriction mentioned earlier
related to the
acl2-defaults-table. Consider the following form.
(encapsulate () (local (program)) (defun foo (x) (if (equal 0 x) 0 (1+ (foo (- x))))))See local-incompatibility for a discussion of how
encapsulateprocesses event forms. Briefly, on the first pass through the events the definition of
foowill be accepted in
program, and hence accepted. But on the second pass the form
(local (program))is skipped because it is marked as local, and hence
foois accepted in
logic. Yet, no proof has been performed in order to admit
foo, and in fact, it is not hard to prove a contradiction from this definition!