		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Uaconvert-types

Apply the usual arithmetic conversions to two arithmetic types [C17:6.3.1.8].

Signature
(uaconvert-types type1 type2) → type
Arguments: type1 — Guard (typep type1).; type2 — Guard (typep type2).
Returns: type — Type (typep type).

These determine a common type from the two types, which is also the type of the result of a binary operator applied to operands of the two types.

Definitions and Theorems

Function: uaconvert-types

(defun uaconvert-types (type1 type2)
  (declare (xargs :guard (and (typep type1) (typep type2))))
  (declare (xargs :guard (and (type-arithmeticp type1)
                              (type-arithmeticp type2))))
  (b* ((type1 (promote-type type1))
       (type2 (promote-type type2))
       ((acl2::fun (irr-type))
        (ec-call (type-fix :irrelevant))))
    (case (type-kind type1)
      (:sllong (case (type-kind type2)
                 (:sllong (type-sllong))
                 (:slong (type-sllong))
                 (:sint (type-sllong))
                 (:ullong (type-ullong))
                 (:ulong (if (>= (sllong-max) (ulong-max))
                             (type-sllong)
                           (type-ullong)))
                 (:uint (if (>= (sllong-max) (uint-max))
                            (type-sllong)
                          (type-ullong)))
                 (t (prog2$ (impossible) (irr-type)))))
      (:slong (case (type-kind type2)
                (:sllong (type-sllong))
                (:slong (type-slong))
                (:sint (type-slong))
                (:ullong (type-ullong))
                (:ulong (type-ulong))
                (:uint (if (>= (slong-max) (uint-max))
                           (type-slong)
                         (type-ulong)))
                (t (prog2$ (impossible) (irr-type)))))
      (:sint (case (type-kind type2)
               (:sllong (type-sllong))
               (:slong (type-slong))
               (:sint (type-sint))
               (:ullong (type-ullong))
               (:ulong (type-ulong))
               (:uint (type-uint))
               (t (prog2$ (impossible) (irr-type)))))
      (:ullong (case (type-kind type2)
                 (:sllong (type-ullong))
                 (:slong (type-ullong))
                 (:sint (type-ullong))
                 (:ullong (type-ullong))
                 (:ulong (type-ullong))
                 (:uint (type-ullong))
                 (t (prog2$ (impossible) (irr-type)))))
      (:ulong (case (type-kind type2)
                (:sllong (if (>= (sllong-max) (ulong-max))
                             (type-sllong)
                           (type-ullong)))
                (:slong (type-ulong))
                (:sint (type-ulong))
                (:ullong (type-ullong))
                (:ulong (type-ulong))
                (:uint (type-ulong))
                (t (prog2$ (impossible) (irr-type)))))
      (:uint (case (type-kind type2)
               (:sllong (if (>= (sllong-max) (uint-max))
                            (type-sllong)
                          (type-ullong)))
               (:slong (if (>= (slong-max) (uint-max))
                           (type-slong)
                         (type-ulong)))
               (:sint (type-uint))
               (:ullong (type-ullong))
               (:ulong (type-ulong))
               (:uint (type-uint))
               (t (prog2$ (impossible) (irr-type)))))
      (t (prog2$ (impossible) (irr-type))))))

Theorem: typep-of-uaconvert-types

(defthm typep-of-uaconvert-types
  (b* ((type (uaconvert-types type1 type2)))
    (typep type))
  :rule-classes :rewrite)

Theorem: type-arithmeticp-of-uaconvert-types

(defthm type-arithmeticp-of-uaconvert-types
  (equal (type-arithmeticp (uaconvert-types type1 type2))
         (and (type-arithmeticp type1)
              (type-arithmeticp type2))))

Theorem: type-integerp-of-uaconvert-types

(defthm type-integerp-of-uaconvert-types
  (implies (and (type-arithmeticp type1)
                (type-arithmeticp type2))
           (equal (type-integerp (uaconvert-types type1 type2))
                  (and (type-integerp type1)
                       (type-integerp type2)))))

Theorem: type-nonchar-integerp-of-uaconvert-types

(defthm type-nonchar-integerp-of-uaconvert-types
  (implies (and (type-integerp type1)
                (type-integerp type2))
           (b* ((?type (uaconvert-types type1 type2)))
             (type-nonchar-integerp type))))

Theorem: type-kind-of-uaconvert-types-not-schar

(defthm type-kind-of-uaconvert-types-not-schar
  (not (equal (type-kind (uaconvert-types type1 type2))
              :schar)))

Theorem: type-kind-of-uaconvert-types-not-uchar

(defthm type-kind-of-uaconvert-types-not-uchar
  (not (equal (type-kind (uaconvert-types type1 type2))
              :uchar)))

Theorem: type-kind-of-uaconvert-types-not-sshort

(defthm type-kind-of-uaconvert-types-not-sshort
  (not (equal (type-kind (uaconvert-types type1 type2))
              :sshort)))

Theorem: type-kind-of-uaconvert-types-not-ushort

(defthm type-kind-of-uaconvert-types-not-ushort
  (not (equal (type-kind (uaconvert-types type1 type2))
              :ushort)))

Theorem: uaconvert-types-when-same

(defthm uaconvert-types-when-same
  (implies (and (type-arithmeticp type1)
                (type-arithmeticp type2)
                (type-equiv type1 type2))
           (equal (uaconvert-types type1 type2)
                  (promote-type type1))))

Theorem: uaconvert-types-symmetry

(defthm uaconvert-types-symmetry
  (implies (and (type-arithmeticp type1)
                (type-arithmeticp type2))
           (equal (uaconvert-types type1 type2)
                  (uaconvert-types type2 type1))))

Theorem: uaconvert-types-of-type-fix-type1

(defthm uaconvert-types-of-type-fix-type1
  (equal (uaconvert-types (type-fix type1) type2)
         (uaconvert-types type1 type2)))

Theorem: uaconvert-types-type-equiv-congruence-on-type1

(defthm uaconvert-types-type-equiv-congruence-on-type1
  (implies (type-equiv type1 type1-equiv)
           (equal (uaconvert-types type1 type2)
                  (uaconvert-types type1-equiv type2)))
  :rule-classes :congruence)

Theorem: uaconvert-types-of-type-fix-type2

(defthm uaconvert-types-of-type-fix-type2
  (equal (uaconvert-types type1 (type-fix type2))
         (uaconvert-types type1 type2)))

Theorem: uaconvert-types-type-equiv-congruence-on-type2

(defthm uaconvert-types-type-equiv-congruence-on-type2
  (implies (type-equiv type2 type2-equiv)
           (equal (uaconvert-types type1 type2)
                  (uaconvert-types type1 type2-equiv)))
  :rule-classes :congruence)