Generate the name of the mv class for the given types.
(atj-gen-shallow-mv-class-name types) → class-name
Since Java does not allow methods to return multiple values directly, we need to create, for ACL2 functions that return mv results, Java classes that group these multiple values into single objects. There is a different class for each tuple of types of the multiple values. Here we generate the names of these classes, based on the ATJ types of the multiple values.
These classes have names of the form
The list of ATJ types must have at least two elements. It does not make sense to have a multiple value consisting of zero or one values.
Function:
(defun atj-gen-shallow-mv-class-name-aux (types) (declare (xargs :guard (atj-type-listp types))) (let ((__function__ 'atj-gen-shallow-mv-class-name-aux)) (declare (ignorable __function__)) (b* (((when (endp types)) "") (type (car types)) (jtype (atj-type-to-jitype type)) (first (cond ((equal jtype (jtype-boolean)) "_boolean") ((equal jtype (jtype-char)) "_char") ((equal jtype (jtype-byte)) "_byte") ((equal jtype (jtype-short)) "_short") ((equal jtype (jtype-int)) "_int") ((equal jtype (jtype-long)) "_long") ((equal jtype (jtype-float)) "_float") ((equal jtype (jtype-double)) "_double") ((equal jtype (jtype-array (jtype-boolean))) "_booleanarray") ((equal jtype (jtype-array (jtype-char))) "_chararray") ((equal jtype (jtype-array (jtype-byte))) "_bytearray") ((equal jtype (jtype-array (jtype-short))) "_shortarray") ((equal jtype (jtype-array (jtype-int))) "_intarray") ((equal jtype (jtype-array (jtype-long))) "_longarray") ((equal jtype (jtype-array (jtype-float))) "_floatarray") ((equal jtype (jtype-array (jtype-double))) "_doublearray") (t (str::cat "_" (jtype-class->name jtype))))) (rest (atj-gen-shallow-mv-class-name-aux (cdr types)))) (str::cat first rest))))
Theorem:
(defthm stringp-of-atj-gen-shallow-mv-class-name-aux (b* ((class-name-suffix (atj-gen-shallow-mv-class-name-aux types))) (stringp class-name-suffix)) :rule-classes :rewrite)
Function:
(defun atj-gen-shallow-mv-class-name (types) (declare (xargs :guard (atj-type-listp types))) (declare (xargs :guard (>= (len types) 2))) (let ((__function__ 'atj-gen-shallow-mv-class-name)) (declare (ignorable __function__)) (str::cat "MV" (atj-gen-shallow-mv-class-name-aux types))))
Theorem:
(defthm stringp-of-atj-gen-shallow-mv-class-name (b* ((class-name (atj-gen-shallow-mv-class-name types))) (stringp class-name)) :rule-classes :rewrite)