Make-event-details
Details on make-event expansion
The normal user of make-event can probably ignore this
section, but we include it for completeness. We assume that the reader has
read and understood the basic documentation for make-event (see make-event), but we begin below with a summary of expansion.
Introduction
Here is a summary of how we handle expansion involving make-event
forms.
(make-event form :check-expansion nil)
This shows the :check-expansion default of nil, and is typical
user input. We compute the expansion exp of form, which is the
expansion of the original make-event expression and is evaluated in place
of that expression.
(make-event form :check-expansion t)
The user presumably wants it checked that the expansion doesn't change in
the future, in particular during include-book. If the expansion of
form is exp, then we will evaluate exp to obtain the value as
before, but this time we record that the expansion of the original
make-event expression is (make-event form :check-expansion exp)
rather than simply exp.
(make-event form :check-expansion exp) ; exp a cons
This is generated for the case that :check-expansion is t, as
explained above. Evaluation is handled as described in that above case,
except here we check that the expansion result is the given exp.
(Actually, the user is also allowed supply such a form.) The original
make-event expression does not undergo any expansion (intuitively, it
expands to itself).
Now let us take a brief look at how we expand progn and encapsulate forms. More details are found further below (see ``Detailed
semantics'').
(progn ... (make-event form ...) ...)
The expansion is obtained, roughly speaking, by replacing the
make-event form by its expansion, exp, except that if
:check-expansion exp is supplied explicitly, then no such replacement
takes place.
Expansion for (encapsulate ... (make-event form ...) ...) is similar
to the case for progn, except that if the expansion of form is
exp, then what is stored is (record-expansion (make-event form ...)
exp). Also as for progn, the exception is that when
:check-expansion exp is supplied explicitly, no such replacement takes
place. Here, record-expansion is a macro that simply returns its second
argument, but is used for checking redundancy of encapsulate forms (see
redundant-encapsulate).
Certain ``wrappers'' around a make-event are restored as the last part
of the expansion process, in particular for make-event calls that are
inside calls of encapsulate or progn, as well as in events
processed during a book's certification, including portcullis commands
from the certification world. For example, if you evaluate a form
(local (with-prover-step-limit 100 (make-event ...))) where the
make-event call has expansion <exp>, and then you certify a book,
the book's certificate file will include among its portcullis commands
the form (local (with-prover-step-limit 100 <exp>)). Macroexpansion is
performed to determine the wrappers. The wrappers thus restored are as
follows.
local
skip-proofs
with-cbd
with-guard-checking-event
with-output
with-prover-step-limit
with-prover-time-limit
The discussion below references this process as the final expansion being
``rebuilt from'' the form.
Detailed semantics
In our explanation of the semantics of make-event, we assume
familiarity with the notion of ``embedded event form'' (see embedded-event-form).
Let's say that the ``actual embedded event form'' corresponding to a given
form is the underlying call of an ACL2 event: that is, locals are
dropped when ld-skip-proofsp is 'include-book, and macros are
expanded away, thus leaving us with a progn, a make-event, or
an event form (possibly encapsulate), any of which might have
surrounding local, skip-proofs, or with-output
calls.
Thus, such an actual embedded event form can be viewed as having the form
(rebuild-expansion wrappers base-form) where base-form is a
progn, a make-event, or an event form (possibly encapsulate),
and wrappers are (as in ACL2 source function destructure-expansion)
the result of successively removing the event form from the result of
macroexpansion, leaving a sequence of (local), (skip-proofs), and
(with-output ...) forms. In this case we say that the form
``destructures into'' the indicated wrappers and base-form, and that
it can be ``rebuilt from'' those wrappers and base-form.
Elsewhere we define the notion of the ``expansion result'' from an
evaluation (see make-event), and we mention that when expansion
concludes, the ACL2 logical world and most of the state are
restored to their pre-expansion values. Specifically, after evaluation of the
argument of make-event (even if it is aborted), the ACL2 logical world is
restored to its pre-evaluation value, as are all state global variables in the
list *protected-system-state-globals*. Thus, assignments to user-defined
state globals (see assign) do persist after expansion, since they are
not in that list.
We recursively define the combination of evaluation and expansion of an
embedded event form as shown below. We also simultaneously define the notion
of ``expansion takes place,'' which is assumed to propagate upward (in a sense
that will be obvious), such that if no expansion takes place, then the
expansion of the given form is considered to be itself. It is useful to keep
in mind a goal that we will consider later: Every make-event subterm of
an expansion result has a :check-expansion field that is a consp,
where for this purpose make-event is viewed as a macro that returns its
:check-expansion field.
If the given form is not an embedded event form, then simply cause a soft
error, (mv erp val state) where erp is not nil. Otherwise:
If the evaluation of the given form does not take place (presumably because
local events are being skipped), then no expansion takes place.
Otherwise:
Let x be the actual embedded event form corresponding to the given
form, which destructures into wrappers W and base-form B. Then the
original form is evaluated by evaluating x, and its expansion is as
follows.
If B is (make-event form :check-expansion val), then expansion
takes place if and only if val is not a consp and no error occurs,
as now described. Let R be the expansion result from protected
evaluation of form, if there is no error. R must be an embedded
event form, or it is an error. Then evaluate/expand R, where if val
is not nil then state global 'ld-skip-proofsp is initialized to
nil. (This initialization is important so that subsequent expansions are
checked in a corresponding environment, i.e., where proofs are turned on in
both the original and subsequent environments.) It is an error if this
evaluation causes an error. Otherwise, the evaluation yields a value, which
is the result of evaluation of the original make-event expression, as
well as an expansion, E_R. Let E be rebuilt from W and
E_R. The expansion of the original form is E if val is
nil, and otherwise is the result of replacing the original form's
:check-expansion field with E, with the added requirement that if
val is not t (thus, a consp) then E must equal val or
else we cause an error.
If B is (progn form1 form2 ...) (and similarly for progn!), and at least one formi has an expansion, then the expansion of
the original form is obtained by replacing each formi by its expansion
and then rebuilding the entire progn call from B.
If B is (encapsulate sigs form1 form2 ...), then after evaluating
B, the expansion of the original form is the result of rebuilding from
B, with wrappers W, after replacing each formi in B for
which expansion takes place by (record-expansion formi formi'), where
formi' is the expansion of formi. Note that these expansions are
determined as the formi are evaluated in sequence (where in the case of
encapsulate, this determination occurs only during the first pass).
Except, if no expansion takes place for any formi, then the expansion of
the original form is itself.
Otherwise, the expansion of the original form is itself.
(Optional Implementation Notes. The latest expansion of a make-event, progn, progn!, or encapsulate is
temporarily stored in state global 'last-make-event-expansion, except
that if no expansion has taken place for that form then
'last-make-event-expansion has value nil. Expansions ultimately
show up in the world's command tuples; for example, immediately after
processing a command its expansion is
(access-command-tuple-last-make-event-expansion (cddr (car (w state)))).
Top-level expansions do not include rebuilding of wrappers, although such
wrappers are restored when constructing portcullis commands as
discussed above. End of Implementation Notes.)
Similarly to the progn and encapsulate cases above, book
certification causes a book to be replaced by its so-called ``book
expansion,'' where each event ev for which expansion took place during
the proof pass of certification is replaced by its expansion, but with certain
local events elided.
Optional Implementation Note. The book expansion is actually implemented
by way of the :expansion-alist field of its certificate, which
associates 0-based positions of top-level forms in the book (not including the
initial in-package form) with their expansions. Thus, the book's
source file is not overwritten; rather, the certificate's expansion-alist is
applied when the book is included or compiled. End of Implementation
Note.
It is straightforward by computational induction to see that for any
expansion of an embedded event form, every make-event sub-event has a
consp :check-expansion field. Here, by ``sub-event'' we mean to
expand macros; and we also mean to traverse progn and encapsulate
forms as well as :check-expansion fields of make-event forms. Thus,
we will only see make-event forms with consp :check-expansion
fields in the course of include-book forms, the second pass of
encapsulate forms, and raw Lisp. This fact guarantees that an event form
will always be treated as its original expansion.
Notes on ttags
See defttag for documentation of the notion of ``trust tag''
(``ttag''). We note here that even if an event (defttag tag-name) for
non-nil tag-name is admitted only during the expansion phase of a
make-event form, then such expansion will nevertheless still cause
tag-name to be recorded in the logical world (assuming that the
make-event form is admitted). So in order to certify such a book, a
suitable :ttags argument must be supplied; see certify-book.
ACL2 does provide a way to avoid the need for :ttags arguments in such
cases. The idea is to certify a book twice, where the results of
make-event expansion are saved from the first call of certify-book and provided to the second call. See set-write-ACL2x.
Finally, we discuss a very unusual case where certification does not
involve trust tags but a subsequent include-book does involve trust
tags: a make-event call specifying :check-expansion t, whose
expansion generates a defttag event during include-book but
not certify-book. Consider the following book.
(in-package "ACL2")
(make-event
(er-progn
(if (@ skip-notify-on-defttag) ; non-nil when including a certified book
(pprogn
(fms "Value of (@ skip-notify-on-defttag): ~x0~|"
(list (cons #0 (@ skip-notify-on-defttag)))
*standard-co* state nil)
(encapsulate
()
(defttag :foo)
(value-triple "Imagine something bad here!")))
(value nil))
(value '(value-triple :some-value)))
:check-expansion t)
This book certifies successfully without the need for a :ttags
argument for certify-book. Indeed, the above book's certificate does not specify :foo as a trust tag associated with the
book, because no defttag event was executed during book certification.
Unfortunately, if we try to include this book without specifying a value of
:ttags that allows :foo, book inclusion will cause executing of the
above defttag. If that inclusion happens in the context of certifying
some superior book and the appropriate :ttags arguments have not been
provided, that certification will fail.
Expansion errors and the :ON-BEHALF-OF keyword
Consider the case that expansion returns an error-triple (mv erp
val state), where erp is not nil. Then make-event may
conclude with an error message, as follows.
- If keyword :ON-BEHALF-OF has value :quiet! then there is no such
concluding error message.
- Otherwise, if erp is a string, then the concluding error message is
produced by printing erp with the call (er soft ctx erp), where
ctx is the context (see ctx).
- Otherwise, if erp is a message (see msg), then the concluding
error message is produced by the call (er soft ctx "~@0" erp), where
ctx is the context (see ctx).
- Otherwise, if keyword :ON-BEHALF-OF has value :quiet then there
is no concluding error message.
- Otherwise, if keyword :ON-BEHALF-OF is not supplied or has value
nil — so we are now in the typical case — then the concluding
error message is ``Error in MAKE-EVENT from expansion of:'' followed by the
form.
- Otherwise, keyword :ON-BEHALF-OF has a value x other than
:quiet!, :quiet, or nil, in which case the concluding error
message is as just above, except that after ``Error in MAKE-EVENT'' is
stated ``on behalf of'' followed by x.
Note that errors generated during expansion are not affected by the cases
above; those only control the concluding error message, if any.
