		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-multiple-values

Atj-restore-mv-calls-in-term

Restore mv calls in a translated term.

Signature
(atj-restore-mv-calls-in-term term numres wrld) → new-term
Arguments: term — Guard (pseudo-termp term).; numres — Guard (posp numres).; wrld — Guard (plist-worldp wrld).
Returns: new-term — Type (pseudo-termp 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 numres parameter.

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 mv variable that results from a translated mv-let (see check-mv-let-call), but as explained below we process translated mv-lets specially: when we reach a variable, it is never that mv variable, and so it is always single-valued.

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 mv-term, we need to determine how many results it is expected to return. Because of the pre-translation step that removes unused variables, this cannot be determined, in general, from the term, because some mv-nth calls may have been removed. Even if they were all present, it is still possible (though unlikely) that the term does not involve multiple values, and that it just looks like a translated mv-let. Thus, we use the term-possible-numbers-of-results utility to calculate the number of results of the mv-term. Recall that this may return two possibilities, namely 1 and a number greater than 1: in this case, we pick the number greater than 1 (but it would be also correct to pick 1). If instead there is just one possibility, then we obviously use that. This value is used as numres to recursively process the mv-term, which in general may restore not only mv calls at the top level of that term, but also in subterms. We also recursively process the body-term, this time with the same numres as for the mv-let term.

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 nil. If the expected number of results is 1, we leave this term as is, i.e. as a single list. Otherwise, we replace the term with an mv call.

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 numres as the if call.

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 numres as the lambda call.

Theorem: return-type-of-atj-restore-mv-calls-in-term.new-term

(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: return-type-of-atj-restore-mv-calls-in-args.new-args

(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)

Subtopics

Atj-restore-mv-calls-in-args