		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-binary-pure

Check the application of a pure binary operator to two expressions.

Signature
(check-binary-pure op arg1-expr arg1-etype arg2-expr arg2-etype) → etype
Arguments: op — Guard (binopp op).; arg1-expr — Guard (exprp arg1-expr).; arg1-etype — Guard (expr-typep arg1-etype).; arg2-expr — Guard (exprp arg2-expr).; arg2-etype — Guard (expr-typep arg2-etype).
Returns: etype — Type (expr-type-resultp etype).

We check arg1-etype and arg2-etype against op; arg1-expr and arg2-expr are used just for errors. We return the type of the binary expression; a binary pure expression is never an lvalue.

For multiplication, division, and reminder, the operands must be arithmetic, and the result has the type of the usual arithmetic conversions.

For addition and subtraction, for now we require the operands to be arithmetic, and the result has the type of the usual arithmetic conversions. We do not yet support arithmetic involving pointers.

For left and right shifts, the operands must be integers, and the result has the type of the promoted first operand.

For the relational operators, for now we require the operands to be real, and the result has type int. We do not yet support comparisons between pointers.

For the equality operators, for now we require the operands to be arithmetic, and the result has type int. We do not yet support equalities between pointers.

For the bitwise logical operators, the operands must be integers, and the result has the type of the usual arithmetic conversions.

For the conditional logical operators, the operands must be scalar, and the result is int.

Definitions and Theorems

Function: check-binary-pure

