Generate a shallowly embedded ACL2 not call.
(atj-gen-shallow-not-call arg-block arg-expr arg-term src-types dst-types) → (mv block expr)
This is called only if
If the argument has type
In any case, we never generate a call of the Java method for not. That method is still generated for external code to call though.
Function:
(defun atj-gen-shallow-not-call (arg-block arg-expr arg-term src-types dst-types) (declare (xargs :guard (and (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-not-call)) (declare (ignorable __function__)) (b* (((mv & & arg-types) (atj-type-unwrap-term arg-term)) (expr (if (equal arg-types (list (atj-type-acl2 (atj-atype-boolean)))) (jexpr-unary (junop-logcompl) arg-expr) (jexpr-binary (jbinop-eq) arg-expr (atj-gen-symbol nil t nil)))) (src-type (atj-type-list-to-type src-types)) (dst-type (atj-type-list-to-type dst-types))) (mv (jblock-fix arg-block) (atj-adapt-expr-to-type expr src-type dst-type t)))))
Theorem:
(defthm jblockp-of-atj-gen-shallow-not-call.block (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-not-call arg-block arg-expr arg-term src-types dst-types))) (jblockp block)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-gen-shallow-not-call.expr (b* (((mv common-lisp::?block ?expr) (atj-gen-shallow-not-call arg-block arg-expr arg-term src-types dst-types))) (jexprp expr)) :rule-classes :rewrite)