		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-gen-shallow-not-call

Generate a shallowly embedded ACL2 not call.

Signature
(atj-gen-shallow-not-call arg-block arg-expr arg-term src-types dst-types) → (mv block expr)
Arguments: arg-block — Guard (jblockp arg-block).; arg-expr — Guard (jexprp arg-expr).; arg-term — Guard (pseudo-termp arg-term).; src-types — Guard (atj-type-listp src-types).; dst-types — Guard (atj-type-listp dst-types).
Returns: block — Type (jblockp block).; expr — Type (jexprp expr).

This is called only if :guards is t. This is called after translating the argument of not to Java. The resulting block and expression are passed as parameters here, along with the original ACL2 term that is the not argument.

If the argument has type :aboolean, since when :guards is t ACL2 booleans are mapped to Java booleans, we apply Java's logical complement operator. If instead the argument has a different type, which must be an :acl2 type, we convert the resulting expression to a Java boolean by comparing it with nil for equality: the result is a Java boolean, which is appropriate because when :guards is t we map ACL2 booleans to Java booleans.

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.

Definitions and Theorems

Function: atj-gen-shallow-not-call

(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: jblockp-of-atj-gen-shallow-not-call.block

(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: jexprp-of-atj-gen-shallow-not-call.expr

(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)