		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Term-possible-numbers-of-results

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-lets (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 return nil.
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, the mv 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.

Definitions and Theorems

Function: term-possible-numbers-of-results

(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: pos-listp-of-term-possible-numbers-of-results

(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: len-of-term-possible-numbers-of-results-upper-bound

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