Method to convert a Java expression to a Java primitive array type.
(atj-convert-expr-to-jprimarr-method type) → method
This is used to translate calls of Java primitive array conversions like byte-array-from-sbyte8-list.
The Java expression must return an ACL2 list (assuming guard verification), which we want to convert to a corresponding Java array whose components are Java primitive values obtained by converting the elements of the list. This should be done with a Java loop, of course. However, we want the conversion code generated from the constructors to be a relatively simple ``inline'' expression. Thus, we generate private methods to perform the loop conversion, and translate the deconstructor calls to calls of these methods.
The generated method has the following form:
private static <type>[] <name>(Acl2Value list) { int length = 0; Acl2Value saveList = list; while (list instanceof Acl2Cons) { ++length; list = ((Acl2ConsPair) list).getCdr(); } <type>[] array = new <type>(length); int index = 0; list = savedList; while (index < length) { Acl2ConsPair pair = (Acl2ConsPair) list; array[index] = <conv-type(pair.getCar())>; list = pair.getCdr(); ++index; } return array; }
where
Function:
(defun atj-convert-expr-to-jprimarr-method (type) (declare (xargs :guard (primitive-typep type))) (let ((__function__ 'atj-convert-expr-to-jprimarr-method)) (declare (ignorable __function__)) (b* ((method-name (atj-convert-expr-to-jprimarr-method-name type)) (jtype (atj-type-to-jitype (atj-type-jprim type))) (array "array") (index "index") (length "length") (list "list") (pair "pair") (saved "savedList") (array[index] (jexpr-array (jexpr-name array) (jexpr-name index))) (pair.getcar (jexpr-imethod (jexpr-name pair) "getCar" nil)) (conv-pair.getcar (atj-convert-expr-to-jprim pair.getcar type nil)) (method-body (append (jblock-locvar (jtype-int) length (jexpr-literal-0)) (jblock-locvar *aij-type-value* saved (jexpr-name list)) (jblock-while (jexpr-instanceof (jexpr-name list) *aij-type-cons*) (append (jblock-expr (jexpr-unary (junop-preinc) (jexpr-name length))) (jblock-asg (jexpr-name list) (jexpr-imethod (jexpr-cast *aij-type-cons* (jexpr-name list)) "getCdr" nil)))) (jblock-locvar (jtype-array jtype) array (jexpr-newarray jtype (jexpr-name length))) (jblock-locvar (jtype-int) index (jexpr-literal-0)) (jblock-asg (jexpr-name list) (jexpr-name saved)) (jblock-while (jexpr-binary (jbinop-lt) (jexpr-name index) (jexpr-name length)) (append (jblock-locvar *aij-type-cons* pair (jexpr-cast *aij-type-cons* (jexpr-name list))) (jblock-asg array[index] conv-pair.getcar) (jblock-asg (jexpr-name list) (jexpr-imethod (jexpr-name pair) "getCdr" nil)) (jblock-expr (jexpr-unary (junop-preinc) (jexpr-name index))))) (jblock-return (jexpr-name array))))) (make-jmethod :access (jaccess-private) :abstract? nil :static? t :final? nil :synchronized? nil :native? nil :strictfp? nil :result (jresult-type (jtype-array jtype)) :name method-name :params (list (jparam nil *aij-type-value* list)) :throws nil :body method-body))))
Theorem:
(defthm jmethodp-of-atj-convert-expr-to-jprimarr-method (b* ((method (atj-convert-expr-to-jprimarr-method type))) (jmethodp method)) :rule-classes :rewrite)
Theorem:
(defthm atj-convert-expr-to-jprimarr-method-of-primitive-type-fix-type (equal (atj-convert-expr-to-jprimarr-method (primitive-type-fix type)) (atj-convert-expr-to-jprimarr-method type)))
Theorem:
(defthm atj-convert-expr-to-jprimarr-method-primitive-type-equiv-congruence-on-type (implies (primitive-type-equiv type type-equiv) (equal (atj-convert-expr-to-jprimarr-method type) (atj-convert-expr-to-jprimarr-method type-equiv))) :rule-classes :congruence)