Trans*
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 trans, the trans* command can show not only the
translation of a given expression but also the intermediate expansions leading
to that translation, and trans* can also show make-event
expansions. Another difference between trans* and trans is that
trans* does not enforce code restrictions; thus, multiple-value
mismatches and violations of single-threadedness are permitted by trans*.
That is: when trans* takes steps to convert an untranslated term to a
translated term, it does so as though one is translating a theorem statement,
not a definition body.
For discussion of how one may use a keyword command like :trans* in
place of calling the corresponding utility, in this case trans*, see
keyword-commands. Below we focus on the use of the keyword command,
:trans*.
We begin with some simple examples that may suffice to explain how to use
trans*. We then document this utility before concluding with further
details.
Introductory Examples
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 :trans*; comments are
below.
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, mac. The
next iteration expands away the resulting call of the macro, append.
Those two steps are labeled with “(by expansion)” because they are
removing top-level macro calls. The result of the second iteration is not a
macro call, so :trans* finishes up by translating that result to obtain
the final result; notice translation of the second argument of the
binary-append call by expanding rest to cdr.
The example above illustrates a couple of aspects of :trans*.
- An expansion step occurs only with a top-level macro call.
- A translation step is always last.
The result is the same for input :trans* 3 (mac u v), i.e., if first
argument t is replaced by 3 or, in fact, any integer that is at
least the total number of iterations produced with argument t. But we
can specify that we want to stop before the final step. One way is to specify
a number less than the number of iterations. Here is what we get when we
specify that we should stop after 1 iteration.
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 nil or a negative integer as the first
argument.
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, (mv nil (BINARY-APPEND V
(REST U)) state). Without the parentheses, (mv nil :invisible state)
is returned. See error-triple.
Documentation
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 n is a positive integer and form is any ACL2 expression
(i.e., any untranslated term; see term). These commands repeat
translation steps as described later below, according to the value of the
first argument, as follows.
- t: iterate to completion, printing intermediate results
- nil: iterate to completion except for skipping the final translation
step, printing intermediate results
- n: iterate at most n steps, printing intermediate results
- -n: iterate at most n steps except for skipping a final
translation step, printing intermediate results
- (x): same as x but without printing intermediate results, and
returning an error-triple (mv nil val state) where val is the
final result,
It is reasonable to think of a first argument of t as
“infinity” and of nil as “minus infinity”.
Although a first argument of (t) is much like using trans, key
differences besides enforcement of code restrictions (as discussed above) are
that trans* performs make-event expansion and discards certain
“wrappers” like with-output, as described below. The
related utility trans*- differs from trans* in only one way:
trans*- does not perform make-event expansion.
Here is a specification of the iteration step performed on a given form,
which is initially the second argument of trans* and is updated by each
iteration. If the form is not a true-list then iteration halts without any
further result. Otherwise the form may be written as a call (caller arg1
... argk), and the next step's result, if any, depends on caller as
follows.
- 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, denoted argk above.
- Else if caller is make-event, the result is the form's
make-event expansion. (This step is skipped when trans*- is used
rather than trans*.)
- 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 whether caller 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* is nil or a negative integer, then this step is
skipped and instead iteration is halted.
Further Details
While trans* will almost always determine accurately how the given
input expands and is ultimately translated, it is not quite 100% reliable for
that purpose. In particular, make-event expansion isn't guaranteed to
check that the expansion is an embedded event form, as is required for make-event. Another limitation for make-event expansion is that when an
iteration reaches the form (:OR ev1 ... evk), the iteration concludes
rather than evaluating the events evi (see make-event).
A similar utility, trans*-, stops iteration at a call of
make-event without continuing with its make-event expansion. That
is, in fact, the only difference between trans* and trans*-.
We conclude by adding emphasis to an aspect of trans* that is already
noted above: expansion (whether macroexpansion or make-event expansion)
and elimination of event wrappers only take place for the top-level call, not
calls occurring in subterms. Of course, one can call trans* on subterms.
Consider the following example.
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 trans* on the defund subterm to see its
expansion.
