Generate a shallowly embedded ACL2 call of a Java primitive constructor.
(atj-gen-shallow-jprim-constr-call fn arg-block arg-expr arg-term src-types dst-types) → (mv block expr)
This is called only if
If the argument is a quoted constant,
the function call is translated
to the constant Java primitive expression
whose value is the quoted constant;
in this case, the
Function:
(defun atj-gen-shallow-jprim-constr-call (fn arg-block arg-expr arg-term src-types dst-types) (declare (xargs :guard (and (atj-jprim-constr-fn-p fn) (jblockp arg-block) (jexprp arg-expr) (pseudo-termp arg-term) (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-jprim-constr-call)) (declare (ignorable __function__)) (b* (((mv uarg & &) (atj-type-unwrap-term arg-term)) (src-type (atj-type-list-to-type src-types)) (dst-type (atj-type-list-to-type dst-types)) ((mv block expr) (if (pseudo-term-case uarg :quote) (b* ((val (pseudo-term-quote->val uarg))) (mv nil (atj-jprim-constr-fn-of-qconst-to-expr fn val))) (mv (jblock-fix arg-block) (atj-convert-expr-to-jprim arg-expr (atj-jprim-constr-fn-to-ptype fn) t)))) (expr (atj-adapt-expr-to-type expr src-type dst-type t))) (mv block expr))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-jprim-constr-call.block (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-jprim-constr-call fn arg-block arg-expr arg-term src-types dst-types))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-shallow-jprim-constr-call.expr (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-jprim-constr-call fn arg-block arg-expr arg-term src-types dst-types))) (jexprp expr)) :rule-classes :rewrite)