		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-mv-params

Generate the parameters of the factory method of the mv class for the given types.

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

As explained in atj-gen-shallow-mv-class-name, we generate Java classes that represent mv values. Each such class has a static factory method that re-uses a singleton instance of the class. The names of this method's parameter are the same as the corresponding fields.

Definitions and Theorems

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

(defun atj-gen-shallow-mv-params-aux (types index)
 (declare (xargs :guard (and (atj-type-listp types)
                             (natp index))))
 (let ((__function__ 'atj-gen-shallow-mv-params-aux))
   (declare (ignorable __function__))
   (b*
    (((when (endp types)) nil)
     (type (car types))
     (param
          (make-jparam :final? nil
                       :type (atj-type-to-jitype type)
                       :name (atj-gen-shallow-mv-field-name index)))
     (params (atj-gen-shallow-mv-params-aux (cdr types)
                                            (1+ index))))
    (cons param params))))

Theorem: jparam-listp-of-atj-gen-shallow-mv-params-aux

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

Function: atj-gen-shallow-mv-params

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

Theorem: jparam-listp-of-atj-gen-shallow-mv-params

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