		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-or-call

Generate a shallowly embedded ACL2 or call.

Signature
(atj-gen-shallow-or-call left-block right-block left-expr right-expr types jvar-tmp-base jvar-tmp-index) → (mv block expr new-jvar-tmp-index)
Arguments: left-block — Guard (jblockp left-block).; right-block — Guard (jblockp right-block).; left-expr — Guard (jexprp left-expr).; right-expr — Guard (jexprp right-expr).; 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 to Java. The resulting blocks and expressions are passed as parameters here.

Recall that ATJ's pre-translation (see atj-pre-translation-disjunctions) turns (annotated) terms (if a a b) into (or a b). Here we recognize, and treat specially, these or calls.

The parameter types is the type (list) of both operands. They have the same type because the type annotation step ensures that both branches of ifs, including those of the form (if a a b) that are turned into (or a b), have the same types.

If both operands have type :aboolean, we generate the block <left-block> and the non-strict expression <left-expr> || <right-expr>: in other words, we translate ACL2's boolean or calls (in the original term) to a || binary expression in Java, preceded by any computations needed by <left-expr>; but this is possible only if the calculation of the right operand, which must be executed only if the first operand is true, involves just an expression <right-expr> and not a (non-empty) block <right-block>. In all other cases, we generate the block

<left-block>
<type> <tmp> = <a-expr>;
if (<tmp> == NIL) {
    <b-block>
    <tmp> = <b-expr>;
}

and the Java expression <tmp>, where: <tmp> consists of the base name in the parameter jvar-tmp-base followed by the numeric index in the parameter jvar-tmp-index; and <type> is the Java type of the operands.

Definitions and Theorems

Function: atj-gen-shallow-or-call

(defun atj-gen-shallow-or-call
       (left-block right-block left-expr right-expr
                   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 types)
                             (stringp jvar-tmp-base)
                             (posp jvar-tmp-index))))
 (declare (xargs :guard (consp types)))
 (let ((__function__ 'atj-gen-shallow-or-call))
  (declare (ignorable __function__))
  (if (and (equal types
                  (list (atj-type-acl2 (atj-atype-boolean))))
           (null right-block))
      (mv (jblock-fix left-block)
          (jexpr-binary (jbinop-condor)
                        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 types)
           jvar-tmp-base jvar-tmp-index left-expr))
     (if-block
        (jblock-if (jexpr-binary (jbinop-eq)
                                 (jexpr-name jvar-tmp)
                                 (atj-gen-symbol nil t nil))
                   (append right-block
                           (jblock-asg-name jvar-tmp right-expr)))))
    (mv (append (jblock-fix left-block)
                tmp-locvar-block if-block)
        (jexpr-name jvar-tmp)
        jvar-tmp-index)))))

Theorem: jblockp-of-atj-gen-shallow-or-call.block

(defthm jblockp-of-atj-gen-shallow-or-call.block
  (b*
    (((mv common-lisp::?block
          ?expr ?new-jvar-tmp-index)
      (atj-gen-shallow-or-call left-block
                               right-block left-expr right-expr
                               types jvar-tmp-base jvar-tmp-index)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: jexprp-of-atj-gen-shallow-or-call.expr

(defthm jexprp-of-atj-gen-shallow-or-call.expr
  (b*
    (((mv common-lisp::?block
          ?expr ?new-jvar-tmp-index)
      (atj-gen-shallow-or-call left-block
                               right-block left-expr right-expr
                               types jvar-tmp-base jvar-tmp-index)))
    (jexprp expr))
  :rule-classes :rewrite)

Theorem: posp-of-atj-gen-shallow-or-call.new-jvar-tmp-index

(defthm posp-of-atj-gen-shallow-or-call.new-jvar-tmp-index
 (implies
   (posp jvar-tmp-index)
   (b*
    (((mv common-lisp::?block
          ?expr ?new-jvar-tmp-index)
      (atj-gen-shallow-or-call left-block
                               right-block left-expr right-expr
                               types jvar-tmp-base jvar-tmp-index)))
    (posp new-jvar-tmp-index)))
 :rule-classes :rewrite)