Restore mv calls in a translated term.
(atj-restore-mv-calls-in-term term numres wrld) → new-term
We restore not only mv calls returned by multi-result functions, but also mv calls that may happen in an mv-let in a function that may or may not return multiple results.
At the top level,
this code is called on the body of a function
that must be translated to Java.
In this top-level call,
we pass as second argument the number of result of the function,
which is known: see atj-restore-mv-calls-in-body.
As we descend into the term, this number may change.
When we try to restore mv calls in a term,
we always know the number of results that the term should return,
as the
When we encounter a variable,
we must be expecting one result,
and in that case we leave the variable unchanged.
This would not be true for the
When we encounter a quoted constant, we must be expecting one result, and in that case we leave the quoted constant unchanged.
Before processing a call,
we use check-mv-let-call to see if
the term may be a translated mv-let.
If the term has that form, it is possible, but unlikely,
that it is not actually a translated mv-let.
In order to properly restore mv calls in the
If the term does not have the form of a translated mv-let,
we check whether it is a translated list,
i.e. a nest of conses ending with a quoted
If the term does not have any of the previous forms,
we check whether it is a call of if.
In that case, we recursively process the arguments:
the test must be single-valued,
while the branches have the same
We check for return-last for robustness, but those have been all removed by a previous pre-translation step.
We treat all other calls as follows.
We recursively process the arguments,
each of which must return a single value.
If the function is a lambda expression,
we recursively process its body,
with the same
Theorem:
(defthm return-type-of-atj-restore-mv-calls-in-term.new-term (b* ((?new-term (atj-restore-mv-calls-in-term term numres wrld))) (pseudo-termp new-term)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-restore-mv-calls-in-args.new-args (implies (pseudo-term-listp args) (b* ((?new-args (atj-restore-mv-calls-in-args args wrld))) (and (pseudo-term-listp new-args) (equal (len new-args) (len args))))) :rule-classes :rewrite)