		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-primarray-write-method

Generate a Java method to write a primitive array component.

Signature
(atj-gen-shallow-primarray-write-method type) → method
Arguments: type — Guard (primitive-typep type).
Returns: method — Type (jmethodp method).

In the translation step from ACL2 to Java, we turn calls of the ACL2 functions that model array writes into calls of one of eight methods, one for each primitive type, that destructively assign the array component and then return the array. (Calls of these methods are then removed by post-translation.) This function generates these methods, which are private because only code in the main class (including its nested classes) needs to call them.

The generated method has this form:

private static <type>[] <name>(<type>[] array,
                               int index,
                               <type> component) {
    array[index] = component;
    return array;
}

where <type> is the Java primitive type.

Definitions and Theorems

Function: atj-gen-shallow-primarray-write-method

(defun atj-gen-shallow-primarray-write-method (type)
  (declare (xargs :guard (primitive-typep type)))
  (let ((__function__ 'atj-gen-shallow-primarray-write-method))
    (declare (ignorable __function__))
    (b* ((method-name (atj-primarray-write-method-name type))
         (array-type (jtype-array (jtype-prim type)))
         (index-type (jtype-int))
         (component-type (jtype-prim type))
         (array "array")
         (index "index")
         (component "component")
         (array[index] (jexpr-array (jexpr-name array)
                                    (jexpr-name index)))
         (array[index]=component
              (jblock-asg array[index] (jexpr-name component)))
         (return-array (jblock-return (jexpr-name array)))
         (method-body (append array[index]=component return-array)))
      (make-jmethod
           :access (jaccess-private)
           :abstract? nil
           :static? t
           :final? nil
           :synchronized? nil
           :native? nil
           :strictfp? nil
           :result (jresult-type array-type)
           :name method-name
           :params (list (jparam nil array-type array)
                         (jparam nil index-type index)
                         (jparam nil component-type component))
           :throws nil
           :body method-body))))

Theorem: jmethodp-of-atj-gen-shallow-primarray-write-method

(defthm jmethodp-of-atj-gen-shallow-primarray-write-method
  (b* ((method (atj-gen-shallow-primarray-write-method type)))
    (jmethodp method))
  :rule-classes :rewrite)