Adapt a Java expression from a source type to a destination type.
This is used when generating shallowly embedded ACL2 calls of named functions. As explained in atj-types, when, for instance, the type of an actual argument of a function call is not the same as or a subtype (according to Java subtyping) of the type of the formal argument, ATJ adds Java code to convert from the former type to the latter type.
This code generation function does that.
The input Java expression is the one generated for the actual argument,
whose type is
To convert between the
Function:
(defun atj-adapt-expr-to-type (expr src-type dst-type guards$) (declare (xargs :guard (and (jexprp expr) (atj-typep src-type) (atj-typep dst-type) (booleanp guards$)))) (let ((__function__ 'atj-adapt-expr-to-type)) (declare (ignorable __function__)) (cond ((atj-type-equiv src-type dst-type) (jexpr-fix expr)) ((and (atj-type-case src-type :acl2) (atj-type-case dst-type :acl2)) (cond ((atj-type-<= src-type dst-type) (if guards$ (cond ((and (atj-atype-case (atj-type-acl2->get src-type) :boolean) (not (atj-atype-case (atj-type-acl2->get dst-type) :boolean))) (jexpr-cond expr (atj-gen-symbol t t nil) (atj-gen-symbol nil t nil))) ((and (atj-atype-case (atj-type-acl2->get src-type) :character) (not (atj-atype-case (atj-type-acl2->get dst-type) :character))) (jexpr-smethod *aij-type-char* "make" (list expr))) ((and (atj-atype-case (atj-type-acl2->get src-type) :string) (not (atj-atype-case (atj-type-acl2->get dst-type) :string))) (jexpr-smethod *aij-type-string* "make" (list expr))) (t (jexpr-fix expr))) (jexpr-fix expr))) ((atj-type-< dst-type src-type) (if guards$ (cond ((atj-atype-case (atj-type-acl2->get dst-type) :boolean) (jexpr-binary (jbinop-ne) expr (atj-gen-symbol nil t nil))) ((atj-atype-case (atj-type-acl2->get dst-type) :character) (jexpr-imethod (jexpr-cast *aij-type-char* expr) "getJavaChar" nil)) ((atj-atype-case (atj-type-acl2->get dst-type) :string) (jexpr-imethod (jexpr-cast *aij-type-string* expr) "getJavaString" nil)) (t (jexpr-cast (atj-type-to-jitype dst-type) expr))) (jexpr-cast (atj-type-to-jitype dst-type) expr))) (t (prog2$ (raise "Internal error: ~ unexpected conversion from ~x0 to ~x1." src-type dst-type) (jexpr-fix expr))))) (t (prog2$ (raise "Internal error: ~ unexpected conversion from ~x0 to ~x1." src-type dst-type) (jexpr-fix expr))))))
Theorem:
(defthm jexprp-of-atj-adapt-expr-to-type (b* ((new-expr (atj-adapt-expr-to-type expr src-type dst-type guards$))) (jexprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm atj-adapt-expr-to-type-of-jexpr-fix-expr (equal (atj-adapt-expr-to-type (jexpr-fix expr) src-type dst-type guards$) (atj-adapt-expr-to-type expr src-type dst-type guards$)))
Theorem:
(defthm atj-adapt-expr-to-type-jexpr-equiv-congruence-on-expr (implies (jexpr-equiv expr expr-equiv) (equal (atj-adapt-expr-to-type expr src-type dst-type guards$) (atj-adapt-expr-to-type expr-equiv src-type dst-type guards$))) :rule-classes :congruence)
Theorem:
(defthm atj-adapt-expr-to-type-of-atj-type-fix-src-type (equal (atj-adapt-expr-to-type expr (atj-type-fix src-type) dst-type guards$) (atj-adapt-expr-to-type expr src-type dst-type guards$)))
Theorem:
(defthm atj-adapt-expr-to-type-atj-type-equiv-congruence-on-src-type (implies (atj-type-equiv src-type src-type-equiv) (equal (atj-adapt-expr-to-type expr src-type dst-type guards$) (atj-adapt-expr-to-type expr src-type-equiv dst-type guards$))) :rule-classes :congruence)
Theorem:
(defthm atj-adapt-expr-to-type-of-atj-type-fix-dst-type (equal (atj-adapt-expr-to-type expr src-type (atj-type-fix dst-type) guards$) (atj-adapt-expr-to-type expr src-type dst-type guards$)))
Theorem:
(defthm atj-adapt-expr-to-type-atj-type-equiv-congruence-on-dst-type (implies (atj-type-equiv dst-type dst-type-equiv) (equal (atj-adapt-expr-to-type expr src-type dst-type guards$) (atj-adapt-expr-to-type expr src-type dst-type-equiv guards$))) :rule-classes :congruence)
Theorem:
(defthm atj-adapt-expr-to-type-of-bool-fix-guards$ (equal (atj-adapt-expr-to-type expr src-type dst-type (acl2::bool-fix guards$)) (atj-adapt-expr-to-type expr src-type dst-type guards$)))
Theorem:
(defthm atj-adapt-expr-to-type-iff-congruence-on-guards$ (implies (iff guards$ guards$-equiv) (equal (atj-adapt-expr-to-type expr src-type dst-type guards$) (atj-adapt-expr-to-type expr src-type dst-type guards$-equiv))) :rule-classes :congruence)