Map an ACL2 function that models a Java primitive conversion to the result Java type of the conversion.
(atj-jprim-conv-fn-to-jtype fn) → type
Function:
(defun atj-jprim-conv-fn-to-jtype (fn) (declare (xargs :guard (atj-jprim-conv-fn-p fn))) (let ((__function__ 'atj-jprim-conv-fn-to-jtype)) (declare (ignorable __function__)) (case fn (byte-to-short (jtype-short)) (byte-to-int (jtype-int)) (byte-to-long (jtype-long)) (byte-to-float (jtype-float)) (byte-to-double (jtype-double)) (short-to-int (jtype-int)) (short-to-long (jtype-long)) (short-to-float (jtype-float)) (short-to-double (jtype-double)) (char-to-int (jtype-int)) (char-to-long (jtype-long)) (char-to-float (jtype-float)) (char-to-double (jtype-double)) (int-to-long (jtype-long)) (int-to-float (jtype-float)) (int-to-double (jtype-double)) (long-to-float (jtype-float)) (long-to-double (jtype-double)) (float-to-double (jtype-double)) (short-to-byte (jtype-byte)) (short-to-char (jtype-char)) (char-to-byte (jtype-byte)) (char-to-short (jtype-short)) (int-to-byte (jtype-byte)) (int-to-short (jtype-short)) (int-to-char (jtype-char)) (long-to-byte (jtype-byte)) (long-to-short (jtype-short)) (long-to-char (jtype-char)) (long-to-int (jtype-int)) (float-to-byte (jtype-byte)) (float-to-short (jtype-short)) (float-to-char (jtype-char)) (float-to-int (jtype-int)) (float-to-long (jtype-long)) (double-to-byte (jtype-byte)) (double-to-short (jtype-short)) (double-to-char (jtype-char)) (double-to-int (jtype-int)) (double-to-long (jtype-long)) (double-to-float (jtype-float)) (byte-to-char (jtype-char)) (t (prog2$ (impossible) (ec-call (jtype-fix :irrelevant)))))))
Theorem:
(defthm jtypep-of-atj-jprim-conv-fn-to-jtype (b* ((type (atj-jprim-conv-fn-to-jtype fn))) (jtypep type)) :rule-classes :rewrite)