Directed-untranslate
Create a user-level form that reflects a given user-level form's
structure.
See term for relevant background about user-level ``terms''
and actual ``translated'' terms.
General Form:
(directed-untranslate uterm tterm sterm iff-flg stobjs-out wrld)
where:
- uterm is an untranslated form that translates to the term,
tterm;
- sterm is a term, which might share a lot of structure with
tterm (we may think of sterm as a simplified version of
tterm);
- iff-flg is a Boolean;
- stobjs-out is either nil or a true-listp each of whose
members is either nil or the name of a stobj, with no stobj name
repeated; and
- wrld is a logical world, typically (w state).
The result is an untranslated form whose translation is provably equal to
sterm, except that if iff-flg is true then these need only be
Boolean equivalent rather than equal. The goal is that the shared structure
between tterm and sterm is reflected in similar sharing between
uterm and the result. If stobjs-out is not nil, then an
attempt is made to produce a result with multiple-value return, whose i-th
element is an ordinary value or a stobj, st, according to whether the
i-th element of stobjs-out is nil or st, respectively.
Example Form:
(directed-untranslate
'(and a (if b c nil)) ; uterm
'(if a (if b c 'nil) 'nil) ; tterm
'(if a2 (if b2 c2 'nil) 'nil) ; sterm, a form to be untranslated
nil nil
(w state))
The returned value from the example above is:
(AND A2 (IF B2 C2 NIL))
Compare this with the value returned by calling the system function
untranslate instead on the final three arguments:
ACL2 !>(untranslate '(if a2 (if b2 c2 'nil) 'nil) nil (w state))
(AND A2 B2 C2)
ACL2 !>
The original structure of the given ``uterm'', (and a (if b c nil)),
has been preserved by directed-untranslate, but not by untranslate.
Thus, directed-untranslate may be particularly useful when a given form,
uterm, translates to a term, tterm, which in turn simplifies to a
related term, sterm, and your goal is to untranslate sterm in a way
that preserves structure from uterm.
Remarks.
- The directed-untranslate utility is based on heuristics that may not
always produce the result you want. They have been designed to work best in
the case that sterm is a simplification of tterm.
- For an example of the heuristics, suppose that uterm let-binds a
variable, v, which thus is lambda-bound in tterm to some
expression, expr. If v has essentially been replaced by a value
expr' that occurs in sterm, then an attempt is often made to use
lambda abstraction to let-bind v to expr' in the result. (No such
attempt is made if expr has essentially disappeared in sterm.) The
utility, directed-untranslate-no-lets, is similar but does not make such
an attempt.
- For another example, results involving b* are biased towards the
intended primary use case, in which sterm is a simplification of tterm and the
result is intended to be in simplified form. In particular, bindings of the
form (var val) that specify an ignored or ignorable variable are handled
as follows.
- A b* binding (- val) in uterm translates to (prog2$
val ...), so is generally preserved if there is a corresponding prog2$ call in sterm.
- A b* binding of (& val) or (?!x val) in uterm is
completely discarded in translation to tterm, so is presumably not
present in sterm, hence is also discarded in the result.
- A b* binding (?x val) in uterm generates an ignorable
declaration, so is generally preserved if and only if x occurs free in
sterm. (If the binding were restored after being simplified away, it
could contain an unsimplified term, which we deem to be undesirable.)
- Directed-untranslate may be improved over time; hence it may produce
different results as the tool uses increasingly sophisticated heuristics. For
example, here are some features that are not yet implemented but might be in
the future, quite possibly only upon request.
- A better untranslation might be obtainable when the simplified
term (sterm) has similar structure to a proper subterm of the original
term (tterm). As it stands now, the original untranslated term uterm
is probably useless in that case.
- More macros could quite reasonably be handled, but aren't yet, such as
case.
- Support for b* may be improved by comprehending more binders.
End of Remarks.
