Trans
Print the translation of a form
Examples:
:trans (list a b c)
:trans (caddr x)
:trans (cond (p q) (r))
ACL2 accepts user-level syntax as input, and it prints the result of
translating it to an internal syntax. This translation includes
macroexpansion, replacing let forms by lambda expressions,
quoting constants, and so on. See term for relevant background. The
printing can be abbreviated, as it uses the :term evisc-tuple
(with a flg of nil, hence without any abbreviation by default; see
set-evisc-tuple).
Note that the trans command prints a term that need not obey
code restrictions: that term can be used in theorems but might not be allowed
in definitions (except in non-executable contexts; see defun-nx
and see non-exec).
Trans takes one argument, an alleged term in user syntax, and
translates it, expanding the macros in it completely. Either an error is
caused or the internal syntax for the term (representing its formal meaning)
is printed. It also prints the ``output signature'' which indicates how many
results are returned and which are single-threaded objects. For example, a
term that returns one ordinary object (e.g., an object other than state or a user-defined single-threaded object (see defstobj)) has the
output signature
=> *
A term that returns the single-threaded object STATE has the output
signature
=> STATE
and a term that returns four results might have the output signature
=> (MV $MEM * * STATE)
This signature indicates that the first result is the (user defined)
single-threaded object $MEM, that the next two results are ordinary, and
that the last result is STATE.
See trans! for a corresponding command that does not enforce
restrictions of single-threaded objects. See trans* for a command that
can show intermediate expansion results.
The argument supplied to :trans may contain variables, including stobj names. However, variables that are not stobj names are assumed not to
be dfs (see df). For example, :trans (df+ x y) causes an error;
to see the desired translation use :trans! (df+ x y).
It is sometimes more convenient to use :trans1, which, unlike
:trans, only does top-level macroexpansion.
For more, see term.
