Map an ACL2 function that models a Java primitive constructor to the Java expression that constructs the primitive value, when the argument of the constructor is a quoted constant.
(atj-jprim-constr-fn-of-qconst-to-expr fn arg) → expr
The parameter
Function:
(defun atj-jprim-constr-fn-of-qconst-to-expr (fn arg) (declare (xargs :guard (atj-jprim-constr-fn-p fn))) (let ((__function__ 'atj-jprim-constr-fn-of-qconst-to-expr)) (declare (ignorable __function__)) (case fn (boolean-value (if (booleanp arg) (atj-gen-jboolean arg) (prog2$ (raise "Internal error: BOOLEAN-VALUE applied to ~x0." arg) (ec-call (jexpr-fix :irrelevant))))) (char-value (if (ubyte16p arg) (atj-gen-jchar arg) (prog2$ (raise "Internal error: CHAR-VALUE applied to ~x0." arg) (ec-call (jexpr-fix :irrelevant))))) (byte-value (if (sbyte8p arg) (atj-gen-jbyte arg) (prog2$ (raise "Internal error: BYTE-VALUE applied to ~x0." arg) (ec-call (jexpr-fix :irrelevant))))) (short-value (if (sbyte16p arg) (atj-gen-jshort arg) (prog2$ (raise "Internal error: SHORT-VALUE applied to ~x0." arg) (ec-call (jexpr-fix :irrelevant))))) (int-value (if (sbyte32p arg) (atj-gen-jint arg) (prog2$ (raise "Internal error: INT-VALUE applied to ~x0." arg) (ec-call (jexpr-fix :irrelevant))))) (long-value (if (sbyte64p arg) (atj-gen-jlong arg) (prog2$ (raise "Internal error: LONG-VALUE applied to ~x0." arg) (ec-call (jexpr-fix :irrelevant))))) (t (prog2$ (impossible) (ec-call (jexpr-fix :irrelevant)))))))
Theorem:
(defthm jexprp-of-atj-jprim-constr-fn-of-qconst-to-expr (b* ((expr (atj-jprim-constr-fn-of-qconst-to-expr fn arg))) (jexprp expr)) :rule-classes :rewrite)