		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integer-conversions

Def-integer-conversion

Event to generate the conversion between C integer types.

Signature
(def-integer-conversion stype dtype) → event
Arguments: stype — Guard (typep stype).; dtype — Guard (typep dtype).
Returns: event — Type (pseudo-event-formp event).

The conversion turns values of a source type stype into values of the destination type dtype. The two types must be different.

Unless the destination type is signed, and the source type is also signed and always included in the destination type (for every possible choice of integer bit sizes), we generate not only the conversion, but also a function for the guard of the conversion, asserting that the original value is representable in the destination type. Some of the generated guards may be always true for certain choices of integer bit sizes.

Definitions and Theorems

Function: def-integer-conversion

(defun def-integer-conversion (stype dtype)
 (declare (xargs :guard (and (typep stype) (typep dtype))))
 (declare (xargs :guard (and (type-nonchar-integerp stype)
                             (type-nonchar-integerp dtype)
                             (not (equal stype dtype)))))
 (let ((__function__ 'def-integer-conversion))
  (declare (ignorable __function__))
  (b*
   ((stype-string (integer-type-xdoc-string stype))
    (dtype-string (integer-type-xdoc-string dtype))
    (signedp (type-signed-integerp dtype))
    (guardp
     (and
        signedp
        (case (type-kind dtype)
          (:schar t)
          (:sshort (not (eq (type-kind stype) :schar)))
          (:sint (not (member-eq (type-kind stype)
                                 '(:schar :sshort))))
          (:slong (not (member-eq (type-kind stype)
                                  '(:schar :sshort :sint))))
          (:sllong (not (member-eq (type-kind stype)
                                   '(:schar :sshort :sint :slong))))
          (t (impossible)))))
    (<stype> (integer-type-to-fixtype stype))
    (<dtype> (integer-type-to-fixtype dtype))
    (<stype>p (pack <stype> 'p))
    (<dtype>p (pack <dtype> 'p))
    (integer-from-<stype> (pack 'integer-from- <stype>))
    (<dtype>-from-integer (pack <dtype> '-from-integer))
    (<dtype>-integerp (pack <dtype> '-integerp))
    (<dtype>-integerp-alt-def (pack <dtype>-integerp '-alt-def))
    (<dtype>-from-integer-mod (pack <dtype>-from-integer '-mod))
    (<dtype>-from-<stype> (pack <dtype> '-from- <stype>))
    (<dtype>-from-<stype>-okp (pack <dtype>-from-<stype> '-okp)))
   (cons
    'progn
    (append
     (and
      guardp
      (cons
       (cons
        'define
        (cons
         <dtype>-from-<stype>-okp
         (cons
          (cons (cons 'x (cons <stype>p 'nil))
                'nil)
          (cons
           ':returns
           (cons
            '(yes/no booleanp)
            (cons
             ':short
             (cons
                  (str::cat "Check if a conversion from "
                            stype-string
                            " to " dtype-string " is well-defined.")
                  (cons (cons <dtype>-integerp
                              (cons (cons integer-from-<stype> '(x))
                                    'nil))
                        '(:hooks (:fix))))))))))
       'nil))
     (cons
      (cons
       'define
       (cons
        <dtype>-from-<stype>
        (cons
         (cons (cons 'x (cons <stype>p 'nil))
               'nil)
         (append
          (and guardp
               (cons ':guard
                     (cons (cons <dtype>-from-<stype>-okp '(x))
                           'nil)))
          (cons
           ':returns
           (cons
            (cons 'result (cons <dtype>p 'nil))
            (cons
             ':short
             (cons
              (str::cat "Convert from "
                        stype-string " to " dtype-string ".")
              (cons
               (cons (if signedp <dtype>-from-integer
                       <dtype>-from-integer-mod)
                     (cons (cons integer-from-<stype> '(x))
                           'nil))
               (cons
                ':guard-hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons 'enable
                           (cons (if guardp <dtype>-from-<stype>-okp
                                   <dtype>-integerp-alt-def)
                                 'nil))
                     'nil)))
                  'nil)
                 '(:hooks (:fix)))))))))))))
      'nil))))))

Theorem: pseudo-event-formp-of-def-integer-conversion

(defthm pseudo-event-formp-of-def-integer-conversion
  (b* ((event (def-integer-conversion stype dtype)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)