		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-common

Atc-check-binop

Check if a term may represent a strict pure binary expression.

Signature
(atc-check-binop term) → (mv erp yes/no fn arg1 arg2 in-type1 in-type2 out-type op)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; arg1 — Type (pseudo-termp arg1).; arg2 — Type (pseudo-termp arg2).; in-type1 — Type (typep in-type1).; in-type2 — Type (typep in-type2).; out-type — Type (typep out-type).; op — Type (binopp op).

If the term is a call of one of the ACL2 functions that represent C strict pure binary operators, we return the function, the argument terms, the inputs and output types, and the C operator.

If the term does not have that form, we return an indication of failure. The term may represent some other kind of C expression.

Definitions and Theorems

Function: atc-check-binop

(defun atc-check-binop (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'atc-check-binop))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil nil nil (irr-type)
     (irr-type)
     (irr-type)
     (irr-binop))
    ((acl2::fun (no))
     (retok nil nil nil nil (irr-type)
            (irr-type)
            (irr-type)
            (irr-binop)))
    ((mv okp fn args)
     (fty-check-fn-call term))
    ((unless okp) (no))
    ((mv okp op fixtype1 fixtype2)
     (atc-check-symbol-3part fn))
    (in-type1 (fixtype-to-integer-type fixtype1))
    (in-type2 (fixtype-to-integer-type fixtype2))
    ((unless
      (and okp
           (member-eq op
                      '(add sub mul div rem shl shr
                            lt le gt ge eq ne bitand bitxor bitior))
           in-type1 in-type2))
     (no))
    ((unless (equal (symbol-package-name fn) "C"))
     (reterr
      (msg
       "Invalid function ~x0 encountered: ~
                      it has the form of an integer binary operation function, ~
                      but it is not in the \"C\" package."
       fn)))
    ((unless (list-lenp 2 args))
     (reterr
          (raise "Internal error: ~x0 not applied to 2 arguments."
                 term)))
    (arg1 (first args))
    (arg2 (second args))
    ((mv out-type binop)
     (case op
       (add (mv (uaconvert-types in-type1 in-type2)
                (binop-add)))
       (sub (mv (uaconvert-types in-type1 in-type2)
                (binop-sub)))
       (mul (mv (uaconvert-types in-type1 in-type2)
                (binop-mul)))
       (div (mv (uaconvert-types in-type1 in-type2)
                (binop-div)))
       (rem (mv (uaconvert-types in-type1 in-type2)
                (binop-rem)))
       (shl (mv (promote-type in-type1)
                (binop-shl)))
       (shr (mv (promote-type in-type1)
                (binop-shr)))
       (lt (mv (type-sint) (binop-lt)))
       (le (mv (type-sint) (binop-le)))
       (gt (mv (type-sint) (binop-gt)))
       (ge (mv (type-sint) (binop-ge)))
       (eq (mv (type-sint) (binop-eq)))
       (ne (mv (type-sint) (binop-ne)))
       (bitand (mv (uaconvert-types in-type1 in-type2)
                   (binop-bitand)))
       (bitxor (mv (uaconvert-types in-type1 in-type2)
                   (binop-bitxor)))
       (bitior (mv (uaconvert-types in-type1 in-type2)
                   (binop-bitior)))
       (t (prog2$ (impossible)
                  (mv (irr-type) (irr-binop)))))))
   (retok t fn arg1 arg2
          in-type1 in-type2 out-type binop))))

Theorem: booleanp-of-atc-check-binop.yes/no

(defthm booleanp-of-atc-check-binop.yes/no
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-binop.fn

(defthm symbolp-of-atc-check-binop.fn
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-binop.arg1

(defthm pseudo-termp-of-atc-check-binop.arg1
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (pseudo-termp arg1))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-binop.arg2

(defthm pseudo-termp-of-atc-check-binop.arg2
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (pseudo-termp arg2))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-binop.in-type1

(defthm typep-of-atc-check-binop.in-type1
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (typep in-type1))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-binop.in-type2

(defthm typep-of-atc-check-binop.in-type2
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (typep in-type2))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-binop.out-type

(defthm typep-of-atc-check-binop.out-type
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (typep out-type))
  :rule-classes :rewrite)

Theorem: binopp-of-atc-check-binop.op

(defthm binopp-of-atc-check-binop.op
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (binopp op))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-binop-arg1

(defthm pseudo-term-count-of-atc-check-binop-arg1
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (implies yes/no
             (< (pseudo-term-count arg1)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-binop-arg2

(defthm pseudo-term-count-of-atc-check-binop-arg2
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (implies yes/no
             (< (pseudo-term-count arg2)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: type-nonchar-integerp-of-atc-check-binop-in-type1

(defthm type-nonchar-integerp-of-atc-check-binop-in-type1
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (implies yes/no
             (type-nonchar-integerp in-type1))))

Theorem: type-nonchar-integerp-of-atc-check-binop-in-type2

(defthm type-nonchar-integerp-of-atc-check-binop-in-type2
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (implies yes/no
             (type-nonchar-integerp in-type2))))

Theorem: type-nonchar-integerp-of-atc-check-binop-out-type

(defthm type-nonchar-integerp-of-atc-check-binop-out-type
  (b* (((mv acl2::?erp ?yes/no ?fn ?arg1
            ?arg2 ?in-type1 ?in-type2 ?out-type ?op)
        (atc-check-binop term)))
    (implies yes/no
             (type-nonchar-integerp out-type))))