Method to convert a Java expression from a Java primitive array type.
(atj-convert-expr-from-jprimarr-method type) → method
This is used to translate calls of Java primitive array conversions like byte-array-to-sbyte8-list.
We want to convert the array to a corresponding ACL2 list,
whose elements are instances of (subtypes of)
This function generates these methods,
one for each Java primitive type except
The method has the following form:
private static Acl2Value <name>(<type>[] array) { Acl2Value result = Acl2Symbol.NIL; int index = array.length - 1; while (index >= 0) { result = Acl2ConsPair.make(<conv-type(array[index])>, result); --index; } return result; }
where
Note that we generate an expression name for
Function:
(defun atj-convert-expr-from-jprimarr-method (type) (declare (xargs :guard (primitive-typep type))) (let ((__function__ 'atj-convert-expr-from-jprimarr-method)) (declare (ignorable __function__)) (b* ((method-name (atj-convert-expr-from-jprimarr-method-name type)) (jtype (atj-type-to-jitype (atj-type-jprim type))) (array "array") (index "index") (result "result") (array[index] (jexpr-array (jexpr-name array) (jexpr-name index))) (conv-array[index] (atj-convert-expr-from-jprim array[index] type nil)) (method-body (append (jblock-locvar *aij-type-value* result (atj-gen-symbol nil t nil)) (jblock-locvar (jtype-int) index (jexpr-binary (jbinop-sub) (jexpr-name (str::cat array "." "length")) (jexpr-literal-1))) (jblock-while (jexpr-binary (jbinop-ge) (jexpr-name index) (jexpr-literal-0)) (append (jblock-asg (jexpr-name result) (jexpr-smethod *aij-type-cons* "make" (list conv-array[index] (jexpr-name result)))) (jblock-expr (jexpr-unary (junop-predec) (jexpr-name index))))) (jblock-return (jexpr-name result))))) (make-jmethod :access (jaccess-private) :abstract? nil :static? t :final? nil :synchronized? nil :native? nil :strictfp? nil :result (jresult-type *aij-type-value*) :name method-name :params (list (jparam nil (jtype-array jtype) array)) :throws nil :body method-body))))
Theorem:
(defthm jmethodp-of-atj-convert-expr-from-jprimarr-method (b* ((method (atj-convert-expr-from-jprimarr-method type))) (jmethodp method)) :rule-classes :rewrite)
Theorem:
(defthm atj-convert-expr-from-jprimarr-method-of-primitive-type-fix-type (equal (atj-convert-expr-from-jprimarr-method (primitive-type-fix type)) (atj-convert-expr-from-jprimarr-method type)))
Theorem:
(defthm atj-convert-expr-from-jprimarr-method-primitive-type-equiv-congruence-on-type (implies (primitive-type-equiv type type-equiv) (equal (atj-convert-expr-from-jprimarr-method type) (atj-convert-expr-from-jprimarr-method type-equiv))) :rule-classes :congruence)