Convert a Java expression from a Java primitive type.
(atj-convert-expr-from-jprim expr type guards$) → new-expr
This is used to translate calls of Java primitive deconstructors like byte-value->int.
If the type is
If the type is
If the type is
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)