		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-convert-expr-from-jprimarr-method

Method to convert a Java expression from a Java primitive array type.

Signature
(atj-convert-expr-from-jprimarr-method type) → method
Arguments: type — Guard (primitive-typep type).
Returns: method — Type (jmethodp 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) Acl2Value obtained by converting the components of the array. This should be done with a Java loop, of course. However, we want the conversion code generated from the deconstructors 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.

This function generates these methods, one for each Java primitive type except float and double. These methods are generated directly in the main Java class. The method names are chosen to avoid conflicts with other generated methods in the same class.

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 <type> is a Java primitive type and <conv-type(...)> is the conversion code generated by atj-convert-expr-from-jprim for that primitive type. We pass nil as guards$ argument to that function, even though this array conversion method is only relevant when :guards is t, because, in the case of boolean arrays, we need to actually convert to the Acl2Symbols in the list from Java booleans.

Note that we generate an expression name for array.length, because grammatically this is not a field access expression in Java: it cannot be generated from the nonterminal field-acces; it can be generated from the nonterminal expression-name.

Definitions and Theorems

Function: atj-convert-expr-from-jprimarr-method

(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: jmethodp-of-atj-convert-expr-from-jprimarr-method

(defthm jmethodp-of-atj-convert-expr-from-jprimarr-method
  (b* ((method (atj-convert-expr-from-jprimarr-method type)))
    (jmethodp method))
  :rule-classes :rewrite)

Theorem: atj-convert-expr-from-jprimarr-method-of-primitive-type-fix-type

(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: atj-convert-expr-from-jprimarr-method-primitive-type-equiv-congruence-on-type

(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)