Major Section: MISCELLANEOUS
Examples:
(defun hd (x) (if (consp x) (car x) 0))
(local (defthm lemma23 ...))
(progn (defun fn1 ...)
(local (defun fn2 ...))
...)
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 (WITH-OUTPUT ... 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-TRIPLE &), where & is any term;
x macroexpands to one of the forms above.
An exception: an embedded event form may not set the
acl2-defaults-table when 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-table implicitly. An
example at the end of the discussion below illustrates why there is
this restriction.
When an embedded event is executed while ld-skip-proofsp is
'include-book, those parts of it inside local forms are ignored.
Thus,
(progn (defun f1 () 1)
(local (defun f2 () 2))
(defun f3 () 3))
will define f1, f2, and f3 when ld-skip-proofsp is nil but will
define only f1 and f3 when ld-skip-proofsp is 'include-book.Discussion:
Encapsulate and 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
ld-skip-proofs t) are indeed admissible provided that the sequence
of local and non-local events is admissible when ld-skip-proofs is
nil.
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 :rewrite rule
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
ld-skip-proofsp, nil the second
defun is executed and the defthm succeeds. But when we process the
events with ld-skip-proofsp 'include-book, the second defun is
executed, so that foo no longer has the same definition it did when
we proved foo-is-1. Thus, an invalid formula is assumed when we
process the defthm while 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::bar must have been read before the
defpkg for "MY-PKG" was executed.
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 encapsulate
processes event forms. Briefly, on the first pass through the
events the definition of foo will be accepted in defun mode
:program, and hence accepted. But on the second pass the form
(local (program)) is skipped because it is marked as local, and
hence foo is accepted in defun mode :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!
