Generate a shallowly embedded ACL2 call of a Java primitive write operation.
(atj-gen-shallow-jprimarr-write-call fn array-block index-block component-block array-expr index-expr component-expr src-types dst-types) → (mv block expr)
This is called only if
We generate a call of the Java method to write arrays.
Function:
(defun atj-gen-shallow-jprimarr-write-call (fn array-block index-block component-block array-expr index-expr component-expr src-types dst-types) (declare (xargs :guard (and (atj-jprimarr-write-fn-p fn) (jblockp array-block) (jblockp index-block) (jblockp component-block) (jexprp array-expr) (jexprp index-expr) (jexprp component-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-write-call)) (declare (ignorable __function__)) (b* ((block (append (jblock-fix array-block) (jblock-fix index-block) (jblock-fix component-block))) (expr (jexpr-method (atj-jprimarr-write-to-method-name fn) (list array-expr index-expr component-expr)))) (mv 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-write-call.block (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-jprimarr-write-call fn array-block index-block component-block array-expr index-expr component-expr src-types dst-types))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-shallow-jprimarr-write-call.expr (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-jprimarr-write-call fn array-block index-block component-block array-expr index-expr component-expr src-types dst-types))) (jexprp expr)) :rule-classes :rewrite)