		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-and-call

Generate a shallowly embedded ACL2 and call.

Signature
(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)
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).; left-types — Guard (atj-type-listp left-types).; right-types — Guard (atj-type-listp right-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-conjunctions) turns (annotated) terms (if a b nil) into (and a b). Here we recognize, and treat specially, these and calls.

If both operands have type :aboolean and <right-block is empty, we generate the block <left-block> and the non-strict expression <left-expr> && <right-expr>: in other words, we translate ACL2's boolean and 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>
<right-type> <tmp>;
if (<left-test>) {
    <right-block>
    <tmp> = <right-expr>;
} else {
    <tmp> = <false/NIL>;
}

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; <right-type> is the Java type of the right operand; <left-test> is <left-expr> if boolean, or otherwise <left-expr> != NIL; and <false/NIL> is false if <right-type> is boolean or otherwise NIL (note that these are the only two possible translations of nil).

Definitions and Theorems

Function: atj-gen-shallow-and-call

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

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

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

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