Show intermediate expansion results for the translation of a form

See term for background on translated and untranslated
terms. See trans, trans!, and `trans1` for other
utilities that expand and translate their input.

Unlike `make-event`
expansions. Another difference between

For discussion of how one may use a keyword command like

We begin with some simple examples that may suffice to explain how to use

The examples below assume that the following definition has been submitted.

(defmacro mac (x y) `(append ,y (rest ,x)))

Here is a log showing a typical use of

ACL2 !>:trans* t (mac u v) Iteration 1 produces (by expansion): (APPEND V (REST U)) ---------- Iteration 2 produces (by expansion): (BINARY-APPEND V (REST U)) ---------- Iteration 3 produces (by translation): (BINARY-APPEND V (CDR U)) ---------- ACL2 !>

We see that Iteration 1 expands away the call of the macro, `rest` to `cdr`.

The example above illustrates a couple of aspects of

- An expansion step occurs only with a top-level macro call.
- A translation step is always last.

The result is the same for input

ACL2 !>:trans* 1 (mac u v) Iteration 1 produces (by expansion): (APPEND V (REST U)) ---------- ACL2 !>

Another way to stop early is to rule out the final translation step. Here
is an example by using

ACL2 !>:trans* -5 (mac u v) ; same for nil, -2, -3, -4, etc. instead of -5 Iteration 1 produces (by expansion): (APPEND V (REST U)) ---------- Iteration 2 produces (by expansion): (BINARY-APPEND V (REST U)) ---------- ACL2 !>

If you are only interested in obtaining the final result, with no intermediate printing, put parentheses around the first argument. Here is what happens when we make that modification to the example immediately above.

ACL2 !>:trans* (-5) (mac u v) ; same answer for nil, -2, -3, etc instead of -5 (BINARY-APPEND V (REST U)) ACL2 !>

Note the single space of indentation in the result above. That indicates
that what is actually returned is multiple values,

General Forms: :trans t form :trans nil form :trans n form :trans -n form :trans (x) form ; for x = t, nil, n, or -n

where

t : iterate to completion, printing intermediate resultsnil : iterate to completion except for skipping the final translation step, printing intermediate resultsn : iterate at mostn steps, printing intermediate results-n : iterate at mostn steps except for skipping a final translation step, printing intermediate results(x) : same asx but without printing intermediate results, and returning an error-triple(mv nil val state) whereval is the final result,

It is reasonable to think of a first argument of `trans`, key
differences besides enforcement of code restrictions (as discussed above) are
that `make-event` expansion and discards certain
“wrappers” like `with-output`, as described below. The
related utility `trans*-` differs from

Here is a specification of the iteration step performed on a given form,
which is initially the second argument of

- If
caller is in the list of “event wrappers”,(local skip-proofs with-cbd with-current-package with-guard-checking-event with-output with-prover-step-limit with-prover-time-limit) , then the next step's result is the last argument of the call, denotedargk above. - Else if
caller is`make-event`, the result is the form'smake-event expansion. (This step is skipped when`trans*-`is used rather thantrans* .) - Else if
caller is a built-in event constructor such as`defun`or`defthm`, or one of`certify-book`,`defpkg`, or`in-package`, then iteration is halted. (Technical note: The actual test used here is whethercaller is a key of the alist value of the constant,*syms-not-callable-in-code-fal* .) - Else if
caller is a macro, expand the macro call. - Otherwise translate the form, except that as noted above, if the first
argument of
trans* isnil or a negative integer, then this step is skipped and instead iteration is halted.

While `make-event`. Another limitation for

A similar utility, `trans*-`, stops iteration at a call of

We conclude by adding emphasis to an aspect of

ACL2 !>:trans* t (defund-nx f (x) x) Iteration 1 produces (by expansion): (WITH-OUTPUT :STACK :PUSH :OFF :ALL (PROGN (ENCAPSULATE NIL (LOGIC) (SET-STATE-OK T) (WITH-OUTPUT :STACK :POP (DEFUND F (X) (DECLARE (XARGS :NON-EXECUTABLE T :MODE :LOGIC)) (PROG2$ (THROW-NONEXEC-ERROR 'F (LIST X)) X))) (WITH-OUTPUT :STACK :POP :OFF SUMMARY (IN-THEORY (DISABLE (:E F))))) (WITH-OUTPUT :STACK :POP :OFF SUMMARY (VALUE-TRIPLE '(:DEFUND-NX F))))) ---------- Iteration 2 is dropping the WITH-OUTPUT wrapper: (PROGN (ENCAPSULATE NIL (LOGIC) (SET-STATE-OK T) (WITH-OUTPUT :STACK :POP (DEFUND F (X) (DECLARE (XARGS :NON-EXECUTABLE T :MODE :LOGIC)) (PROG2$ (THROW-NONEXEC-ERROR 'F (LIST X)) X))) (WITH-OUTPUT :STACK :POP :OFF SUMMARY (IN-THEORY (DISABLE (:E F))))) (WITH-OUTPUT :STACK :POP :OFF SUMMARY (VALUE-TRIPLE '(:DEFUND-NX F)))) ---------- ACL2 !>

One can then call `defund` subterm to see its
expansion.