Generate a Java method to write a primitive array component.
(atj-gen-shallow-primarray-write-method type) → 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
Function:
(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:
(defthm jmethodp-of-atj-gen-shallow-primarray-write-method (b* ((method (atj-gen-shallow-primarray-write-method type))) (jmethodp method)) :rule-classes :rewrite)