Make-event
Evaluate (expand) a given form and then evaluate the result
Make-event is a utility for generating events. It
provides a capability not offered by Lisp macros (see defmacro), as it
allows access to the ACL2 state and logical world. In essence,
the expression (make-event form) replaces itself with the result of
evaluating form — let's call that result ev — as though
one had submitted ev instead of the make-event call. For example,
(make-event (quote (defun f (x) x))) is equivalent to the event (defun
f (x) x).
We assume basic familiarity with the ACL2 state. For relevant
background, see state and perhaps see programming-with-state.
There are several simple examples below. For examples that can give
additional insight into the use of make-event for tool development, see
make-event-example-1 and make-event-example-2. Also see the
make-event/ subdirectory of the ACL2 community-books for more
examples, for example, books/make-event/search-generation.lisp.
We break this documentation into the following sections.
- Introduction
- Detailed Documentation
- Error Reporting
- Restriction to Event Contexts
- Examples Illustrating How to Access State
- Advanced Expansion Control
We begin with an introduction, which focuses on examples and introduces the
key notion of ``expansion phase''.
Introduction
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 state.
Suppose for example that we want to define a constant *world-length*,
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 make-event call
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
*world-length*.
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 the formal parameter
"STATE" is bound to the syntactic object in the macro call, not to the
actual ACL2 state; see defmacro. You can try to experiment with
other such direct methods to define a macro that accesses the ACL2 state, but
they won't work.
Instead, however, you can use the approach illustrated by the
make-event example above to define the desired macro, as follows.
(defmacro define-world-length-constant (name)
`(make-event (list 'defconst ',name (length (w state)))))
Here is a log that may help to explain this macro, assuming it has been
defined as displayed just above.
ACL2 !>:trans1 (define-world-length-constant *foo*)
(MAKE-EVENT (LIST 'DEFCONST
'*FOO*
(LENGTH (W STATE))))
ACL2 !>(LIST 'DEFCONST
'*FOO*
(LENGTH (W STATE)))
(DEFCONST *FOO* 109707)
ACL2 !>
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.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
*FOO*
ACL2 !>*foo*
109707
ACL2 !>:pe *foo*
2:x(DEFINE-WORLD-LENGTH-CONSTANT *FOO*)
> (DEFCONST *FOO* 109707)
ACL2 !>(length (w state))
109713
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*
109713
ACL2 !>:pe *bar*
3:x(DEFINE-WORLD-LENGTH-CONSTANT *BAR*)
> (DEFCONST *BAR* 109713)
ACL2 !>(length (w state))
109719
ACL2 !>
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 ACL2 world at all, but instead saves the length of the
world into a state global variable (see assign).
(make-event
(er-progn (assign my-world-length (length (w state)))
(value '(value-triple nil))))
Notice that this time, the value returned by the expansion phase is not a
single value; rather, it is an error-triple 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-event call above is to change the
state by associating the length of the current logical world with the
state global, 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))
109700
ACL2 !>(make-event
(er-progn (assign my-world-length (length (w state)))
(value '(value-triple nil))))
Summary
Form: ( MAKE-EVENT (ER-PROGN ...))
Rules: NIL
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
NIL
ACL2 !>(length (w state))
109700
ACL2 !>:pbt 0
0:x(EXIT-BOOT-STRAP-MODE)
ACL2 !>
When make-event is invoked by a book, it is expanded during book
certification but not, by default, when the book is included. Consider again
the example (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 length at include-book time. That is because the expansion,
(DEFCONST *FOO* 109700), is recorded in the book's certificate and
re-used during a subsequent include-book.
However, the keyword :check-expansion may be given the value t so
that the expansion is done even during include-book, which comes with a
check that the result is the same as it was during book certification. This
keyword 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 certify-book or during include-book.
(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)
Detailed Documentation
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)
General Form:
(make-event form
:CHECK-EXPANSION chk
:ON-BEHALF-OF obj
:EXPANSION? form
:SAVE-EVENT-DATA save)
where chk is nil (the default), t, or the intended
``expansion result'' from the evaluation of form (as explained below);
obj is an arbitrary ACL2 object, used only in reporting errors in
expansion, i.e., in the evaluation of form; and save is arbitrary but is
considered only as either nil or non-nil. The :EXPANSION?
keyword is discussed in the final section, on Advanced Expansion Control. See
make-event-details for discussion of the :ON-BEHALF-OF
and :SAVE-EVENT-DATA keywords.
We strongly recommend that you browse some .lisp files in the
community books directory books/make-event/. You may even find it
helpful, in order to understand make-event, to do so before continuing to
read this documentation. You may also find it useful to browse community book
books/std/testing/eval.lisp, which contains definitions of macros
must-succeed and must-fail that are useful for testing and are used
in many books in the books/make-event/ directory, especially
eval-tests.lisp. Another example, books/make-event/defrule.lisp,
shows how to use macros whose calls expand to make-event forms, which in
turn can generate events. For more examples, see file
books/make-event/Readme.lsp. Other than the examples, the explanations
here should suffice for most users. If you want explanations of subtler
details, see make-event-details.
Note that make-event is generally legal only where an embedded event
form is expected: essentially, at the top level of a book or the
read-eval-print loop, possibly within surrounding calls of make-event or
of event constructors such as progn and encapsulate. For
details 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.'' The final section, on Advanced
Expansion Control, will generalize these processes in a way that we ignore for
now.
``is evaluated'' — The argument can be any expression, which is
evaluated as would be any expression submitted to ACL2's top level loop.
Thus, state and user-defined 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 state global 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
state global 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 during expansion (see ld-skip-proofsp) if
keyword :CHECK-EXPANSION is supplied a non-nil value or a certain
attachment is made (see (4) below).
``expansion result'' — The above expansion may result in an ordinary
(non-state, non-stobj) value, which we call the ``expansion
result.'' Or, expansion may result in a multiple value of the form (mv erp
val state), or, more generally, (mv erp val state stobj-1 ... stobj-k)
where each stobj-i is a stobj; then the expansion result is
val unless erp is not nil, in which case there is no expansion
result, and the original make-event evaluates to a soft error. In either
case (single or multiple value), either val is an embedded event form
(see embedded-event-form), or else the original make-event
evaluates to a soft error, printed as described under ``Error Reporting''
below.
(Technical remark: The expansion result described above may be modified
for include-book, add-include-book-dir, and add-include-book-dir!, replacing book-names to indicate full-book-names. For further details see comments in source function
make-include-books-absolute. End of technical remark.)
``evaluated again'' — the expansion result is evaluated in place of
the original make-event.
The expansion process can invoke subsidiary calls of make-event, and
the expansion result can (perhaps after macroexpansion) be a call of
make-event. It can be useful to track all these make-event calls.
The state global variable make-event-debug may be set to a
non-nil value, for example (assign make-event-debug t), in order to
see a trace of the expansion process, where a level is displayed (as in
``3>'') to indicate the depth of subsidiary expansions.
Expansion of a make-event call will yield an event that replaces the
original make-event call. In particular, if you put a make-event
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.
A make-event call generates a ``make-event replacement'' that may
be stored by the system. In the simplest case, this replacement is the
expansion result. When a book is certified, these replacements are stored in
a book's certificate (technically, in the :EXPANSION-ALIST field). Thus,
although the book is not textually altered during certification, one may
imagine a ``book expansion'' corresponding to the original book, in which
events are substituted by replacements that were generated during the proof
phase of certification. A subsequent include-book will then include
the book expansion corresponding to the indicated book. When a book is
compiled during 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)), and is followed by (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.
A make-event replacement might not be the expansion when either of the
keyword arguments :CHECK-EXPANSION or :EXPANSION? is supplied. We
deal with the latter in the final section, on Advanced Expansion Control. If
:CHECK-EXPANSION t is supplied and the expansion is exp, then the
replacement is obtained from the original make-event call, by
substituting exp for t as the value of keyword
:CHECK-EXPANSION. Such a make-event call — during the second
pass of an encapsulate, or during event processing on behalf of include-book other than when including a book near the end of its
certification process — will do the expansion again and check that the
expansion result is equal to the original expansion result, exp. In the
unusual case that you know the expected expansion result, res, you can
specify :CHECK-EXPANSION res in the first place, so that the check is
also done during the initial evaluation of the make-event form.
IMPORTANT BUT OBSCURE DETAIL: 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-nil :CHECK-EXPANSION argument causes include-book to 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: when the expansion
result is a local event, then the make-event replacement is
(local (value-triple :ELIDED)).
The notion of ``expansion'' and ``replacement'' extend 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 :here
The above call of pe shows that the form (my-mac) has a
make-event expansion (and replacement) of (DEFUN FOO (X) X):
(ENCAPSULATE NIL
(DEFMACRO MY-MAC
NIL
'(MAKE-EVENT '(DEFUN FOO (X) X)))
(DEFUN FOO (X) X))
Error Reporting
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
value (mv erp val state ...) where erp is not nil. If erp
is a string, then that string is printed in the error message. If erp is
a cons pair whose car is a string, then the error prints
"~@0" with #\0 bound to that cons pair; see fmt. Any
other non-nil value of erp causes a generic error message to be
printed.
Restriction to Event Contexts
A make-event call must occur either at the top level, or during
make-event expansion, or as an argument of an event constructor. We
explain in more detail below. This restriction is imposed to enable ACL2 to
track expansions produced by make-event.
The 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: a make-event call that is not itself evaluated during
make-event expansion is subject to the following requirement. After
macroexpansion has taken place, such a make-event call 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.)
- A form submitted at the top level, or more generally, supplied to a call
of ld, is in an event context.
- A form occurring at the top level of a book is in an event context.
- If (local x1) is in an event context, then so is
x1.
- If (skip-proofs x1) is in an event context, then so is
x1.
- If (make-event x ...) is in an event context and its
expansion x1 is an embedded event form, then x1 is in an event
context.
- If (with-output ... x1), (with-prover-step-limit ... x1 ...), or (with-prover-time-limit ... x1) is in an event context, then so is
x1.
- For any call of progn or progn!, each of its arguments is
in an event context.
- For any call of encapsulate, each of its arguments except the
first (the signature list) is in an event context.
- If (RECORD-EXPANSION x1 x2) is in an event context, then x1 and
x2 are in event contexts. Note: record-expansion is intended for
use only by the implementation.
Low-level remark, for system implementors. There is the one exception to
the above restriction: a single state-global-let* form immediately
under a 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.
Avoiding large make-event forms in certificate files
The certificate file for a book contains expansions of
make-event forms from the book. (Those interested may find details about
this in an Implementation Note about ``The book expansion'' in the
documentation topic, make-event-details.) Those expansions can be very
large if one is not careful. Consider the difference between the following
two events.
(make-event
`(defconst *foo* ,(length (w state))))
(make-event
`(defconst *foo* (length ',(w state))))
The first generates an expansion such as (defconst *foo* 122700)
(where the numeric value depends on the world in which the
make-event form is evaluated). The second, however, generates an
expansion of the form (defconst *foo* (length '<wrld>)), where <wrld
is an ACL2 world — a very large structure. The .cert file for a
book containing the second form will therefore contain many megabytes.
Moreover, with the second form the length of that world will need to be
computed when the book is included (which may be fast, but could be slow for a
different such computation).
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. Let us look at some examples and then consider a
restriction for many built-in state globals.
First consider the following. Notice that expansion modifies a state
global, my-global, during make-event expansion (see assign);
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 !>
Because make-event creates event forms that can go into books and encapsulate events, you can use make-event forms such
as those above to modify the ACL2 state using books and
encapsulate events. The most common way to do this is for the
make-event expansion to be a trivial event form such as (value-triple
nil), such as the following.
(make-event (er-progn (assign my-list-of-10 (make-list 10))
(value '(value-triple nil))))
The desired effect will take place during calls of certify-book,
but it will generally not take place during include-book on a
certified book because the expansion is evaluated (it is stored in the book's
certificate for this purpose), but the expansion is merely
(value-triple nil). To ensure that the original make-event call is
evaluated even when including the book, use :check-expansion t, for
example as follows.
(make-event (er-progn (assign my-list-of-10 (make-list 10))
(value '(value-triple nil)))
:check-expansion t)
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 !>
Many built-in state globals revert after expansion. If your own
state global (like my-global above) can be set during expansion, then the
new value will persist. But that persistence will fail for many state
globals, specifically, those that are stored in the list,
*protected-system-state-globals*. We advise users not to assume
that system state modifications, such as the state of guard-checking, will
persist after executing a make-event form; persistence depends on the
relevant state globals not being in the list,
*protected-system-state-globals*.
That advice may suffice for most users. But if you want to understand the
point above more deeply, then consider the following example.
(make-event
(er-progn (set-guard-checking :none) ; sets state global 'guard-checking-on
(assign my-global (car 3))
(value (list 'value-triple (@ my-global)))))
This make-event form succeeds and afterwards, the value of (@
my-global) is nil, which of course is the value expected after the call
above of assign. However, the value of (@ guard-checking-on)
after executing this make-event form is t, not :none. That is
because the symbol guard-checking-on belongs to the list of symbols
stored in the constant, *protected-system-state-globals*, and thus the
value of the state global guard-checking-on is reverted to its initial
value (which was assume here is the default, t) after the make-event
form completes execution.
Remarks on *Protected-system-state-globals* for advanced
users.
- The constant *protected-system-state-globals* is defined to include
all built-in state globals, except for those that the ACL2 implementors
have decided can safely retain values set during make-event expansion.
If you find state globals that you would like to be added to this list of
exceptions, please contact the ACL2 implementors. Note for example that it
would not be safe to allow guard-checking-on as an exception, since ACL2
relies on the persistence of this state global's value after each event
(for explanation, see the Essay on Guard Checking in the ACL2 sources).
- As noted in a comment in the example above, the macro set-guard-checking sets the state global, 'guard-checking-on. A natural
question is how one might know this. For most ACL2 users (one might say,
traditional ACL2 users), it should suffice simply not to expect system state
modifications (like the state of guard-checking) to persist after executing a
make-event form. For system implementors, one however needs to work with
the ACL2 system by looking at the definition of the utility — in this
example, set-guard-checking — or at the least, get a sense of its
expansion by using macroexpansion (for example see trans1).
Advanced Expansion Control
We conclude this documentation section by discussing additional
control over make-event expansion. The discussion below is split into
the following parts; further discussion follows. The first three parts are
illustrated in community book
books/make-event/make-event-keywords-or-exp.lisp.
(1) The value produced by expansion may have the form (:DO-PROOFS
exp), which specifies exp as the expansion result, to be evaluated
without skipping proofs even when including a book.
(2) The value produced by expansion may have the form (:OR exp-1
... exp-k), which specifies that the first form exp-i to evaluate
without error is the expansion result.
(3) The keyword argument :EXPANSION? can serve to eliminate the
storing of make-event replacements, as described above for the ``book
expansion'' of a book.
(4) In contexts where proofs are normally skipped (see ld-skip-proofsp), the expansion phase normally takes place with proofs
skipped unless the :CHECK-EXPANSION keyword is supplied a non-nil
value. However, proofs can be made to take place unconditionally during the
expansion phase by using an attachment, as discussed below.
We now elaborate on each of these.
(1) :DO-PROOFS ``call'' produced by expansion.
We have discussed the expansion result produced by the expansion phase of
evaluating a make-event call. However, if the expansion phase produces
an expression of the form (:DO-PROOFS exp), then the expansion result is
actually exp. The :DO-PROOFS wrapper indicates that even if proofs
are currently being skipped (see ld-skip-proofsp), then evaluation of
exp should take place with proofs not skipped. For example, proofs will
be performed when evaluating the make-event expansion, namely the
indicated defthm event, in the following example.
(set-ld-skip-proofsp t state)
(make-event '(:DO-PROOFS
(defthm app-assoc (equal
(append (append x y) z)
(append x y z)))))
Note that such use of :DO-PROOFS causes proofs to be performed when
evaluating the expansion while including an uncertified book. But when
including a certified book, then unless :CHECK-EXPANSION is supplied a
non-nil value, the make-event replacement will just be the
expansion, which does not include the :DO-PROOFS wrapper and hence will
be evaluated with proofs skipped.
(2) :OR ``call'' produced by expansion.
There may be times where you want to try different expansions. For
example, the community book books/make-event/proof-by-arith.lisp attempts
to admit a given event, which we'll denote EV, by trying events of the
following form as BOOK varies over different community books.
(encapsulate
()
(local (include-book BOOK :DIR :SYSTEM))
EV)
A naive implementation of this macro would evaluate all such encapsulate events until one succeeds, and then return that successful event
as the expansion. Then that event would need to be evaluated again! With
some hacking one could avoid that re-evaluation by using skip-proofs,
but that won't work if you are trying to create a certified book without
skipped proofs. Instead, the implementation creates an expansion of the form
(:OR ev-1 ev-2 ... ev-k), where the list (ev-1 ev-2 ... ev-k)
enumerates the generated encapsulate events. In general, for this
``disjunctive case'' of a result from expansion, each ev-i is evaluated
in sequence, and the first that succeeds without error is considered to be the
expansion result — and a repeat evaluation is avoided. If evaluation of
each ev-i results in an error, then so does the make-event call.
This special use of :OR in a value produced by expansion does not
permit nesting such as (:OR ev-1 (:OR ev-2 ev-3)). That is, when an
expansion result is (:OR ev-1 ev-2 ... ev-k), none of the ev-i may
be of the form (:OR ...). Note that it is allowed for ev-i to be a
call of make-event, even one involving this special use of :OR. If
ev-i is (:DO-PROOFS ev-i'), then ev-i' is considered to be
the expansion in place of ev-i.
(3) The :EXPANSION? keyword argument.
If keyword argument :EXPANSION? has a nonnil value, then the
:CHECK-EXPANSION keyword must be omitted or have value nil or
t, hence not a cons pair.
The idea of the :EXPANSION? keyword is to give you a way to avoid
storing expansion results in a book's certificate. Roughly speaking,
when the expansion result matches the value of :EXPANSION?, then no
expansion result is stored for the event by book certification; then when the
book is later included, the value of :EXPANSION? is used as the
expansion, thus bypassing the expansion phase. One could say that the event
is its own make-event replacement, but it is more accurate to say that there
is no make-event replacement at all, since nothing is stored in the
certificate for this event. Below, we elaborate on make-event replacements
when :EXPANSION? is used and also discuss other properties of this
keyword.
We modify the notion of ``expansion result'' for make-event forms to
comprehend the use of the :EXPANSION? keyword. For that purpose, let's
consider a call of make-event to be ``reducible'' if it has an
:EXPANSION? keyword with non-nil value, exp, and its
:CHECK-EXPANSION keyword is missing or has value nil, in which case
the ``reduction'' of this make-event call is defined to be exp. The
expansion result as originally defined is modified by the following
``recursive reduction'' process: recur through the original expansion, passing
through calls of local, skip-proofs, with-output,
with-prover-step-limit, and with-prover-time-limit, and
replacing (recursively) any reducible call of make-event by its
reduction. Furthermore, we refer to two forms as ``reduction equivalent'' if
their recursive reductions are equal. Note that the recursive reduction
process does not pass through progn or encapsulate, but that
process is applied to the computation of expansions for their subsidiary
make-event calls.
To explain further the effect of :EXPANSION? exp, we split into the
following two cases.
Case 1: Evaluation is not taking place when including a book or
evaluating the second pass of an encapsulate event; more precisely,
the value of (ld-skip-proofsp state) is not the symbol INCLUDE-BOOK.
There are two subcases.
- Case 1a: The expansion result is not reduction-equivalent to exp.
Then the make-event call is processed as though the :EXPANSION?
keyword had been omitted.
- Case 2a: The expansion result is reduction-equivalent to exp. Then
there is no make-event replacement for this call of make-event; no
replacement will be put into the certificate file for a book containing
this make-event call. When that book is subsequently included, the
original form will be evaluated in the manner described in the next
case.
Case 2: Evaluation is taking place when including a book or evaluating
the second pass of an encapsulate event; more precisely, the value of
(ld-skip-proofsp state) is the symbol INCLUDE-BOOK. Then the
expansion is exp. The expansion phase is skipped unless
:CHECK-EXPANSION is t.
The :EXPANSION? keyword can be particularly useful in concert with the
disjunctive (``:OR'') case (2) discussed above. Suppose that expansion
produces a value as discussed in (2) above, (:OR exp-1 ... exp-k). If
one of these expressions exp-i is more likely than the others to be the
expansion, then you may wish to specify :EXPANSION? exp-i, as this will
avoid storing a make-event replacement in that common case. This could
be useful if the expressions are large, to avoid enlarging the certificate file for a book containing the make-event call.
It is legal to specify both :EXPANSION? exp and :CHECK-EXPANSION
t. When either (ld-skip-proofsp state) is the symbol
INCLUDE-BOOK, or evaluation is taking place in raw Lisp, then this
combination is treated the same as if :EXPANSION? is omitted and the
value of :CHECK-EXPANSION is exp. Otherwise, this combination is
treated the same as :CHECK-EXPANSION t, modified to accommodate the
effect of :EXPANSION? as discussed above: if the expansion is indeed the
value of :EXPANSION?, then no make-event replacement is
generated.
(4) Unconditionally enabling proofs during the expansion phase using an
attachment.
Proofs are normally skipped during the expansion phase unless the
:CHECK-EXPANSION keyword is supplied a non-nil value. To cause
proofs to take place unconditionally during the expansion phase, evaluate one
of the following two forms, as explained below.
(defattach (always-do-proofs-during-make-event-expansion
constant-t-function-arity-0)
:system-ok t)
(defattach (always-do-proofs-during-make-event-expansion
constant-all-function-arity-0)
:system-ok t)
The first of these is probably preferred in most cases, since it does not
have any effect while evaluating an include-book form (more precisely,
when (ld-skip-proofsp state) is 'include-book). The second removes
that restriction.
To restore the default behavior, evaluate the following.
(defattach (always-do-proofs-during-make-event-expansion
constant-nil-function-arity-0)
:system-ok t)
(If you would like an explanation of defattach in general, see defattach.)
Subtopics
- Make-event-details
- Details on make-event expansion
- Make-event-example-2
- An example use of make-event
- Make-event-example-1
- An example use of make-event
- Make-event-example-3
- Using make-event to define thm
- Make-event-terse
- A variant of make-event with terser screen output.
