MAKE-EVENT

evaluate (expand) a given form and then evaluate the result 
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 the ACL2 state and logical world. In essence, the expression (make-event form) replaces itself with the result of evaluating form, say, ev, as though one had submitted ev instead of the make-event call. But the evaluation of form may involve state and even modify state, for example by attempting to admit some definitions and theorems. Make-event protects the ACL2 logical world so that it is restored after form is evaluated, before ev is submitted.

Some Related Topics

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 chk is nil (the default), t, or the intended ``expansion result'' from the evaluation of form (as explained below); and if supplied, obj is 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 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. For example, eval.lisp contains definitions of macros must-succeed and must-fail that are useful for testing and are used in many other books in that directory, especially eval-tests.lisp. Another example, 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 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.

Note that 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, 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 at the start of expansion (see ld-skip-proofsp), because an anticipated use of make-event is 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-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 stobj-1 ... stobj-k), where k may be 0; in fact the most common case is probably (mv erp val state). In that case, if erp is not nil, then there is no expansion result, and the original make-event evaluates to a soft error. If however erp is nil, then the resulting value is val. Moreover, val must be an embedded event form (see embedded-event-form); otherwise, the original make-event evaluates 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 make-event.

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 ld to evaluate some 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 ``3>'') indicates the depth of expansions in progress.

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.

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 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)), 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.

The preceding paragraph begins with ``by default'' because if you specify :check-expansion t, then subsequent evaluation of the same make-event 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, res, you can specify :check-expansion res. This will will cause a check that every subsequent expansion result for the make-event form is res, 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-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 for book certificates: a local event arising from make-event expansion is replaced in that expansion by (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 :here
The above call of pe shows that the form (my-mac) has a make-event expansion of (DEFUN FOO (X) X): 
(ENCAPSULATE NIL
             (DEFMACRO MY-MAC
                       NIL
                       '(MAKE-EVENT '(DEFUN FOO (X) X)))
             (RECORD-EXPANSION (MY-MAC)
                               (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 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 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: after macroexpansion has taken place, 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.)

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.

o If (LOCAL x1) is in an event context, then so is x1.

o If (SKIP-PROOFS x1) is in an event context, then so is x1.

o 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.

o If (WITH-OUTPUT ... x1), (WITH-PROVER-STEP-LIMIT ... x1 ...), or (WITH-PROVER-TIME-LIMIT ... x1) is in an event context, then so is x1.

o Given a call of PROGN or PROGN! in an event context, each of its arguments is in an event context.

o Given a call of ENCAPSULATE in an event context, each of its arguments except the first (the signature list) is in an event context.

o 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, which imposes the additional restriction that x1 and its subsidiary make-event calls (if any) must specify a :check-expansion argument 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 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 ...))
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 my-global during 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.