(defun check-binary-pure (op arg1-expr
                             arg1-etype arg2-expr arg2-etype)
 (declare (xargs :guard (and (binopp op)
                             (exprp arg1-expr)
                             (expr-typep arg1-etype)
                             (exprp arg2-expr)
                             (expr-typep arg2-etype))))
 (declare (xargs :guard (binop-purep op)))
 (let ((__function__ 'check-binary-pure))
   (declare (ignorable __function__))
   (b* ((arg1-type (apconvert-type (expr-type->type arg1-etype)))
        (arg2-type (apconvert-type (expr-type->type arg2-etype)))
        ((okf type)
         (case (binop-kind op)
           ((:mul :div :rem :add :sub)
            (if (and (type-arithmeticp arg1-type)
                     (type-arithmeticp arg2-type))
                (uaconvert-types arg1-type arg2-type)
              (reserrf (list :binary-mistype (binop-fix op)
                             (expr-fix arg1-expr)
                             (expr-fix arg2-expr)
                             :required :arithmetic :arithmetic
                             :supplied (type-fix arg1-type)
                             (type-fix arg2-type)))))
           ((:shl :shr)
            (if (and (type-integerp arg1-type)
                     (type-integerp arg2-type))
                (promote-type arg1-type)
              (reserrf (list :binary-mistype (binop-fix op)
                             (expr-fix arg1-expr)
                             (expr-fix arg2-expr)
                             :required :integer
                             :integer :supplied (type-fix arg1-type)
                             (type-fix arg2-type)))))
           ((:lt :gt :le :ge)
            (if (and (type-realp arg1-type)
                     (type-realp arg2-type))
                (type-sint)
              (reserrf (list :binary-mistype (binop-fix op)
                             (expr-fix arg1-expr)
                             (expr-fix arg2-expr)
                             :required :real
                             :real :supplied (type-fix arg1-type)
                             (type-fix arg2-type)))))
           ((:eq :ne)
            (if (and (type-arithmeticp arg1-type)
                     (type-arithmeticp arg2-type))
                (type-sint)
              (reserrf (list :binary-mistype (binop-fix op)
                             (expr-fix arg1-expr)
                             (expr-fix arg2-expr)
                             :required :arithmetic :arithmetic
                             :supplied (type-fix arg1-type)
                             (type-fix arg2-type)))))
           ((:bitand :bitxor :bitior)
            (if (and (type-integerp arg1-type)
                     (type-integerp arg2-type))
                (uaconvert-types arg1-type arg2-type)
              (reserrf (list :binary-mistype (binop-fix op)
                             (expr-fix arg1-expr)
                             (expr-fix arg2-expr)
                             :required :integer
                             :integer :supplied (type-fix arg1-type)
                             (type-fix arg2-type)))))
           ((:logand :logor)
            (if (and (type-scalarp arg1-type)
                     (type-scalarp arg2-type))
                (type-sint)
              (reserrf (list :binary-mistype (binop-fix op)
                             (expr-fix arg1-expr)
                             (expr-fix arg2-expr)
                             :required :integer
                             :integer :supplied (type-fix arg1-type)
                             (type-fix arg2-type)))))
           (t (reserrf (impossible))))))
     (make-expr-type :type type
                     :lvalue nil))))

Theorem: expr-type-resultp-of-check-binary-pure

(defthm expr-type-resultp-of-check-binary-pure
  (b* ((etype (check-binary-pure op arg1-expr
                                 arg1-etype arg2-expr arg2-etype)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-binary-pure-of-binop-fix-op

(defthm check-binary-pure-of-binop-fix-op
  (equal (check-binary-pure (binop-fix op)
                            arg1-expr
                            arg1-etype arg2-expr arg2-etype)
         (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)))

Theorem: check-binary-pure-binop-equiv-congruence-on-op

(defthm check-binary-pure-binop-equiv-congruence-on-op
  (implies
       (binop-equiv op op-equiv)
       (equal (check-binary-pure op arg1-expr
                                 arg1-etype arg2-expr arg2-etype)
              (check-binary-pure op-equiv arg1-expr
                                 arg1-etype arg2-expr arg2-etype)))
  :rule-classes :congruence)

Theorem: check-binary-pure-of-expr-fix-arg1-expr

(defthm check-binary-pure-of-expr-fix-arg1-expr
  (equal (check-binary-pure op (expr-fix arg1-expr)
                            arg1-etype arg2-expr arg2-etype)
         (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)))

Theorem: check-binary-pure-expr-equiv-congruence-on-arg1-expr

(defthm check-binary-pure-expr-equiv-congruence-on-arg1-expr
  (implies
       (expr-equiv arg1-expr arg1-expr-equiv)
       (equal (check-binary-pure op arg1-expr
                                 arg1-etype arg2-expr arg2-etype)
              (check-binary-pure op arg1-expr-equiv
                                 arg1-etype arg2-expr arg2-etype)))
  :rule-classes :congruence)

Theorem: check-binary-pure-of-expr-type-fix-arg1-etype

(defthm check-binary-pure-of-expr-type-fix-arg1-etype
  (equal (check-binary-pure op arg1-expr (expr-type-fix arg1-etype)
                            arg2-expr arg2-etype)
         (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)))

Theorem: check-binary-pure-expr-type-equiv-congruence-on-arg1-etype

(defthm check-binary-pure-expr-type-equiv-congruence-on-arg1-etype
 (implies
  (expr-type-equiv arg1-etype arg1-etype-equiv)
  (equal (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)
         (check-binary-pure op arg1-expr
                            arg1-etype-equiv arg2-expr arg2-etype)))
 :rule-classes :congruence)

Theorem: check-binary-pure-of-expr-fix-arg2-expr

(defthm check-binary-pure-of-expr-fix-arg2-expr
  (equal (check-binary-pure op arg1-expr
                            arg1-etype (expr-fix arg2-expr)
                            arg2-etype)
         (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)))

Theorem: check-binary-pure-expr-equiv-congruence-on-arg2-expr

(defthm check-binary-pure-expr-equiv-congruence-on-arg2-expr
 (implies
  (expr-equiv arg2-expr arg2-expr-equiv)
  (equal (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)
         (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr-equiv arg2-etype)))
 :rule-classes :congruence)

Theorem: check-binary-pure-of-expr-type-fix-arg2-etype

(defthm check-binary-pure-of-expr-type-fix-arg2-etype
  (equal (check-binary-pure op arg1-expr arg1-etype
                            arg2-expr (expr-type-fix arg2-etype))
         (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)))

Theorem: check-binary-pure-expr-type-equiv-congruence-on-arg2-etype

(defthm check-binary-pure-expr-type-equiv-congruence-on-arg2-etype
 (implies
  (expr-type-equiv arg2-etype arg2-etype-equiv)
  (equal (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype)
         (check-binary-pure op arg1-expr
                            arg1-etype arg2-expr arg2-etype-equiv)))
 :rule-classes :congruence)