Generate a shallowly embedded ACL2 call of a Java primitive array length operation.
(atj-gen-shallow-jprimarr-length-call array-block array-expr src-types dst-types) → (mv block expr)
This is called only if
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
Function:
(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:
(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:
(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)