		Search-engine friendly clone of the ACL2 documentation.

Make-event

Make-event-example-2

An example use of make-event

Here, we develop a reasonably self-contained example that illustrates how to use make-event to develop tools. For another such example, see make-event-example-1. We thank Yan Peng for putting forward this problem.

We begin by discussing prerequisites for this presentation. Next, we present the challenge problem, followed by code that solves the problem together with an example that illustrates its use. Finally, we start from the beginning and show how to develop the solution step-by-step.

Prerequisites

We assume some general ACL2 and Common Lisp background, including familiarity with macros and backquote. But we do some programming below that goes beyond that general background in our use of the ACL2 state. See programming-with-state for relevant discussion, including state global variables, f-get-global, f-put-global, error-triples and their construction using value, value-triple, and pprogn. We also assume familiarity with both progn and the notion of legal event form; see embedded-event-form. If you are not familiar with these notions, then the discussion below might still make some sense, but you might need to read about these notions in order to complete your understanding.

Next, we present the challenge problem that we will solve below.

Challenge problem

Define a utility that evaluates a given sequence of events, even continuing past errors, which stores the list of event forms that caused errors.

Let us call this utility progn+, since it can be viewed as an enhancement of progn. So a successful solution should allow us to evaluate the following form to define function symbols f1, f2, and f3, as well as the event good-thm, and also store the events for bad-thm and bad-fn.

(progn+ (defun f1 (x) x)
        (defthm good-thm (equal 1 1) :rule-classes nil)
        (value-triple (cw "@@HI~%"))
        (defthm bad-thm (equal x y) :rule-classes nil) ; error!
        (defun f2 (x) x)
        (defun bad-fn (x) y) ; error!
        (defun f3 (x) x)
        )

We next present a definition of progn+, together with output from the example displayed above. After that we will start from the beginning and describe how one might develop progn+ from scratch.

The completed code and a test

(defmacro save-progn+-error (x)
  `(make-event
    (pprogn (f-put-global 'progn+-errors
                          (cons ,x
                                (f-get-global 'progn+-errors state))
                          state)
            (value '(value-triple nil)))))

(defun progn+-fn (lst)
  (declare (xargs :guard (true-listp lst) :mode :program))
  (cond ((endp lst) nil)
        (t (cons `(make-event '(:or ,(car lst) (save-progn+-error ',(car lst))))
                 (progn+-fn (cdr lst))))))

