Generate a shallowly embedded ACL2 named function call.
(atj-gen-shallow-fn-call fn args arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg guards$) → (mv block expr new-jvar-tmp-index)
Calls of if are handled via a separate function, non-strictly.
We only pass one of
Calls of and are also handled via a separate function.
Recall that and calls are
if calls of the form
Calls of or are also handled via a separate function.
Recall that or calls are
if calls of the form
If
In all other cases, in which the call is always strict, we generate a call of the method that corresponds to the function, and finally we wrap that into a Java conversion if needed. (We treat the Java abstract syntax somewhat improperly here, by using a generic method call with a possibly qualified method name, which should be therefore a static method call; this still produces correct Java code, but it should be handled more properly in a future version of this implementation.) Note that, because of the type annotations of the ACL2 terms, the actual argument expressions will have types appropriate to the method's formal argument types.
Function:
(defun atj-gen-shallow-fn-call (fn args arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg guards$) (declare (xargs :guard (and (symbolp fn) (pseudo-term-listp args) (jblock-listp arg-blocks) (jexpr-listp arg-exprs) (atj-type-listp src-types) (atj-type-listp dst-types) (stringp jvar-tmp-base) (posp jvar-tmp-index) (string-string-alistp pkg-class-names) (symbol-string-alistp fn-method-names) (stringp curr-pkg) (booleanp guards$)))) (declare (xargs :guard (and (= (len args) (len arg-blocks)) (= (len args) (len arg-exprs)) (consp src-types) (consp dst-types) (not (equal curr-pkg ""))))) (let ((__function__ 'atj-gen-shallow-fn-call)) (declare (ignorable __function__)) (b* (((when (and (eq fn 'if) (int= (len args) 3))) (b* (((mv test-block then-block else-block) (atj-jblock-list-to-3-jblocks arg-blocks)) ((mv test-expr then-expr else-expr) (atj-jexpr-list-to-3-jexprs arg-exprs))) (atj-gen-shallow-if-call test-block then-block else-block test-expr then-expr else-expr (first args) dst-types jvar-tmp-base jvar-tmp-index))) ((when (and (eq fn 'and) (int= (len args) 2))) (b* (((mv left-block right-block) (atj-jblock-list-to-2-jblocks arg-blocks)) ((mv left-expr right-expr) (atj-jexpr-list-to-2-jexprs arg-exprs)) ((mv & & left-types) (atj-type-unwrap-term (first args))) ((mv & & right-types) (atj-type-unwrap-term (second args)))) (atj-gen-shallow-and-call left-block right-block left-expr right-expr left-types right-types jvar-tmp-base jvar-tmp-index))) ((when (and (eq fn 'or) (int= (len args) 2))) (b* (((mv left-block right-block) (atj-jblock-list-to-2-jblocks arg-blocks)) ((mv left-expr right-expr) (atj-jexpr-list-to-2-jexprs arg-exprs)) ((mv & & types) (atj-type-unwrap-term (second args)))) (atj-gen-shallow-or-call left-block right-block left-expr right-expr types jvar-tmp-base jvar-tmp-index))) ((when (and guards$ (eq fn 'not) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-not-call (car arg-blocks) (car arg-exprs) (car args) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprim-constr-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprim-constr-call fn (car arg-blocks) (car arg-exprs) (car args) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprim-deconstr-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprim-deconstr-call fn (car arg-blocks) (car arg-exprs) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprim-unop-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprim-unop-call fn (car arg-blocks) (car arg-exprs) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprim-binop-fn-p fn) (int= (len args) 2))) (b* (((mv left-block right-block) (atj-jblock-list-to-2-jblocks arg-blocks)) ((mv left-expr right-expr) (atj-jexpr-list-to-2-jexprs arg-exprs)) ((mv block expr) (atj-gen-shallow-jprim-binop-call fn left-block right-block left-expr right-expr src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprim-conv-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprim-conv-call fn (car arg-blocks) (car arg-exprs) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprimarr-read-fn-p fn) (int= (len args) 2))) (b* (((mv array-block index-block) (atj-jblock-list-to-2-jblocks arg-blocks)) ((mv array-expr index-expr) (atj-jexpr-list-to-2-jexprs arg-exprs)) ((mv block expr) (atj-gen-shallow-jprimarr-read-call array-block index-block array-expr index-expr src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprimarr-length-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprimarr-length-call (car arg-blocks) (car arg-exprs) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprimarr-write-fn-p fn) (int= (len args) 3))) (b* (((mv array-block index-block component-block) (atj-jblock-list-to-3-jblocks arg-blocks)) ((mv array-expr index-expr component-expr) (atj-jexpr-list-to-3-jexprs arg-exprs)) ((mv 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))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprimarr-new-len-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprimarr-new-len-call fn (car arg-blocks) (car arg-exprs) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprimarr-new-init-fn-p fn))) (b* (((mv block expr) (atj-gen-shallow-jprimarr-new-init-call fn arg-blocks arg-exprs src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprimarr-conv-fromlist-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprimarr-conv-fromlist-call fn (car arg-blocks) (car arg-exprs) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (and guards$ (atj-jprimarr-conv-tolist-fn-p fn) (int= (len args) 1))) (b* (((mv block expr) (atj-gen-shallow-jprimarr-conv-tolist-call fn (car arg-blocks) (car arg-exprs) src-types dst-types))) (mv block expr jvar-tmp-index))) ((when (eq fn 'mv)) (b* (((mv block expr) (atj-gen-shallow-mv-call arg-blocks arg-exprs src-types dst-types guards$))) (mv block expr jvar-tmp-index))) (expr (jexpr-method (atj-gen-shallow-fnname fn pkg-class-names fn-method-names curr-pkg) arg-exprs)) ((unless (= (len src-types) (len dst-types))) (raise "Internal error: ~ the source types ~x0 and destination types ~x1 ~ differ in number." src-types dst-types) (mv nil (jexpr-name "irrelevant") jvar-tmp-index)) ((mv adapt-block expr jvar-tmp-index) (atj-adapt-expr-to-types expr src-types dst-types jvar-tmp-base jvar-tmp-index guards$))) (mv (append (flatten (jblock-list-fix arg-blocks)) adapt-block) expr jvar-tmp-index))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-fn-call.block (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-fn-call fn args arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg guards$))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-shallow-fn-call.expr (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-fn-call fn args arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg guards$))) (jexprp expr)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atj-gen-shallow-fn-call.new-jvar-tmp-index (implies (posp jvar-tmp-index) (b* (((mv common-lisp::?block ?expr ?new-jvar-tmp-index) (atj-gen-shallow-fn-call fn args arg-blocks arg-exprs src-types dst-types jvar-tmp-base jvar-tmp-index pkg-class-names fn-method-names curr-pkg guards$))) (posp new-jvar-tmp-index))) :rule-classes :rewrite)