		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-convert-expr-to-jprimarr-method

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

Signature
(atj-convert-expr-to-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-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 <type> is a Java primitive type and <conv-type(...)> is the conversion code generated by atj-convert-expr-to-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 from the Acl2Symbols in the list to Java booleans.

Definitions and Theorems

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

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

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

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

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

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