(defmacro progn+ (&rest lst)
  (declare (xargs :guard (and (true-listp lst)
                              lst)))
  `(progn (make-event (pprogn (f-put-global 'progn+-errors nil state)
                              (value '(value-triple nil))))
           ,@(progn+-fn lst)))

; Example:
(progn+ (defun f1 (x) x)
        (defthm good-thm (equal 1 1) :rule-classes nil)
        (value-triple (cw "@@HI~%"))
        (defthm bad-thm (equal x y) :rule-classes nil)
        (defun f2 (x) x)
        (defun bad-fn (x) y)
        (defun f3 (x) x)
        )

After running the example (which is the final form above), we expect the resulting logical world to contain definitions of function symbols f1, f2, and f3, as well as the event good-thm, but that no events would be stored for bad-thm or bad-fn. Moreover, we expect that a state global variable holds the event forms for bad-thm and bad-fn. Let us check that all of these expectations are met.

ACL2 !>:pe f1
           4:x(PROGN+ (DEFUN F1 # ...)
                      (DEFTHM GOOD-THM # ...)
                      ...)
              
>L             (DEFUN F1 (X) X)
ACL2 !>:pe f2
           4:x(PROGN+ (DEFUN F1 # ...)
                      (DEFTHM GOOD-THM # ...)
                      ...)
              
>L             (DEFUN F2 (X) X)
ACL2 !>:pe f3
           4:x(PROGN+ (DEFUN F1 # ...)
                      (DEFTHM GOOD-THM # ...)
                      ...)
              
>L             (DEFUN F3 (X) X)
ACL2 !>(@ progn+-errors) ; same as (f-get-global 'progn+-errors state)
((DEFUN BAD-FN (X) Y)
 (DEFTHM BAD-THM (EQUAL X Y)
         :RULE-CLASSES NIL))
ACL2 !>

Development of the solution

We now start from the beginning. Recall that progn does almost what we ask progn+ to do, except that progn stops at the first error. So our approach will be to define a macro that is much like progn, except that each event is modified as follows: if evaluation fails for an event, then that event is pushed onto the value of a specific state global (see programming-with-state), progn+-errors. Moreover, since progn is applied only to legal event forms (see embedded-event-form), we need this modification to be a legal event form, too. Fortunately, a call of make-event is a legal event form. So our plan is for (progn+ ... <event> ...) to expand to a call (progn ... (make-event ...) ...) so that the indicated make-event call attempts to evaluate <event>, and if that attempt fails, then <event> it is pushed onto progn+-errors.

Thus, we begin with a simple piece of the task, by showing how to create an event that will push a specific form, (defthm bad-thm (equal x y) :rule-classes nil), onto progn+-errors.

(make-event
 (pprogn (f-put-global 'progn+-errors
                       (cons '(defthm bad-thm (equal x y) :rule-classes nil)
                             (f-get-global 'progn+-errors state))
                       state)
         (value '(value-triple nil))))

It might seem more natural to write (f-put-global ...), instead of the more complex (pprogn (f-put-global ...) (value '(value-triple nil))). However, the argument to make-event must evaluate to either: (1) a legal event form; or (2) an error-triple, (mv nil x state), where x is a legal event form. Since the f-put-global call modifies state, (1) is not an option; so we choose (2). Since the role of x is only to provide an event form, we choose x to be the trivial event form (value-triple nil).

We follow good programming practice by wrapping the functionality displayed above into a concise utility, as follows.

(defmacro save-progn+-error (x)
; Push x (which is evaluated) onto the value of state global 'progn+-errors.
  `(make-event
    (pprogn (f-put-global 'progn+-errors
                          (cons ,x
                                (f-get-global 'progn+-errors state))
                          state)
            (value '(value-triple nil)))))

Before we write progn+, it helps to approximate its expansion in the specific ``Example'' displayed above. We know in advance which two forms will fail, so we `cheat' by using progn but with those two forms replaced by calls to save-progn+-error.

(f-put-global 'progn+-errors nil state)
(progn  (defun f1 (x) x)
        (defthm good-thm (equal 1 1) :rule-classes nil)
        (value-triple (cw "@@HI~%"))
        (save-progn+-error
         '(defthm bad-thm (equal x y) :rule-classes nil))
        (defun f2 (x) x)
        (save-progn+-error
         '(defun bad-fn (x) y))
        (defun f3 (x) x)
        )

Our next task is to find a way to tell ACL2 that it should run a given event, and if that event fails it should save it using save-progn+-error. Fortunately, the :OR keyword of make-event is perfect for this task. Consider the following two examples.

(make-event '(:or (defun f2 (x) x)
                  (save-progn+-error '(defun f2 (x) x))))

(make-event '(:or (defun bad-fn (x) y)
                  (save-progn+-error '(defun bad-fn (x) y))))

In the first example, make-event invokes the given call of defun, which runs without error; and make-event then exits without error. In the second example, make-event invokes the given call of defun, which causes an error; so then make-event evaluates the second argument of the :OR, to invoke save-progn+-error on that same defun call. Since that call of save-progn+-error evaluates without error (because it expands to (value-triple nil)), the make-event call exits without error. See make-event for more information about the :OR keyword.

We can now define progn+ to be the result of modifying each of its forms as in the two examples displayed just above. First we write a function that transforms a list by applying that modification to each of its members.

(defun progn+-fn (lst)
  (declare (xargs :guard (true-listp lst) :mode :program))
  (cond ((endp lst) nil)
        (t (cons `(make-event '(:or ,(car lst) (save-progn+-error ',(car lst))))
                 (progn+-fn (cdr lst))))))

We complete our definition of progn+, by generating a progn call with the desired modification of each form in the list, using progn+-fn — but preceded by yet another make-event call, this one for initializing our state global to nil.

(defmacro progn+ (&rest lst)
  (declare (xargs :guard (and (true-listp lst)
                              lst)))
  `(progn (make-event (pprogn (f-put-global 'progn+-errors nil state)
                              (value '(value-triple nil))))
           ,@(progn+-fn lst)))

Exercise: Modify this tool so that instead of merely updating a state global, it prints the failed events at the end of execution; and moreover, it prints them in their original order. See make-event-example-2-exercise for a solution.

Subtopics

Make-event-example-2-exercise: Solution to an exercise from make-event-example-2