		Search-engine friendly clone of the ACL2 documentation.

Types

Type-integer-promote

Perform integer promotions on an arithmetic type [C17:6.3.1.1/2].

Signature
(type-integer-promote type ienv) → new-type
Arguments: type — Guard (typep type).; ienv — Guard (ienvp ienv).
Returns: new-type — Type (typep new-type).

This only changes integer types of rank lower than int; the other types are left unchanged. We need the implementation environment because the new type may depend on the relative range of the initial type and signed int. The range of _Bool always fits within signed int, and so do signed char and signed short. For unsigned char and unsigned short, as well as for char (which may have the same range as unsigned char), we need to compare the maxima, and return either signed int or unsigned int as the promoted type.

The rank of an enumerated type (which is an integer type) is implementation-defined, and could even vary based on the program, as mentioned in footnote 131 of [C17:6.7.2.2/4]. Thus, for now we promote the (one) enumerated type to unknown.

Definitions and Theorems

Function: type-integer-promote

(defun type-integer-promote (type ienv)
  (declare (xargs :guard (and (typep type) (ienvp ienv))))
  (declare (xargs :guard (type-arithmeticp type)))
  (type-case type :bool (type-sint)
             :char
             (if (<= (ienv->char-max ienv)
                     (ienv->sint-max ienv))
                 (type-sint)
               (type-uint))
             :schar (type-sint)
             :uchar
             (if (<= (ienv->uchar-max ienv)
                     (ienv->sint-max ienv))
                 (type-sint)
               (type-uint))
             :sshort (type-sint)
             :ushort
             (if (<= (ienv->ushort-max ienv)
                     (ienv->sint-max ienv))
                 (type-sint)
               (type-uint))
             :enum (type-unknown)
             :otherwise (type-fix type)))

Theorem: typep-of-type-integer-promote

(defthm typep-of-type-integer-promote
  (b* ((new-type (type-integer-promote type ienv)))
    (typep new-type))
  :rule-classes :rewrite)

Theorem: type-integer-promotedp-of-type-integer-promote

(defthm type-integer-promotedp-of-type-integer-promote
  (b* ((new-type (type-integer-promote type ienv)))
    (type-integer-promotedp new-type))
  :rule-classes :rewrite)

Theorem: type-count-of-type-integer-promote

(defthm type-count-of-type-integer-promote
  (equal (type-count (type-integer-promote type ienv))
         (type-count type)))

Theorem: type-integer-promote-of-type-fix-type

(defthm type-integer-promote-of-type-fix-type
  (equal (type-integer-promote (type-fix type)
                               ienv)
         (type-integer-promote type ienv)))

Theorem: type-integer-promote-type-equiv-congruence-on-type

(defthm type-integer-promote-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (type-integer-promote type ienv)
                  (type-integer-promote type-equiv ienv)))
  :rule-classes :congruence)

Theorem: type-integer-promote-of-ienv-fix-ienv

(defthm type-integer-promote-of-ienv-fix-ienv
  (equal (type-integer-promote type (ienv-fix ienv))
         (type-integer-promote type ienv)))

Theorem: type-integer-promote-ienv-equiv-congruence-on-ienv

(defthm type-integer-promote-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (type-integer-promote type ienv)
                  (type-integer-promote type ienv-equiv)))
  :rule-classes :congruence)