Generate the Java code for a test value.
(atj-gen-test-value tvalue jvar-value-base jvar-value-index deep$ guards$) → (mv block expr type new-jvar-value-index)
We use atj-gen-value for
For
In both cases, we also return the ATJ type of the expression. In the shallow embedding, this will determine the Java type of the local variable that stores the value.
Function:
(defun atj-gen-test-value (tvalue jvar-value-base jvar-value-index deep$ guards$) (declare (xargs :guard (and (atj-test-valuep tvalue) (stringp jvar-value-base) (posp jvar-value-index) (booleanp deep$) (booleanp guards$)))) (let ((__function__ 'atj-gen-test-value)) (declare (ignorable __function__)) (atj-test-value-case tvalue :acl2 (b* (((mv block expr jvar-value-index) (atj-gen-value tvalue.get jvar-value-base jvar-value-index deep$ guards$))) (mv block expr (atj-type-of-value tvalue.get) jvar-value-index)) :jboolean (mv nil (atj-gen-jboolean (boolean-value->bool tvalue.get)) (atj-type-jprim (primitive-type-boolean)) jvar-value-index) :jchar (mv nil (atj-gen-jchar (char-value->nat tvalue.get)) (atj-type-jprim (primitive-type-char)) jvar-value-index) :jbyte (mv nil (atj-gen-jbyte (byte-value->int tvalue.get)) (atj-type-jprim (primitive-type-byte)) jvar-value-index) :jshort (mv nil (atj-gen-jshort (short-value->int tvalue.get)) (atj-type-jprim (primitive-type-short)) jvar-value-index) :jint (mv nil (atj-gen-jint (int-value->int tvalue.get)) (atj-type-jprim (primitive-type-int)) jvar-value-index) :jlong (mv nil (atj-gen-jlong (long-value->int tvalue.get)) (atj-type-jprim (primitive-type-long)) jvar-value-index) :jboolean[] (mv nil (atj-gen-jboolean-array tvalue.get) (atj-type-jprimarr (primitive-type-boolean)) jvar-value-index) :jchar[] (mv nil (atj-gen-jchar-array tvalue.get) (atj-type-jprimarr (primitive-type-char)) jvar-value-index) :jbyte[] (mv nil (atj-gen-jbyte-array tvalue.get) (atj-type-jprimarr (primitive-type-byte)) jvar-value-index) :jshort[] (mv nil (atj-gen-jshort-array tvalue.get) (atj-type-jprimarr (primitive-type-short)) jvar-value-index) :jint[] (mv nil (atj-gen-jint-array tvalue.get) (atj-type-jprimarr (primitive-type-int)) jvar-value-index) :jlong[] (mv nil (atj-gen-jlong-array tvalue.get) (atj-type-jprimarr (primitive-type-long)) jvar-value-index))))
Theorem:
(defthm jblockp-of-atj-gen-test-value.block (b* (((mv common-lisp::?block ?expr common-lisp::?type ?new-jvar-value-index) (atj-gen-test-value tvalue jvar-value-base jvar-value-index deep$ guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-test-value.expr (b* (((mv common-lisp::?block ?expr common-lisp::?type ?new-jvar-value-index) (atj-gen-test-value tvalue jvar-value-base jvar-value-index deep$ guards$))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm atj-typep-of-atj-gen-test-value.type (b* (((mv common-lisp::?block ?expr common-lisp::?type ?new-jvar-value-index) (atj-gen-test-value tvalue jvar-value-base jvar-value-index deep$ guards$))) (atj-typep type)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atj-gen-test-value.new-jvar-value-index (implies (posp jvar-value-index) (b* (((mv common-lisp::?block ?expr common-lisp::?type ?new-jvar-value-index) (atj-gen-test-value tvalue jvar-value-base jvar-value-index deep$ guards$))) (posp new-jvar-value-index))) :rule-classes :rewrite)