Untranslate-specifier
Specifies the form of terms produced by an APT transformation.
BRIEF SUMMARY (details are skipped here but provided below). When the
value of :untranslate is :nice, then a custom utility, directed-untranslate, uses the original user-level ACL2::term (i.e., the body of a given definition) to direct creation of a
user-level transformed term from the translated, transformed term. The
value :nice-expanded is similar to :nice, but may avoid some
attempts to re-introduce LET bindings into the result. If the value
is t, then the translated, transformed term is subjected to ACL2's
usual untranslate utility, rather than to that custom directed-untranslate utility. Otherwise the value should be
nil, in which case the result of simplifying the term is left alone
as a translated ACL2::term. End summary.
Strictly speaking, the notion of an ACL2 term is quite restrictive.
However, ACL2 proof output avoids this notion of ``translated term'',
instead using a more liberal notion of ``untranslated'' term, in
which (for example) macros may appear and numbers are not quoted. For
more about these two notions of term, see ACL2::term.
When a transformation produces a new term (typically, the body of a new
definition), the question arises: How should that term be presented?
There are two obvious choices: the new term can be translated or
untranslated. For example, if a definition with body (+ 1 1 x) is
transformed to a definition in which 2 is added to x, the new
body would be (+ '2 x) as a translated term but would instead be
(+ 2 x) as an untranslated term (which avoids the rather ugly
single-quote mark). Normally the untranslated term is to be preferred,
for readability.
But one can sometimes do better, with heuristics, than simply using the
most obvious untranslated term. Suppose for example that the original
definition body is (+ 1 1 (first x)). The simplified body may be
created as the translated term (+ '2 (car x)), which naturally
``untranslates'' to (+ 2 (car x)). The call of the macro, first, has been lost! A nicer untranslation will attempt to preserve
more of the original untranslated term. This ``nice'' untranslation would
thus be (+ 2 (first x)). See directed-untranslate for
more information on such ``nice'' untranslation.
A potentially tricky problem is to reconstruct let expressions.
Suppose for example that the original body is (let ((z (first x))) (+ 1
1 z)). A transformation might naturally produce a new body that is
(+ 2 (car x)). A ``nice'' untranslation would ideally reconstruct
the let expression (let ((z (first x))) (+ 2 z)). In some
cases, however, the transformation's heuristics might fail to do a good
job with such reconstructions. Consider for example the body
(let* ((cost (expt 2 0)) (inches 1)) (list cost inches x)). a
transformation might naturally produce a term whose ``nice'' untranslation
is (let* ((cost 1) (inches cost)) (list cost inches x)), yet it is
clearly undesirable to bind inches to cost. In some cases, a
fourth option, the ``nice-expanded'' untranslation, would avoid any
attempt to reconstruct let structure; in the example above, the
result might be (list 1 1 x).
An untranslate specifier is passed as the :untranslate input to a
transformation to control the form of terms produced. An untranslate
specifier is one of the following, though some transformations might
support only some of these values, and the defaults may differ.
- :nice — the new term should be produced by a ``nice''
heuristic untranslation that may respect the structure of the old body to
some reasonable extent, as discussed above.
- t — the new term should be produced by the usual untranslation
procedure after transforming the input term.
- nil — the new term should be produced without untranslation.
- :nice-expanded — the new term should be produced by a ``nice''
heuristic untranslation that may respect the structure of the old body to
some reasonable extent, but may avoid some attempts to reconstruct
let/let* structure, as discussed above.
