		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-convert-expr-from-jprim

Convert a Java expression from a Java primitive type.

Signature
(atj-convert-expr-from-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 calls of Java primitive deconstructors like byte-value->int.

If the type is boolean, the deconstructor is boolean-value->bool, whose input ATJ type is :jboolean and whose output ATJ type is :aboolean. If :guards is t, ACL2 booleans are represented as Java booleans, and :aboolean is mapped to Java boolean like :jboolean; 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 via a Java conditional expression.

If the type is char, byte, short, int, or long, we convert it to an Acl2Integer by calling make. The method called is Acl2Integer.make(int) if the type is char, byte, short, or int, while it is Acl2Integer.make(long) if the type is long.

If the type is float or 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-from-jprim

(defun atj-convert-expr-from-jprim (expr type guards$)
 (declare (xargs :guard (and (jexprp expr)
                             (primitive-typep type)
                             (booleanp guards$))))
 (let ((__function__ 'atj-convert-expr-from-jprim))
  (declare (ignorable __function__))
  (case (primitive-type-kind type)
   (:boolean (if guards$ (jexpr-fix expr)
               (jexpr-cond expr (atj-gen-symbol t t nil)
                           (atj-gen-symbol nil t nil))))
   ((:char :byte :short :int :long)
    (jexpr-smethod *aij-type-int* "make" (list expr)))
   (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-from-jprim

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

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

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

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

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

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

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

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

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

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

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

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

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