		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-jprimarr-length-call

Generate a shallowly embedded ACL2 call of a Java primitive array length operation.

Signature
(atj-gen-shallow-jprimarr-length-call array-block array-expr src-types dst-types) → (mv block expr)
Arguments: array-block — Guard (jblockp array-block).; array-expr — Guard (jexprp array-expr).; src-types — Guard (atj-type-listp src-types).; dst-types — Guard (atj-type-listp dst-types).
Returns: block — Type (jblockp block).; expr — Type (jexprp expr).

This is called only if :guards is t. This is called after translating the array to Java. The resulting block and expression are passed as parameters here.

We generate a Java field access expression for the length.

Note that if the array expression is an expression name, we generate an expression name as the resulting expression, because grammatically this is not a field access expression in Java: it cannot be generated from the nonterminal field-acces; it can be generated from the nonterminal expression-name.

Definitions and Theorems

Function: atj-gen-shallow-jprimarr-length-call

(defun atj-gen-shallow-jprimarr-length-call
       (array-block array-expr src-types dst-types)
 (declare (xargs :guard (and (jblockp array-block)
                             (jexprp array-expr)
                             (atj-type-listp src-types)
                             (atj-type-listp dst-types))))
 (declare (xargs :guard (and (consp src-types)
                             (consp dst-types))))
 (let ((__function__ 'atj-gen-shallow-jprimarr-length-call))
  (declare (ignorable __function__))
  (b* ((expr (if (jexpr-case array-expr :name)
                 (jexpr-name (str::cat (jexpr-name->get array-expr)
                                       ".length"))
               (jexpr-field array-expr "length"))))
   (mv
      (jblock-fix array-block)
      (atj-adapt-expr-to-type expr (atj-type-list-to-type src-types)
                              (atj-type-list-to-type dst-types)
                              t)))))

Theorem: jblockp-of-atj-gen-shallow-jprimarr-length-call.block

(defthm jblockp-of-atj-gen-shallow-jprimarr-length-call.block
  (b* (((mv common-lisp::?block ?expr)
        (atj-gen-shallow-jprimarr-length-call
             array-block
             array-expr src-types dst-types)))
    (jblockp block))
  :rule-classes :rewrite)

Theorem: jexprp-of-atj-gen-shallow-jprimarr-length-call.expr

(defthm jexprp-of-atj-gen-shallow-jprimarr-length-call.expr
  (b* (((mv common-lisp::?block ?expr)
        (atj-gen-shallow-jprimarr-length-call
             array-block
             array-expr src-types dst-types)))
    (jexprp expr))
  :rule-classes :rewrite)