Major Section: EVENTS
Make-event is a utility for generating events. It provides a
capability not offered by Lisp macros (see defmacro), as it allows access to
state and logical world. In essence, the expression
(make-event form) replaces itself with the result of evaluating
ev, as though one had submitted
ev instead of the
call. For example,
(make-event (quote (defun f (x) x))) is equivalent to
(defun f (x) x).
We break this documentation into the following sections.
Restriction to Event Contexts
Examples illustrating how to access state
We begin with an informal introduction, which focuses on examples and introduces the key notion of ``expansion phase''.
Make-event is particularly useful for those who program using the ACL2
state; see programming-with-state. That is because the evaluation of
form may read and even modify the ACL2
Suppose for example that we want to define a constant
that is the length of the current ACL2 world. A
make-event form can
accomplish this task, as follows.
ACL2 !>(length (w state)) 98883 ACL2 !>(make-event (list 'defconst '*world-length* (length (w state)))) Summary Form: ( DEFCONST *WORLD-LENGTH* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Summary Form: ( MAKE-EVENT (LIST ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) *WORLD-LENGTH* ACL2 !>*world-length* 98883 ACL2 !>(length (w state)) 98890 ACL2 !>How did this work? First, evaluation of the form
(list 'defconst '*world-length* (length (w state)))returned the event form
(defconst *world-length* 98883). Then that event form was automatically submitted to ACL2. Of course, that changed the ACL2 logical world, which is why the final value of
(length (w state))is greater than its initial value.
The example above illustrates how the evaluation of a
takes place in two phases. The first phase evaluates the argument of the
call, in this case
(list 'defconst '*world-length* (length (w state))),
to compute an event form, in this case
(defconst *world-length* 98883).
We call this evaluation the ``expansion'' phase. Then the resulting event
form is evaluated, which in this case defines the constant
Now suppose we would like to introduce such a
defconst form any time we
like. It is common practice to define macros to automate such tasks. Now we
might be tempted simply to make the following definition.
; WRONG! (defmacro define-world-length-constant (name state) (list 'defconst name (length (w state))))But ACL2 rejects such a definition, because a macro cannot take the ACL2 state as a parameter; instead, the formal parameter to this macro named
"STATE"merely represents an ordinary object. You can try to experiment with other such direct methods to define such a macro, but they won't work.
Instead, however, you can use the approach illustrated by the
example above to define the desired macro, as follows.
(defmacro define-world-length-constant (name) `(make-event (list 'defconst ',name (length (w state)))))Here are example uses of this macro.
ACL2 !>(define-world-length-constant *foo*) Summary Form: ( DEFCONST *FOO* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Summary Form: ( MAKE-EVENT (LIST ...)) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *FOO* ACL2 !>*foo* 98891 ACL2 !>:pe *foo* 2:x(DEFINE-WORLD-LENGTH-CONSTANT *FOO*) > (DEFCONST *FOO* 98891) ACL2 !>(length (w state)) 98897 ACL2 !>(define-world-length-constant *bar*) Summary Form: ( DEFCONST *BAR* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Summary Form: ( MAKE-EVENT (LIST ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) *BAR* ACL2 !>*bar* 98897 ACL2 !>:pe *bar* 3:x(DEFINE-WORLD-LENGTH-CONSTANT *BAR*) > (DEFCONST *BAR* 98897) ACL2 !>(length (w state)) 98903 ACL2 !>
Finally, we note that the expansion phase can be used for computation that has side effects, generally by modifying state. Here is a modification of the above example that does not change the world at all, but instead saves the length of the world in a state global.
(make-event (pprogn (f-put-global 'my-world-length (length (w state)) state) (value '(value-triple nil))))Notice that this time, the value returned by the expansion phase is not an event form, but rather, is an error triple (see error-triples) whose value component is an event form, namely, the event form
(value-triple nil). Evaluation of that event form does not change the ACL2 world (see value-triple). Thus, the sole purpose of the
make-eventcall above is to change the state by associating the length of the current logical world with the state global named
'my-world-length. After evaluating this form,
(@ my-world-length)provides the length of the ACL2 world, as illustrated by the following transcript.
ACL2 !>:pbt 0 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(length (w state)) 98883 ACL2 !>(make-event (pprogn (f-put-global 'my-world-length (length (w state)) state) (value '(value-triple nil)))) Summary Form: ( MAKE-EVENT (PPROGN ...)) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) NIL ACL2 !>(length (w state)) 98883 ACL2 !>:pbt 0 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>
make-event is invoked by a book, it is expanded during book
certification but not, by default, when the book is included. So for the
(define-world-length-constant *foo*) given above, if that form is
in a book, then the value of
*foo* will be the length of the world at the
time this form was invoked during book certification, regardless of world
include-book time. (The expansion is recorded in the book's
certificate, and re-used.) To overcome this default, you can specified
:CHECK-EXPANSION t. This will cause an error if the
expansion is different, but it can be useful for side effects. For example,
if you insert the following form in a book, then the length of the world will
be printed when the form is encountered, whether during
(make-event (pprogn (fms "Length of current world: ~x0~|" (list (cons #\0 (length (w state)))) *standard-co* state nil) (value '(value-triple nil))) :check-expansion t)
Examples: ; Trivial example: evaluate (quote (defun foo (x) x)) to obtain ; (defun foo (x) x), which is then evaluated. (make-event (quote (defun foo (x) x))) ; Evaluate (generate-form state) to obtain (mv nil val state), and ; then evaluate val. (Generate-form is not specified here, but ; imagine for example that it explores the state and then generates ; some desired definition or theorem.) (make-event (generate-form state)) ; As above, but make sure that if this form is in a book, then when ; we include the book, the evaluation of (generate-form state) ; should return the same value as it did when the book was ; certified. (make-event (generate-form state) :check-expansion t) ; As above (where the :check-expansion value can be included or ; not), where if there is an error during expansion, then the error ; message will explain that expansion was on behalf of the indicated ; object, typically specified as the first argument. (make-event (generate-form state) :on-behalf-of (generate-form state)) General Form: (make-event form :check-expansion chk :on-behalf-of obj)where
t, or the intended ``expansion result'' from the evaluation of
form(as explained below); and if supplied,
objis an arbitrary ACL2 object, used only in reporting errors in expansion, i.e., in the evaluation of form.
We strongly recommend that you browse some
.lisp files in the community
books/make-event/. You may even find it helpful, in
order to understand
make-event, to do so before continuing to read this
documentation. For example,
eval.lisp contains definitions of macros
must-fail that are useful for testing and are used
in many other books in that directory, especially
defrule.lisp, shows how to use macros whose calls expand
make-event forms, which in turn can generate events. For more
examples, see file
Readme.lsp in the above directory. Other than the
examples, the explanations here should suffice for most users. If you want
explanations of subtler details, see make-event-details.
make-event may only be used at the ``top level'' or where an
event is expected. See the section ``Restriction to Event Contexts'', below.
Make-event is related to Lisp macroexpansion in the sense that its
argument is evaluated to obtain an expansion result, which is evaluated
again. Let us elaborate on each of these notions in turn: ``is evaluated,''
``expansion result'', and ``evaluated again.''
``is evaluated'' -- The argument can be any expression, which is evaluated as would be any expression submitted to ACL2's top level loop. Thus,
stobjs may appear in the form supplied to
make-event. Henceforth, we will refer to this evaluation as ``expansion.'' Expansion is actually done in a way that restores ACL2's built-in
stateglobal variables, including the logical world, to their pre-expansion values (with a few exceptions -- see make-event-details -- and where we note that changes to user-defined
stateglobal variables (see assign) are preserved). So, for example, events might be evaluated during expansion, but they will disappear from the logical world after expansion returns its result. Moreover, proofs are enabled by default at the start of expansion (see ld-skip-proofsp), because an anticipated use of
make-eventis to call the prover to decide which event to generate, and that would presumably be necessary even if proofs had been disabled.
``expansion result'' -- The above expansion may result in an ordinary (non-
stobj) value, which we call the ``expansion result.'' Or, expansion may result in a multiple value of the form
(mv erp val state stobj-1 ... stobj-k), where
kmay be 0; in fact the most common case is probably
(mv erp val state). In that case, if
nil, then there is no expansion result, and the original
make-eventevaluates to a soft error. If however
nil, then the resulting value is
valmust be an embedded event form (see embedded-event-form); otherwise, the original
make-eventevaluates to a soft error. Note that error messages from expansion are printed as described under ``Error Reporting'' below.
``evaluated again'' -- the expansion result is evaluated in place of the original
Note that the result of expansion can be an ordinary event, but it can
instead be another call of
make-event, or even of a call of a macro that
expands to a call of
make-event. Or, expansion itself can cause
subsidiary calls of
make-event, for example if expansion uses
make-event forms. The state global variable
make-event-debug may be set to a non-
nil value in order to see a
trace of the expansion process, where the level shown (as in ``
indicates the depth of expansions in progress.
Expansion of a
make-event call will yield an event that replaces the
make-event call. In particular, if you put a
form in a book, then in essence it is replaced by its expansion result,
created during the proof pass of the
certify-book process. We now
elaborate on this idea of keeping the original expansion.
By default, a
make-event call in a certified book is replaced (by a
process hidden from the user, in an
:expansion-alist field of the book's
certificate) by the expansion result from evaluation of its first
argument. Thus, although the book is not textually altered during
certification, one may imagine a ``book expansion'' corresponding to the
original book in which all of the events for which expansion took place
(during the proof phase of certification) have been replaced by their
expansions. A subsequent
include-book will then include the book
expansion corresponding to the indicated book. When a book is compiled
certify-book, it is actually the corresponding book expansion,
stored as a temporary file, that is compiled instead. That temporary file is
deleted after compilation unless one first evaluates the form
(assign keep-tmp-files t). Note however that all of the original forms
must still be legal events (see embedded-event-form). So for example,
if the first event in a book is
(local (defmacro my-id (x) x)), followed
(my-id (make-event ...)), the final ``
include-book'' pass of
certify-book will fail because
my-id is not defined when the
my-id call is encountered.
The preceding paragraph begins with ``by default'' because if you specify
:check-expansion t, then subsequent evaluation of the same
call -- during the second pass of an
encapsulate or during event
processing on behalf of
include-book -- will do the expansion again
and check that the expansion result equals the original expansion result. In
the unusual case that you know the expected expansion result,
:check-expansion res. This will will cause a check that
every subsequent expansion result for the
make-event form is
including the original one. IMPORTANT NOTE: That expansion check is only
done when processing events, not during a preliminary load of a book's
compiled file. The following paragraph elaborates.
(Here are details on the point made just above, for those who use the
:check-expansion argument to perform side-effects on the state.
When you include a book, ACL2 generally loads a compiled file before
processing the events in the book; see book-compiled-file. While it is true
that a non-
:check-expansion argument causes
perform expansion of the
make-event form during event processing it does
not perform expansion when the compiled file (or expansion file; again,
see book-compiled-file) is loaded.)
ACL2 performs the following space-saving optimization for book certificates:
local event arising from
make-event expansion is replaced in that
(local (value-triple :ELIDED)).
We note that ACL2 extends the notion of ``make-event expansion'' to the case
that a call of
make-event is found in the course of macroexpansion. The
following example illustrates this point.
(encapsulate () (defmacro my-mac () '(make-event '(defun foo (x) x))) (my-mac)) :pe :hereThe above call of
peshows that the form
(DEFUN FOO (X) X):
(ENCAPSULATE NIL (DEFMACRO MY-MAC NIL '(MAKE-EVENT '(DEFUN FOO (X) X))) (RECORD-EXPANSION (MY-MAC) (DEFUN FOO (X) X)))
Suppose that expansion produces a soft error as described above. That is,
suppose that the argument of a
make-event call evaluates to a multiple
(mv erp val state ...) where
erp is not
a string, then that string is printed in the error message. If
cons pair whose
car is a string, then the error prints
#\0 bound to that
cons pair; see fmt. Any other
nil value of
erp causes a generic error message to be printed.
Restriction to Event Contexts
make-event call must occur either at the top level or as an argument of
an event constructor, as explained in more detail below. This restriction is
imposed to enable ACL2 to track expansions produced by
following examples illustrate this restriction.
; Legal: (progn (with-output :on summary (make-event '(defun foo (x) x)))) ; Illegal: (mv-let (erp val state) (make-event '(defun foo (x) x)) (mv erp val state))
More precisely: after macroexpansion has taken place, a
must be in an ``event context'', defined recursively as follows. (All but
the first two cases below correspond to similar cases for constructing
events; see embedded-event-form.)
o A form submitted at the top level, or more generally, supplied to a call of
ld, is in an event context.
o A form occurring at the top level of a book is in an event context.
x1)is in an event context, then so is
x1)is in an event context, then so is
x ...)is in an event context and its expansion
x1is an embedded event form, then
x1is in an event context.
... x1 ...), or
... x1)is in an event context, then so is
o Given a call of
PROGN!in an event context, each of its arguments is in an event context.
o Given a call of
ENCAPSULATEin an event context, each of its arguments except the first (the signature list) is in an event context.
(RECORD-EXPANSION x1 x2)is in an event context, then
x2are in event contexts. Note:
record-expansionis intended for use only by the implementation, which imposes the additional restriction that
x1and its subsidiary
make-eventcalls (if any) must specify a
:check-expansionargument that is a consp.
Low-level remark, for system implementors. There is the one exception to
the above restriction: a single
state-global-let* form immediately
progn! call. For example:
(progn! (state-global-let* <bindings> (make-event ...)))However, the following form may be preferable (see progn!):
(progn! :state-global-bindings <bindings> (make-event ...))Also see remove-untouchable for an interesting use of this exception.
Examples illustrating how to access state
You can modify the ACL2 state by doing your state-changing computation during the expansion phase, before expansion returns the event that is submitted. Here are some examples.
First consider the following. Notice that expansion modifies state global
make-event expansion, and then expansion returns a
defun event to be evaluated.
(make-event (er-progn (assign my-global (length (w state))) (value '(defun foo (x) (cons x x)))))Then we get:
ACL2 !>(@ my-global) 72271 ACL2 !>:pe foo L 1:x(MAKE-EVENT (ER-PROGN # #)) >L (DEFUN FOO (X) (CONS X X)) ACL2 !>
Here's a slightly fancier example, where the computation affects the
defun. In a new session, execute:
(make-event (er-progn (assign my-global (length (w state))) (value `(defun foo (x) (cons x ,(@ my-global))))))Then:
ACL2 !>(@ my-global) 72271 ACL2 !>:pe foo L 1:x(MAKE-EVENT (ER-PROGN # #)) >L (DEFUN FOO (X) (CONS X 72271)) ACL2 !>Note that ACL2 table events may avoid the need to use state globals. For example, instead of the example above, consider this example in a new session.
(make-event (let ((world-len (length (w state)))) `(progn (table my-table :stored-world-length ,world-len) (defun foo (x) (cons x ,world-len)))))Then:
ACL2 !>(table my-table) ((:STORED-WORLD-LENGTH . 72271)) ACL2 !>:pe foo 1:x(MAKE-EVENT (LET # #)) >L (DEFUN FOO (X) (CONS X 72271)) ACL2 !>
By the way, most built-in state globals revert after expansion. But
your own global (like
my-global above) can be set during expansion, and
the new value will persist.