		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Negate-boolean-jexpr

Negates a (boolean) Java expression.

Signature
(negate-boolean-jexpr expr) → new-expr
Arguments: expr — Guard (jexprp expr).
Returns: new-expr — Type (jexprp new-expr).

This accepts and transforms any Java expression. However, if the original expression is not boolean, the transformed expression is malformed (i.e. ill-typed).

If the expression is a boolean literal, we replace it with the other boolean literal. If the expression is a logical negation !..., we remove the !. If the expression is an (in)equality or comparison, we negate the operator. In all other cases, we put ! before the expression, which is always correct and a default strategy. We may extend the special (i.e. non-default) handling, e.g. by distributing the negation over conjunctions and disjunctions, and over the `then' and `else' branches of the ternary condition operator ? ... : ....

Definitions and Theorems

Function: negate-boolean-jexpr

(defun negate-boolean-jexpr (expr)
  (declare (xargs :guard (jexprp expr)))
  (let ((__function__ 'negate-boolean-jexpr))
    (declare (ignorable __function__))
    (b* ((default-result (jexpr-unary (junop-logcompl) expr)))
      (case (jexpr-kind expr)
        (:literal (b* ((literal (jexpr-literal->get expr)))
                    (if (jliteral-case literal :boolean)
                        (if (jliteral-boolean->value literal)
                            (jexpr-literal-false)
                          (jexpr-literal-true))
                      default-result)))
        (:unary (b* ((op (jexpr-unary->op expr))
                     (arg (jexpr-unary->arg expr)))
                  (if (junop-case op :logcompl)
                      arg
                    default-result)))
        (:binary (b* ((op (jexpr-binary->op expr))
                      (left (jexpr-binary->left expr))
                      (right (jexpr-binary->right expr)))
                   (case (jbinop-kind op)
                     (:lt (jexpr-binary (jbinop-ge) left right))
                     (:gt (jexpr-binary (jbinop-le) left right))
                     (:le (jexpr-binary (jbinop-gt) left right))
                     (:ge (jexpr-binary (jbinop-lt) left right))
                     (:eq (jexpr-binary (jbinop-ne) left right))
                     (:ne (jexpr-binary (jbinop-eq) left right))
                     (otherwise default-result))))
        (otherwise default-result)))))

Theorem: jexprp-of-negate-boolean-jexpr

(defthm jexprp-of-negate-boolean-jexpr
  (b* ((new-expr (negate-boolean-jexpr expr)))
    (jexprp new-expr))
  :rule-classes :rewrite)