Collect the output types of functions that return multiple values.
(atj-all-mv-output-types fns-to-translate guards$ wrld) → mv-typess
As explained in atj-gen-shallow-mv-class-name, we generate Java classes that represent mv values. We generate one such class for each distinct function output type list of length two or more. We go through all the ACL2 functions to translate to Java, and consider the output types of the function types associated to each such function that returns two or more results. For each such list of two or more output types, we generate a distinct class. Here we just return the types, which are then passed to atj-pre-translate where they are augmented with any additional mv type that is not any function's output type.
Function:
(defun atj-all-mv-output-types (fns-to-translate guards$ wrld) (declare (xargs :guard (and (symbol-listp fns-to-translate) (booleanp guards$) (plist-worldp wrld)))) (let ((__function__ 'atj-all-mv-output-types)) (declare (ignorable __function__)) (b* (((when (endp fns-to-translate)) nil) (fn (car fns-to-translate)) ((unless (>= (atj-number-of-results fn wrld) 2)) (atj-all-mv-output-types (cdr fns-to-translate) guards$ wrld)) (fn-info (atj-get-function-type-info fn guards$ wrld)) (out-typess (atj-function-type-info->outputs fn-info)) (out-typess (remove-duplicates-equal out-typess)) ((unless (cons-listp out-typess)) (raise "Internal error: ~ output types ~x0 include an empty list." out-typess))) (union-equal out-typess (atj-all-mv-output-types (cdr fns-to-translate) guards$ wrld)))))
Theorem:
(defthm return-type-of-atj-all-mv-output-types (b* ((mv-typess (atj-all-mv-output-types fns-to-translate guards$ wrld))) (and (atj-type-list-listp mv-typess) (cons-listp mv-typess))) :rule-classes :rewrite)