Calculate the possible numbers of results of a translated term.
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.
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.
(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))))
(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)
(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)