		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-convert-expr-to-jprim

Convert a Java expression to a Java primitive type.

Signature
(atj-convert-expr-to-jprim expr type guards$) → new-expr
Arguments: expr — Guard (jexprp expr).; type — Guard (primitive-typep type).; guards$ — Guard (booleanp guards$).
Returns: new-expr — Type (jexprp new-expr).

This is used to translate some calls of Java primitive constructors like byte-value. (Other calls are translated to Java literals instead.)

If the type is boolean, the constructor is boolean-value, whose input ATJ type is :aboolean. If :guards is t, ACL2 booleans are represented as Java booleans, and :aboolean is mapped to Java boolean, so the expression must have type boolean already; thus, the conversion is a no-op. If :guards is nil, ACL2 booleans are represented as Acl2Symbols, and :aboolean is mapped to Acl2Symbol; thus, we convert the expression by comparing it with (the Java representation of) nil.

If the type is char, byte, or short, the input expression must have type Acl2Integer; see the input and output types of char-value, byte-value, and short-value. In this case, we convert the input expression by extracting a Java int from the Acl2Integer and we cast to the appropriate primitive type.

If the type is int, the input expression must have type Acl2Integer; see the input and output types of int-value. In this case, we convert the input expression by extracting a Java int from the Acl2Integer.

If the type is long, the input expression must have type Acl2Integer; see the input and output types of long-value. In this case, we convert the input expression by extracting a Java long from the Acl2Integer.

If the type is float and double, an error occurs. These conversions are not supported yet, because we have only an abstract model of these two types for now.

Definitions and Theorems

Function: atj-convert-expr-to-jprim

(defun atj-convert-expr-to-jprim (expr type guards$)
 (declare (xargs :guard (and (jexprp expr)
                             (primitive-typep type)
                             (booleanp guards$))))
 (let ((__function__ 'atj-convert-expr-to-jprim))
  (declare (ignorable __function__))
  (case (primitive-type-kind type)
   (:boolean (if guards$ (jexpr-fix expr)
               (jexpr-binary (jbinop-ne)
                             expr (atj-gen-symbol nil t nil))))
   ((:char :byte :short)
    (jexpr-cast (jtype-prim type)
                (jexpr-imethod (jexpr-cast *aij-type-int* expr)
                               "getJavaInt" nil)))
   (:int (jexpr-imethod (jexpr-cast *aij-type-int* expr)
                        "getJavaInt" nil))
   (:long (jexpr-imethod (jexpr-cast *aij-type-int* expr)
                         "getJavaLong" nil))
   (t
    (prog2$
     (raise
      "Internal error: ~
                       cannot convert expression ~x0 to type ~x1."
      expr type)
     (ec-call (jexpr-fix :irrelevant)))))))

Theorem: jexprp-of-atj-convert-expr-to-jprim

(defthm jexprp-of-atj-convert-expr-to-jprim
  (b* ((new-expr (atj-convert-expr-to-jprim expr type guards$)))
    (jexprp new-expr))
  :rule-classes :rewrite)

Theorem: atj-convert-expr-to-jprim-of-jexpr-fix-expr

(defthm atj-convert-expr-to-jprim-of-jexpr-fix-expr
  (equal (atj-convert-expr-to-jprim (jexpr-fix expr)
                                    type guards$)
         (atj-convert-expr-to-jprim expr type guards$)))

Theorem: atj-convert-expr-to-jprim-jexpr-equiv-congruence-on-expr

(defthm atj-convert-expr-to-jprim-jexpr-equiv-congruence-on-expr
  (implies
       (jexpr-equiv expr expr-equiv)
       (equal (atj-convert-expr-to-jprim expr type guards$)
              (atj-convert-expr-to-jprim expr-equiv type guards$)))
  :rule-classes :congruence)

Theorem: atj-convert-expr-to-jprim-of-primitive-type-fix-type

(defthm atj-convert-expr-to-jprim-of-primitive-type-fix-type
  (equal (atj-convert-expr-to-jprim expr (primitive-type-fix type)
                                    guards$)
         (atj-convert-expr-to-jprim expr type guards$)))

Theorem: atj-convert-expr-to-jprim-primitive-type-equiv-congruence-on-type

(defthm
  atj-convert-expr-to-jprim-primitive-type-equiv-congruence-on-type
  (implies
       (primitive-type-equiv type type-equiv)
       (equal (atj-convert-expr-to-jprim expr type guards$)
              (atj-convert-expr-to-jprim expr type-equiv guards$)))
  :rule-classes :congruence)

Theorem: atj-convert-expr-to-jprim-of-bool-fix-guards$

(defthm atj-convert-expr-to-jprim-of-bool-fix-guards$
 (equal
      (atj-convert-expr-to-jprim expr type (acl2::bool-fix guards$))
      (atj-convert-expr-to-jprim expr type guards$)))

Theorem: atj-convert-expr-to-jprim-iff-congruence-on-guards$

(defthm atj-convert-expr-to-jprim-iff-congruence-on-guards$
  (implies
       (iff guards$ guards$-equiv)
       (equal (atj-convert-expr-to-jprim expr type guards$)
              (atj-convert-expr-to-jprim expr type guards$-equiv)))
  :rule-classes :congruence)