Forms that may be embedded in other events
(defun hd (x) (if (consp x) (car x) 0))
(local (defthm lemma23 ...))
(progn (defun fn1 ...)
(local (defun fn2 ...))
An embedded event form is a term, x, such that:
- x is a call of an event function other than defpkg (see
events for a listing of the event functions);
- x is a call of encapsulate, progn, progn!,
- x is of the form (LOCAL x1) where x1 is an
embedded event form;
- x is of the form (MAKE-EVENT &), where & is any term whose
expansion is an embedded event (see make-event);
- x is of the form (SKIP-PROOFS x1) where x1 is
an embedded event form;
- x is of the form (WITH-CBD str x1), where str is a string
and x1 is an embedded event form;
- x is of the form (WITH-GUARD-CHECKING-EVENT c x1) or
(WITH-GUARD-CHECKING-EVENT (QUOTE c) form), where c is a member of
the list (t nil :nowarn :all :none) and x1 is an embedded event
- x is of the form (WITH-OUTPUT ... x1),
(WITH-PROVER-STEP-LIMIT ... x1 ...), or (WITH-PROVER-TIME-LIMIT
... x1), where x1 is an embedded event form;
- x macroexpands to one of the forms above; or
- [intended only for the implementation] x is (RECORD-EXPANSION x1
x2), where x1 and x2 are embedded event forms.
However, we add the following restrictions for local contexts.
Only embedded event forms are allowed in a book after its initial in-package form. See books. However, you may find that make-event allows you to get the effect you want for a form that is not an
embedded event form. For example, you can put the following into a book,
which assigns the value 17 to state global variable x:
(make-event (er-progn (assign x 17)
(value '(value-triple nil)))
For another use of make-event to create embedded event forms, see
When an embedded event is executed while ld-skip-proofsp is
'include-book, those parts of it inside local forms are
(progn (defun f1 () 1)
(local (defun f2 () 2))
(defun f3 () 3))
will define f1, f2, and f3 when ld-skip-proofsp is
nil or t, but will define only f1 and f3 when ld-skip-proofsp is 'include-book.
Encapsulate, progn, and include-book place
restrictions on the kinds of forms that may be processed. These restrictions
ensure that the non-local events are indeed admissible provided that
the sequence of local and non-local events is admissible when
proofs are done, i.e., when ld-skip-proofs is nil. But progn! places no such restrictions, hence is potentially dangerous and should
be avoided unless you understand the ramifications; so it is illegal unless
there is an active trust tag (see defttag).
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 events embedded in encapsulate forms or in books, 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 as an embedded event, consider
allowing the form
(if (ld-skip-proofsp state)
(defun foo () 2)
(defun foo () 1))
(defthm foo-is-1 (equal (foo) 1)).
When we process the events with ld-skip-proofsp is 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.
If you encounter a situation where these restrictions seem to prevent you
from doing what you want to do, then you may find make-event to be
helpful. See make-event.
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,
(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.
(defun foo (x)
(if (equal 0 x)
(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!