		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-mv-fields

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

Signature
(atj-gen-shallow-mv-fields types) → fields
Arguments: types — Guard (atj-type-listp types).
Returns: fields — Type (jfield-listp fields).

As explained in atj-gen-shallow-mv-class-name, we generate Java classes that represent mv values. Each of these classes has a public instance field for each component type. The field is not private so that it can be quickly accessed when we translate calls of mv-nth to Java; this translation is not supported yet, but we are in the process of building more direct support for mv values in the Java code generated by ATJ. The field is public for the reason explained in atj-gen-shallow-mv-class.

Definitions and Theorems

Function: atj-gen-shallow-mv-fields-aux

(defun atj-gen-shallow-mv-fields-aux (types index)
 (declare (xargs :guard (and (atj-type-listp types)
                             (natp index))))
 (let ((__function__ 'atj-gen-shallow-mv-fields-aux))
   (declare (ignorable __function__))
   (b*
    (((when (endp types)) nil)
     (field (make-jfield :access (jaccess-public)
                         :static? nil
                         :final? nil
                         :transient? nil
                         :volatile? nil
                         :type (atj-type-to-jitype (car types))
                         :name (atj-gen-shallow-mv-field-name index)
                         :init? nil))
     (fields (atj-gen-shallow-mv-fields-aux (cdr types)
                                            (1+ index))))
    (cons field fields))))

Theorem: jfield-listp-of-atj-gen-shallow-mv-fields-aux

(defthm jfield-listp-of-atj-gen-shallow-mv-fields-aux
  (b* ((fields (atj-gen-shallow-mv-fields-aux types index)))
    (jfield-listp fields))
  :rule-classes :rewrite)

Function: atj-gen-shallow-mv-fields

(defun atj-gen-shallow-mv-fields (types)
  (declare (xargs :guard (atj-type-listp types)))
  (let ((__function__ 'atj-gen-shallow-mv-fields))
    (declare (ignorable __function__))
    (atj-gen-shallow-mv-fields-aux types 0)))

Theorem: jfield-listp-of-atj-gen-shallow-mv-fields

(defthm jfield-listp-of-atj-gen-shallow-mv-fields
  (b* ((fields (atj-gen-shallow-mv-fields types)))
    (jfield-listp fields))
  :rule-classes :rewrite)