Major Section: ACL2-BUILT-INS
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).
? [RAW LISP] (macroexpand-1 '(RETURN-LAST 'PROGN
(CW "Some CW printing...~%")
(+ 3 4)))
(PROGN (LET ((*AOKP* T)) (CW "SOME CW PRINTING...~%")) (+ 3 4))
T
? [RAW LISP]
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 always included for the second argument as shown except when the
first argument is of the form (QUOTE M) where M is a macro, or (less
important) when the first argument is a symbol or a cons whose car is
QUOTE. This binding allows ACL2 to use attachments in 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. Those who use the experimental HONS version of ACL2
(see hons-and-memoization) will see an additional binding in the above
single-step macroexpansion, which allows the storing of memoized results even
when that would otherwise be prevented because of the use of attachments.)
In general, a form (return-last (quote F) X Y) macroexpands to
(F X Y), where F is 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 (arguent 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 ***********
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 introduceNAMEas an ACL2 macro that expands to a corresponding call ofRAW-NAME(see (2) above) in raw Lisp. The specification of keyword value of:rawasRAW-NAMEmay be omitted ifRAW-NAMEis the result of modifying the symbolNAMEby suffixing the string"-RAW"to thesymbol-nameofNAME.
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. If you wish
to automate certification of such a book with makefiles (see book-makefiles),
perhaps contributing such a book to the ACL2 community books repository (see
http://acl2-books.googlecode.com/), you may also wish to look at
community books file books/misc/Makefile, where you'll notice the following
extra `make' dependency:
profiling.cert: 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), 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 withprog2$
*mbe1-raw, associated withmbe1, a version ofmbe
*ec-call1-raw, associated withec-call1(a variant ofec-call)
*with-guard-checking1-raw, associated withwith-guard-checking1(a variant ofwith-guard-checking)
Note that because of its special status, it is illegal to trace
return-last.
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 *********** 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))))
To see the ACL2 definition of this function, see pf.
