An example use of make-event
Here, we develop a reasonably self-contained example that
illustrates how to use
The challenge is to develop a programmatic method for solving the following sort of problem.
We illustrate how to do this sort of thing by specifying the ``new
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 @(see ; 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
(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
We complete the job by making a programmatic solution, with a macro that
expands to such a
(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 !>