		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-mv-class-name

Generate the name of the mv class for the given types.

Signature
(atj-gen-shallow-mv-class-name types) → class-name
Arguments: types — Guard (atj-type-listp types).
Returns: class-name — Type (stringp 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 MV_A_B_C_..., where A, B, C, etc. correspond to the ATJ types, or more precisely to their Java types counterparts. For AIJ classes, we use the class names themselves. For Java primitive types, we use the primitive types themselves. For Java primitive array types, we use the element types followed by array. For instance, for the ATJ types (:asymbol :jint :jbyte[]), the class name is MV_Acl2Symbol_int_bytearray.

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.

Definitions and Theorems

Function: atj-gen-shallow-mv-class-name-aux

(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: stringp-of-atj-gen-shallow-mv-class-name-aux

(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: atj-gen-shallow-mv-class-name

(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: stringp-of-atj-gen-shallow-mv-class-name

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