		Search-engine friendly clone of the ACL2 documentation.

Return-last

Return the last argument, perhaps with side effects

Return-last is an ACL2 function that returns its last argument. It is used to implement common utilities such as prog2$ and time$. For most users, this may already be more than one needs to know about return-last; for example, ACL2 tends to avoid printing calls of return-last in its output, printing calls of prog2$ or time$ (or other such utilities) instead.

If you encounter a call of return-last during a proof, then you may find it most useful to consider return-last simply as a function defined by the following equation.

(equal (return-last x y z) z)

It may also be useful to know that unlike other ACL2 functions, return-last can take a multiple value as its last argument, in which case this multiple value is returned. The following contrived definition illustrates this point.

ACL2 !>(defun foo (fn x y z)
         (return-last fn x (mv y z)))

Since FOO is non-recursive, its admission is trivial.  We observe that
the type of FOO is described by the theorem
(AND (CONSP (FOO FN X Y Z)) (TRUE-LISTP (FOO FN X Y Z))).  We used
primitive type reasoning.

(FOO * * * *) => (MV * *).

Summary
Form:  ( DEFUN FOO ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 FOO
ACL2 !>(foo 'bar 3 4 5)
(4 5)
ACL2 !>(mv-let (a b)
               (foo 'bar 3 4 5)
               (cons b a))
(5 . 4)
ACL2 !>

Most readers would be well served to avoid reading the rest of this documentation of return-last. For reference, however, below we document it in some detail. We include some discussion of its evaluation, in particular its behavior in raw Lisp, because we expect that most who read further are working with raw Lisp code (and trust tags).

Return-last is an ACL2 function that can arise from macroexpansion of certain utilities that return their last argument, which may be a multiple value. Consider for example the simplest of these, prog2$:

ACL2 !>:trans1 (prog2$ (cw "Some CW printing...~%") (+ 3 4))
 (RETURN-LAST 'PROGN
              (CW "Some CW printing...~%")
              (+ 3 4))
ACL2 !>

Notice that a call of prog2$ macroexpands to a call of return-last in which the first argument is (quote progn). Although return-last is a function in the ACL2 world, it is implemented ``under the hood'' as a macro in raw Lisp, as the following log (continuing the example above) illustrates.

ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
? (macroexpand-1 '(RETURN-LAST 'PROGN
                                (CW "Some CW printing...~%")
                                (+ 3 4)))
(PROGN (LET ((*AOKP* T)) (CW "Some CW printing...~%")) (+ 3 4))
T
?

Thus, the original prog2$ call generates a corresponding call of progn in raw Lisp, which in turn causes evaluation of each argument and returns whatever is returned by evaluation of the last (second) argument.

Remark for those who use defattach. The binding of *aokp* to t is included for the second argument as shown in most cases. That binding is avoided only when the first argument is of the form (QUOTE S) for S a macro name and the second argument is a symbol or of the form (QUOTE X) for any X. By binding *aokp* to t, ACL2 is permitted to use attachments when evaluating the second argument of return-last (hence, in the first argument of prog2$), even in contexts such as proofs in which attachments are normally not allowed.

In general, a form (return-last (quote F) X Y) macroexpands to (F X Y), where F is a symbol defined in raw Lisp to return its last argument. The case that F is progn is a bit misleading, because it is so simple. More commonly, macroexpansion produces a call of a macro defined in raw Lisp that may produce side effects. Consider for example the ACL2 utility with-guard-checking, which is intended to change the guard-checking mode to the indicated value (see with-guard-checking).

ACL2 !>(with-guard-checking :none (car 3)) ; no guard violation
NIL
ACL2 !>:trans1 (with-guard-checking :none (car 3))
 (WITH-GUARD-CHECKING1 (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                       (CAR 3))
ACL2 !>:trans1 (WITH-GUARD-CHECKING1 (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                                     (CAR 3))
 (RETURN-LAST 'WITH-GUARD-CHECKING1-RAW
              (CHK-WITH-GUARD-CHECKING-ARG :NONE)
              (CAR 3))
ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
? [RAW LISP] (macroexpand-1
              '(RETURN-LAST 'WITH-GUARD-CHECKING1-RAW
                             (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                             (CAR 3)))
(WITH-GUARD-CHECKING1-RAW (CHK-WITH-GUARD-CHECKING-ARG :NONE) (CAR 3))
T
? [RAW LISP] (pprint
              (macroexpand-1
               '(WITH-GUARD-CHECKING1-RAW
                 (CHK-WITH-GUARD-CHECKING-ARG :NONE)
                 (CAR 3))))

(LET ((ACL2_GLOBAL_ACL2::GUARD-CHECKING-ON
       (CHK-WITH-GUARD-CHECKING-ARG :NONE)))
  (DECLARE (SPECIAL ACL2_GLOBAL_ACL2::GUARD-CHECKING-ON))
  (CAR 3))
? [RAW LISP]

The above raw Lisp code binds the state global variable guard-checking-on to :none, as chk-with-guard-checking-arg is just the identity function except for causing a hard error for an illegal input.

The intended use of return-last is that the second argument is evaluated first in a normal manner, and then the third argument is evaluated in an environment that may depend on the value of the second argument. (For example, the macro with-prover-time-limit macroexpands to a call of return-last with a first argument of 'WITH-PROVER-TIME-LIMIT1-RAW, a second argument that evaluates to a numeric time limit, and a third argument that is evaluated in an environment where the theorem prover is restricted to avoid running longer than that time limit.) Although this intended usage model is not strictly enforced, it is useful to keep in mind in the following description of how calls of return-last are handled by the ACL2 evaluator.

When a form is submitted in the top-level loop, it is handled by ACL2's custom evaluator. That evaluator is specified to respect the semantics of the expression supplied to it: briefly put, if an expression E evaluates to a value V, then the equality (equal E (quote V)) should be a theorem. Notice that this specification does not discuss the side-effects that may occur when evaluating a call of return-last, so we discuss that now. Suppose that the ACL2 evaluator encounters the call (return-last 'fn expr1 expr2). First it evaluates expr1. If this evaluation succeeds without error, then it constructs an expression of the form (fn *x* ev-form), where *x* is a Lisp variable bound to the result of evaluating expr1 and ev-form is a call of the evaluator for expr2. (Those who want implementation details are invited to look at function ev-rec-return-last in ACL2 source file translate.lisp.) There are exceptions if fn is progn, ec-call1-raw, with-guard-checking1-raw, or mbe1-raw, but the main idea is the same: do a reasonable job emulating the behavior of a raw-Lisp call of return-last.

The following log shows how a time$ call can generate a call of the evaluator for the last argument of return-last (argument expr2, above). We use :trans1 to show single-step macroexpansions, which indicate how a call of time$ expands to a call of return-last. The implementation actually binds the Lisp variable *RETURN-LAST-ARG3* to expr2 before calling the ACL2 evaluator, ev-rec.

ACL2 !>:trans1 (time$ (+ 3 4))
 (TIME$1 (LIST 0 NIL NIL NIL NIL)
         (+ 3 4))
ACL2 !>:trans1 (TIME$1 (LIST 0 NIL NIL NIL NIL)
                       (+ 3 4))
 (RETURN-LAST 'TIME$1-RAW
              (LIST 0 NIL NIL NIL NIL)
              (+ 3 4))
ACL2 !>(time$ (+ 3 4))
; (EV-REC *RETURN-LAST-ARG3* ...) took
; 0.00 seconds realtime, 0.00 seconds runtime
; (1,120 bytes allocated).
7
ACL2 !>

We now show how things can go wrong in other than the ``intended use'' case described above. In the example below, the macro mac-raw is operating directly on the syntactic representation of its first argument, which it obtains of course as the second argument of a return-last call. Again this ``intended use'' of return-last requires that argument to be evaluated and then only its result is relevant; its syntax is not supposed to matter. We emphasize that only top-level evaluation depends on this ``intended use''; once evaluation is passed to Lisp, the issue disappears. We illustrate below how to use the top-level utility to avoid this issue; see top-level. The example uses the utility defmacro-last to ``install'' special handling of the raw-Lisp macro mac-raw by return-last; later below we discuss defmacro-last.

 ACL2 !>(defttag t)

 TTAG NOTE: Adding ttag :T from the top level loop.
  T
 ACL2 !>(progn!
          (set-raw-mode t)
          (defmacro mac-raw (x y)
            `(progn (print (quote ,(cadr x)))
                    (terpri) ; newline
                    ,y)))

 Summary
 Form:  ( PROGN! (SET-RAW-MODE T) ...)
 Rules: NIL
 Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
  NIL
 ACL2 !>(defmacro-last mac)
 [[ ... output omitted ... ]]
  RETURN-LAST-TABLE
 ACL2 !>(return-last 'mac-raw '3 nil)

 ***********************************************
 ************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
 Error:  Fault during read of memory address #x120000300006
 ***********************************************

 If you didn't cause an explicit interrupt (Control-C),
 then the root cause may be call of a :program mode
 function that has the wrong guard specified, or even no
 guard specified (i.e., an implicit guard of t).
 See :DOC guards.

 To enable breaks into the debugger (also see :DOC acl2-customization):
 (SET-DEBUGGER-ENABLE T)
 ACL2 !>(top-level (return-last 'mac-raw '3 nil))

 3
 NIL
 ACL2 !>

We next describe how to extend the behavior of return-last. This requires an active trust tag (see defttag), and is accomplished by extending a table provided by ACL2, see return-last-table. Rather than using table events directly for this purpose, it is probably more convenient to use a macro, defmacro-last. We describe the community book books/misc/profiling.lisp in order to illustrate how this works. The events in that book include the following, which are described below.

(defttag :profiling)

(progn!
 (set-raw-mode t)
 (load (concatenate 'string (cbd) "profiling-raw.lsp")))

(defmacro-last with-profiling)

The first event introduces a trust tag. The second loads a file into raw Lisp that defines a macro, with-profiling-raw, which can do profiling for the form to be evaluated. The third introduces an ACL2 macro with-profiling, whose calls expand into calls of the form (return-last (quote with-profiling-raw) & &). The third event also extends return-last-table so that these calls will expand in raw Lisp to calls of with-profiling-raw.

The example above illustrates the following methodology for introducing a macro that returns its last argument but produces useful side-effects with raw Lisp code.

(1) Introduce a trust tag (see defttag).

(2) Using progn!, load into raw Lisp a file defining a macro, RAW-NAME, that takes two arguments, returning its last (second) argument but using the first argument to produce desired side effects during evaluation of that last argument.

(3) Evaluate the form (defmacro-last NAME :raw RAW-NAME). This will introduce NAME as an ACL2 macro that expands to a corresponding call of RAW-NAME (see (2) above) in raw Lisp. The specification of keyword value of :raw as RAW-NAME may be omitted if RAW-NAME is the result of modifying the symbol NAME by suffixing the string "-RAW" to the symbol-name of NAME.

WARNING: Not every use of return-last can be soundly evaluated outside a function body. The reason is that ACL2's evaluator, ev-rec, recurs through terms that are presented in the top-level loop, and handles return-last calls in a special manner: basically, the call of ev-rec on the form (return-last 'mac-raw x y) leads to evaluation of a macro call of the form (mac-raw *return-last-arg2* (ev-rec ...)), where *return-last-arg2* is a global variable bound to the result of evaluating x with ev-rec. Consider the following example.

(defttag t)
(set-raw-mode-on state)
(defmacro mac-raw (str y) ; print message is an atom
 `(let ((result (consp ,y))
        (str ,str))
    (or result
        (prog2$ (fmx ,str ',y)
                nil))))
(set-raw-mode-off state)
(defmacro-last mac)
; Horrible error:
(mac "Not a cons: ~x0~%" 17)
; Works, but probably many would consider it awkward to use top-level:
(top-level (mac "Not a cons: ~x0~%" 17))

In such cases we suggest supplying keyword :top-level-ok nil to the call of defmacro-last, for example:

(defmacro-last mac :top-level-ok nil)

Then any attempt to call mac at the top level, as opposed to inside a function body, will cause a clean error before evaluation begins.

It is useful to explore what is done by defmacro-last.

ACL2 !>:trans1 (defmacro-last with-profiling)
 (PROGN (DEFMACRO WITH-PROFILING (X Y)
                  (LIST 'RETURN-LAST
                        (LIST 'QUOTE 'WITH-PROFILING-RAW)
                        X Y))
        (TABLE RETURN-LAST-TABLE 'WITH-PROFILING-RAW
               'WITH-PROFILING))
ACL2 !>:trans1 (with-profiling '(assoc-eq fgetprop rewrite) (mini-proveall))
 (RETURN-LAST 'WITH-PROFILING-RAW
              '(ASSOC-EQ FGETPROP REWRITE)
              (MINI-PROVEALL))
ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
? [RAW LISP] (macroexpand-1
              '(RETURN-LAST 'WITH-PROFILING-RAW
                             '(ASSOC-EQ FGETPROP REWRITE)
                             (MINI-PROVEALL)))
(WITH-PROFILING-RAW '(ASSOC-EQ FGETPROP REWRITE) (MINI-PROVEALL))
T
? [RAW LISP]

To understand the macro with-profiling-raw you could look at the community book loaded above: books/misc/profiling-raw.lsp.

We mentioned above that ACL2 tends to print calls of prog2$ or time$ (or other such utilities) instead of calls of return-last. Here we elaborate that point. ACL2's `untranslate' utility treats (return-last (quote F) X Y) as (G X Y) if F corresponds to the symbol G in return-last-table. However, it is generally rare to encounter such a term during a proof, since calls of return-last are generally expanded away early during a proof.

Calls of return-last that occur in code — forms submitted in the top-level ACL2 loop, and definition bodies other than those marked as non-executable (see defun-nx) — have the following restriction: if the first argument is of the form (quote F) where F is a non-nil symbol, then F must be an entry in return-last-table. There are however four exceptions: the following symbols are considered to be keys of return-last-table even if they are no longer associated with non-nil values, say because of a table event with keyword :clear.

* progn, associated with prog2$

* mbe1-raw, associated with mbe1, a version of mbe

* ec-call1-raw, associated with ec-call1 (a variant of ec-call)

* with-guard-checking1-raw, associated with with-guard-checking1 (a variant of with-guard-checking)

Note that because of its special status, it is illegal to trace return-last.

For any object x that is not of the form (quote S) where S is a symbol, the call (return-last x y z) is legal, even in code, if y and z are legal. Such terms are evaluated as though x is (QUOTE PROGN), that is, as though they arose from a call of prog2$. In particular, you are welcome to write terms of the form (return-last '(<some-annotation>) y z).

We conclude by warning that as a user, you take responsibility for not compromising the soundness or error handling of ACL2 when you define a macro in raw Lisp and especially when you install it as a key of return-last-table, either directly or (more likely) using defmacro-last. In particular, be sure that you are defining a macro of two arguments that always returns the value of its last argument, returning the complete multiple value if that last argument evaluates to a multiple value.

The following is correct, and illustrates care taken to return multiple values.

:q
(defmacro my-time1-raw (val form)
  (declare (ignore val))
  `(let  ((start-time (get-internal-run-time))
          (result (multiple-value-list ,form))
          (end-time (get-internal-run-time)))
     (format t "Total time: ~s~%"
             (float (/ (- end-time start-time)
                       internal-time-units-per-second)))
     (values-list result)))
(lp)
(defttag t)
(defmacro-last my-time1)
(defmacro my-time (form)
  `(my-time1 nil ,form))

Then for example:

ACL2 !>(my-time (equal (make-list 1000000) (make-list 1000000)))
Total time: 0.12
T
ACL2 !>

But if instead we provide the following more naive implementation, of the above raw Lisp macro, the above evaluation can produce an error, for example if the host Lisp is CCL.

(defmacro my-time1-raw (val form)
    (declare (ignore val))
    `(let  ((start-time (get-internal-run-time))
            (result ,form)
            (end-time (get-internal-run-time)))
       (format t "Total time: ~s~%"
               (float (/ (- end-time start-time)
                         internal-time-units-per-second)))
       result)) ; WRONG -- need multiple values returned!

Here is a second, similar example. This time we'll start with the error; can you spot it?

(defttag t)
(progn!
 (set-raw-mode t)
 (defmacro foo-raw (x y)
   `(prog1
        ,y
      (cw "Message showing argument 1: ~x0~%" ,x))))
(defmacro-last foo)

We then can wind up with a hard Lisp error:

ACL2 !>(foo 3 (mv 4 5))
Message showing argument 1: 3

***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error:  value NIL is not of the expected type REAL.
***********************************************

If you didn't cause an explicit interrupt (Control-C),
then the root cause may be call of a :program mode
function that has the wrong guard specified, or even no
guard specified (i.e., an implicit guard of t).
See :DOC guards.

To enable breaks into the debugger (also see :DOC acl2-customization):
(SET-DEBUGGER-ENABLE T)
ACL2 !>

Here is a corrected version of the above macro. The point here is that prog1 returns a single value, while our-multiple-value-prog1 returns all the values that are returned by its first argument.

(progn!
 (set-raw-mode t)
 (defmacro foo-raw (x y)
   `(our-multiple-value-prog1 ;; better
     ,y
     (cw "Message showing argument 1: ~x0~%" ,x))))

Function: return-last

(defun return-last (fn eager-arg last-arg)
  (declare (ignore fn eager-arg)
           (xargs :guard
                  (if (equal fn 'mbe1-raw)
                      (equal last-arg eager-arg)
                    t)))
  last-arg)

Subtopics

Return-last-table: Install special raw Lisp behavior