		Search-engine friendly clone of the ACL2 documentation.

Make-event

Make-event-example-1

An example use of make-event

Here, we develop a reasonably self-contained example that illustrates how to use make-event to develop tools, by solving a challenge posed by Alessandro Coglio. For another such example, see make-event-example-2.

The challenge is to develop a programmatic method for solving the following sort of problem.

Create a defun form.
Submit it to ACL2, obtaining a new ACL2 state whose world includes the function just submitted.
Access various elements of this function (e.g., unnormalized body).
Create and return a new defun that's based on elements of the previous one.
Submit this new defun via a make-event, but in a state that does not include the previous defun.

We illustrate how to do this sort of thing by specifying the ``new defun that's based on elements of the previous one'' to be as follows: add the formal, y, and modify the body so that y is consed onto the old body. Of course, this is a trivial example that could be done without make-event; but we solve it in a way that shows how to solve any such problem. For simplicity, let's not worry about the case that y is already a formal of the existing defun. Here are the main steps.

(a) Submit the defun.
(b) Gather information from the resulting world. In this case, we access the formals and body of the definition.
(c) Create the desired event.

The following code does those three things, as explained in comments below, which include references to the three steps above.

(er-progn

; Each of the two forms below returns an error triple (see :DOC
; error-triple), so we can evaluate both by using er-progn, which
; returns the last (second) error triple.

 (defun foo (x) (cons x x)) ; (a)
 (let ((formals (formals 'foo (w state))) ; (b)
       (body (body 'foo nil (w state))))
   (value `(defun foo ,(cons 'y formals) ; (c)
             (cons y ,body)))))

So far so good: we have computed an error triple (mv nil val state) whose value component, val, is the desired defun form. However, that leaves us in a world that includes the first defun form. For a solution to the original challenge (for our specific case), that must not be the case, and moreover the second defun form should be included in the current world. Fortunately, make-event is perfectly suited to do both of these things. Consider the following form, which simply wraps make-event around the code displayed just above.

(make-event (er-progn
             (defun foo (x) (cons x x))
             (let ((formals (formals 'foo (w state)))
                   (body (body 'foo nil (w state))))
               (value `(defun foo ,(cons 'y formals)
                         (cons y ,body))))))

The expansion phase (see make-event) computes the new defun form — the one with the extra formal and modified body — and then that new defun form is evaluated in the original world, which does not include the first defun form.

We complete the job by making a programmatic solution, with a macro that expands to such a make-event form. We make it nice by inhibiting all output except error output.

(defmacro cons-y-onto-body (def new-name)
  `(make-event
    (with-output!
      :off :all
      :on error
      (er-progn
       ,def
       (let* ((name ',(cadr def))
              (new-name ',new-name)
              (formals (formals name (w state)))
              (body (body name nil (w state))))
         (value (list 'defun new-name (cons 'y formals)
                      (list 'cons 'y body))))))
    :on-behalf-of :quiet!))

This could be improved by doing some error checking, but we leave that as an exercise.

Below is a log, with comments added, that shows uses of the macro above.

; First we call the macro successfully.  Notice that although we inhibited
; output during the expansion phase (using with-output!), below we see output
; from the resulting new defun event.

ACL2 !>(cons-y-onto-body (defun f (x) x) new-f)

Since NEW-F is non-recursive, its admission is trivial.  We observe
that the type of NEW-F is described by the theorem (CONSP (NEW-F Y X)).
We used primitive type reasoning.

Summary
Form:  ( DEFUN NEW-F ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)

Summary
Form:  ( MAKE-EVENT (WITH-OUTPUT! :OFF ...) ...)
Rules: NIL
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
 NEW-F
ACL2 !>:pe new-f ; Check that the new definition was indeed submitted.
 L         2:x(CONS-Y-ONTO-BODY (DEFUN F # ...) NEW-F)
              
>L             (DEFUN NEW-F (Y X) (CONS Y X))
ACL2 !>:pe f ; Check that the old definition was NOT submitted.


ACL2 Error in :PE:  The object F is not a logical name.  See :DOC logical-
name.

; The defun below is ill-formed, so we get an error when it is submitted,
; during the expansion phase.  Our use of with-output! allowed error messages,
; so we see the error message in this case.

ACL2 !>(cons-y-onto-body (defun g (x) (+ y y)) new-g)


ACL2 Error in ( DEFUN G ...):  The body of G contains a free occurrence
of the variable symbol Y.


Summary
Form:  ( MAKE-EVENT (WITH-OUTPUT! :OFF ...) ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

ACL2 Error in ( MAKE-EVENT (WITH-OUTPUT! :OFF ...) ...):  See :DOC
failure.

******** FAILED ********
ACL2 !>