		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-if-call

Generate a shallowly embedded ACL2 if call.

Signature
(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)
Arguments: test-block — Guard (jblockp test-block).; then-block — Guard (jblockp then-block).; else-block — Guard (jblockp else-block).; test-expr — Guard (jexprp test-expr).; then-expr — Guard (jexprp then-expr).; else-expr — Guard (jexprp else-expr).; test-term — Guard (pseudo-termp test-term).; types — Guard (atj-type-listp types).; jvar-tmp-base — Guard (stringp jvar-tmp-base).; jvar-tmp-index — Guard (posp jvar-tmp-index).
Returns: block — Type (jblockp block).; expr — Type (jexprp expr).; new-jvar-tmp-index — Type (posp new-jvar-tmp-index), given (posp 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 :aboolean, which may only happen if :guards is t, in which case ACL2 booleans are mapped to Java booleans, we return the resulting expression. If instead the test has a different type, which must be an :acl2 type, we convert the resulting expression to a Java boolean by comparing it with nil for inequality.

Consider a call (if test then else). If the Java code generated for test consists of the block <test-block> and expression <test-expr>, and similarly for then and else, we generate the Java block

<test-block>
<type> <tmp>;
if (<test>) {
    <then-block>
    <tmp> = <then-expr>;
} else {
    <else-block>
    <tmp> = <else-expr>;
}

and the Java expression <tmp>, where <test> is <test-expr> if <test-expr> is boolean or <test-expr> != NIL otherwise, and where <tmp> consists of the base name in the parameter jvar-tmp-base followed by the numeric index in the parameter jvar-tmp-index.

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 <type> of the result variable is derived from the ATJ types passed as parameters. See atj-gen-shallow-fn-call for details.

If the flag *atj-gen-cond-exprs* is set, and if both <then-block> and <else-block> are empty, we generate the Java block

<test-block>

and the Java expression

<test> ? <then-expr> : <else-expr>

Definitions and Theorems

Function: atj-gen-shallow-if-call

(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: jblockp-of-atj-gen-shallow-if-call.block

(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: jexprp-of-atj-gen-shallow-if-call.expr

(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: posp-of-atj-gen-shallow-if-call.new-jvar-tmp-index

(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)