Generate a shallowly embedded ACL2 and call.
(atj-gen-shallow-and-call left-block right-block left-expr right-expr left-types right-types jvar-tmp-base jvar-tmp-index) → (mv block expr new-jvar-tmp-index)
This is called after translating the arguments to Java. The resulting blocks and expressions are passed as parameters here.
Recall that ATJ's pre-translation
(see atj-pre-translation-conjunctions)
turns (annotated) terms
If both operands have type
<left-block> <right-type> <tmp>; if (<left-test>) { <right-block> <tmp> = <right-expr>; } else { <tmp> = <false/NIL>; }
and the Java expression
Function:
(defun atj-gen-shallow-and-call (left-block right-block left-expr right-expr left-types right-types jvar-tmp-base jvar-tmp-index) (declare (xargs :guard (and (jblockp left-block) (jblockp right-block) (jexprp left-expr) (jexprp right-expr) (atj-type-listp left-types) (atj-type-listp right-types) (stringp jvar-tmp-base) (posp jvar-tmp-index)))) (declare (xargs :guard (and (consp left-types) (consp right-types)))) (let ((__function__ 'atj-gen-shallow-and-call)) (declare (ignorable __function__)) (if (and (equal left-types (list (atj-type-acl2 (atj-atype-boolean)))) (equal right-types (list (atj-type-acl2 (atj-atype-boolean)))) (null right-block)) (mv (jblock-fix left-block) (jexpr-binary (jbinop-condand) left-expr right-expr) jvar-tmp-index) (b* (((mv tmp-locvar-block jvar-tmp jvar-tmp-index) (atj-gen-jlocvar-indexed (atj-gen-shallow-jtype right-types) jvar-tmp-base jvar-tmp-index nil)) (test (if (equal left-types (list (atj-type-acl2 (atj-atype-boolean)))) left-expr (jexpr-binary (jbinop-ne) left-expr (atj-gen-symbol nil t nil)))) (false/nil (if (equal right-types (list (atj-type-acl2 (atj-atype-boolean)))) (jexpr-literal-false) (atj-gen-symbol nil t nil))) (if-block (jblock-ifelse test (append right-block (jblock-asg-name jvar-tmp right-expr)) (jblock-asg-name jvar-tmp false/nil)))) (mv (append (jblock-fix left-block) tmp-locvar-block if-block) (jexpr-name jvar-tmp) jvar-tmp-index)))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-and-call.block (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-and-call left-block right-block left-expr right-expr left-types right-types jvar-tmp-base jvar-tmp-index))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-shallow-and-call.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-and-call left-block right-block left-expr right-expr left-types right-types jvar-tmp-base jvar-tmp-index))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atj-gen-shallow-and-call.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-and-call left-block right-block left-expr right-expr left-types right-types jvar-tmp-base jvar-tmp-index))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)