Calculate the possible numbers of results of a translated term.

- Signature
(term-possible-numbers-of-results term wrld) → possible-numbers-of-results

- Arguments
`term`—Guard (pseudo-termp term) .`wrld`—Guard (plist-worldp wrld) .- Returns
`possible-numbers-of-results`—Type (pos-listp possible-numbers-of-results) .

The number of results of an untranslated term,
which is either 1 or more if `mv` is involved directly or indirectly,
can be always determined by translating the term
(see `check-user-term`).
However, that information is largely lost in translated terms.
In some cases, the number of results can be determined,
but in other cases there may be two possilities,
namely 1 or a number greater than 1.
The reason is that calls of the macro `mv`
become calls of `list` when terms are translated,
and therefore we cannot distinguish a single list result
from multiple results.

This utility returns the possible number of results of a translated term, as follows.

- If the term is a variable or a quoted constants,
it always returns one result.
This would not be true for the
`mv`variables that result from translating`mv-let`s (see`check-mv-let-call`), but this utility never reaches such variables (see below); it only reaches other variables, which are always bound to single results. - If the term is a (translated) call of
`list`, we have two possibilities in general, as mentioned above. Unless the call builds an empty or singleton list, in which case it cannot result from an`mv`, which always takes at least two arguments, and thus the call must return a single list result. - If the term is a call of
`return-last`, we recursively process its last argument. Note that`return-last`is in*stobjs-out-invalid* , because it returns the same number of results as its last argument. - If the term is a call of
`if`, we recursively process its second and third arguments, and intersect the possible numbers for the two branches. Note that`if`is in*stobjs-out-invalid* , because it returns the same number of results as its branches. Thus, for example, if one branch is a`list`call that may return either 1 or 3 results, while the other branch is a call of a named function that returns 3 results, the`if`call must return 3 results; one branch resolves the ambiguity of the other branch. However, a translated call(if ... (mv ...) (mv ...)) remains ambiguous, with two possible numbers of results. The case in which the two branches have no numbers of results in common should never happen in translated terms obtained by translating valid untranslated terms; however, this utility cannot make that assumption, and may well returnnil . - A call of any other named function is unambiguous, based on the number of results of that function.
- Finally, if the term is a call of a lambda expression,
we recursively process its body.
Its arguments and bound variables do not matter
for determining the number of results of the lambda call.
In particular, if the term is a translated
`mv-let`, themv variables is skipped over (see`check-mv-let-call`), as mentioned above.

Since this utility always returns 1 or 2 numbers explicitly, or intersects the numbers for subterms, the result always consists of 0, 1, or 2 numbers.

**Function: **

(defun term-possible-numbers-of-results (term wrld) (declare (xargs :guard (and (pseudo-termp term) (plist-worldp wrld)))) (let ((__function__ 'term-possible-numbers-of-results)) (declare (ignorable __function__)) (b* (((when (variablep term)) (list 1)) ((when (fquotep term)) (list 1)) ((mv list-call-p elements) (check-list-call term)) ((when list-call-p) (if (>= (len elements) 2) (list 1 (len elements)) (list 1))) (fn (ffn-symb term)) ((when (eq fn 'return-last)) (term-possible-numbers-of-results (fargn term 3) wrld)) ((when (eq fn 'if)) (intersection$ (term-possible-numbers-of-results (fargn term 2) wrld) (term-possible-numbers-of-results (fargn term 3) wrld))) ((when (eq fn 'read-user-stobj-alist)) (list 1)) ((when (eq fn 'do$)) (let* ((quoted-do-fn (fargn term 3)) (do-fn (and (quotep quoted-do-fn) (unquote quoted-do-fn))) (body (and (consp do-fn) (eq (car do-fn) 'lambda) (true-listp do-fn) (car (last do-fn))))) (cond ((pseudo-termp body) (term-possible-numbers-of-results body wrld)) (t (prog2$ (er hard? 'term-possible-numbers-of-results "Unable to guess the number of results for ~x0." term) '(1)))))) ((when (symbolp fn)) (list (number-of-results+ fn wrld)))) (term-possible-numbers-of-results (lambda-body fn) wrld))))

**Theorem: **

(defthm pos-listp-of-term-possible-numbers-of-results (b* ((possible-numbers-of-results (term-possible-numbers-of-results term wrld))) (pos-listp possible-numbers-of-results)) :rule-classes :rewrite)

**Theorem: **

(defthm len-of-term-possible-numbers-of-results-upper-bound (b* ((?possible-numbers-of-results (term-possible-numbers-of-results term wrld))) (<= (len possible-numbers-of-results) 2)) :rule-classes :linear)