Generate a shallowly embedded ACL2 if call.
(atj-gen-shallow-if-call test-block then-block else-block test-expr then-expr else-expr test-term types jvar-tmp-base jvar-tmp-index) → (mv block expr new-jvar-tmp-index)
This is called after translating the arguments of if to Java. The resulting blocks and expressions are passed as parameters here, along with the original ACL2 term that is the if test.
If the test has type
Consider a call
<test-block> <type> <tmp>; if (<test>) { <then-block> <tmp> = <then-expr>; } else { <else-block> <tmp> = <else-expr>; }
and the Java expression
In other words, we first compute the test and create a local variable to store the final result. Based on the test, we execute either branch (for non-strictness), storing the result into the variable.
The type
If the flag *atj-gen-cond-exprs* is set,
and if both
<test-block>
and the Java expression
<test> ? <then-expr> : <else-expr>
Function:
(defun atj-gen-shallow-if-call (test-block then-block else-block test-expr then-expr else-expr test-term types jvar-tmp-base jvar-tmp-index) (declare (xargs :guard (and (jblockp test-block) (jblockp then-block) (jblockp else-block) (jexprp test-expr) (jexprp then-expr) (jexprp else-expr) (pseudo-termp test-term) (atj-type-listp types) (stringp jvar-tmp-base) (posp jvar-tmp-index)))) (declare (xargs :guard (consp types))) (let ((__function__ 'atj-gen-shallow-if-call)) (declare (ignorable __function__)) (b* (((mv & & test-types) (atj-type-unwrap-term test-term)) (test-expr (if (equal test-types (list (atj-type-acl2 (atj-atype-boolean)))) test-expr (jexpr-binary (jbinop-ne) test-expr (atj-gen-symbol nil t nil)))) ((when (and *atj-gen-cond-exprs* (null then-block) (null else-block))) (b* ((block (jblock-fix test-block)) (expr (jexpr-cond test-expr then-expr else-expr))) (mv block expr jvar-tmp-index))) (jtype (atj-gen-shallow-jtype types)) ((mv result-locvar-block jvar-tmp jvar-tmp-index) (atj-gen-jlocvar-indexed jtype jvar-tmp-base jvar-tmp-index nil)) (if-block (jblock-ifelse test-expr (append then-block (jblock-asg-name jvar-tmp then-expr)) (append else-block (jblock-asg-name jvar-tmp else-expr)))) (block (append (jblock-fix test-block) result-locvar-block if-block)) (expr (jexpr-name jvar-tmp))) (mv block expr jvar-tmp-index))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-if-call.block (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-if-call test-block then-block else-block test-expr then-expr else-expr test-term types jvar-tmp-base jvar-tmp-index))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-shallow-if-call.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-if-call test-block then-block else-block test-expr then-expr else-expr test-term types jvar-tmp-base jvar-tmp-index))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atj-gen-shallow-if-call.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-if-call test-block then-block else-block test-expr then-expr else-expr test-term types jvar-tmp-base jvar-tmp-index))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)