		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Def-integer-range

Event to generate fixtypes, functions, and theorems for ranges of integer types.

Signature
(def-integer-range type) → event
Arguments: type — Guard (typep type).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: def-integer-range

(defun def-integer-range (type)
 (declare (xargs :guard (typep type)))
 (declare (xargs :guard (type-nonchar-integerp type)))
 (let ((__function__ 'def-integer-range))
  (declare (ignorable __function__))
  (b* ((type-string (integer-type-xdoc-string type))
       (minbits (integer-type-minbits type))
       (signedp (type-signed-integerp type))
       (maxbound (if signedp (1- (expt 2 (1- minbits)))
                   (1- (expt 2 minbits))))
       (minbound (if signedp (- (expt 2 (1- minbits)))
                   0))
       (<type>-bits (integer-type-bits-nulfun type))
       (<type> (intern$ (symbol-name (type-kind type))
                        "C"))
       (<type>-integer (pack <type> '-integer))
       (<type>-integerp (pack <type>-integer 'p))
       (<type>-integerp-alt-def (pack <type>-integerp '-alt-def))
       (<type>-integer-list (pack <type>-integer '-list))
       (<type>-integer-listp (pack <type>-integer-list 'p))
       (<type>-max (pack <type> '-max))
       (<type>-min (pack <type> '-min)))
   (cons
    'progn
    (cons
     (cons
      'fty::defbyte
      (cons
       <type>-integer
       (cons
        ':short
        (cons
         (str::cat "Fixtype of ACL2 integers in the range of "
                   type-string ".")
         (cons
          ':size
          (cons
              (cons <type>-bits 'nil)
              (cons ':signed
                    (cons signedp
                          (cons ':pred
                                (cons <type>-integerp 'nil))))))))))
     (cons
      (cons
       'fty::deflist
       (cons
        <type>-integer-list
        (cons
         ':short
         (cons
          (str::cat
               "Fixtype of lists of ACL2 integers in the range of "
               type-string ".")
          (cons
           ':elt-type
           (cons
            <type>-integer
            (cons
             ':true-listp
             (cons
              't
              (cons
               ':elementp-of-nil
               (cons
                   'nil
                   (cons ':pred
                         (cons <type>-integer-listp 'nil))))))))))))
      (cons
       (cons
        'define
        (cons
         <type>-max
         (cons
          'nil
          (cons
           ':returns
           (cons
            (cons <type>-max
                  '(integerp :rule-classes :type-prescription))
            (cons
             ':short
             (cons
              (str::cat "Maximum ACL2 integer value of "
                        type-string ".")
              (cons
               (cons
                '1-
                (cons
                 (cons
                  'expt
                  (cons
                   '2
                   (cons
                      (if signedp
                          (cons '1-
                                (cons (cons <type>-bits 'nil) 'nil))
                        (cons <type>-bits 'nil))
                      'nil)))
                 'nil))
               (cons
                '///
                (cons
                 (cons
                  'in-theory
                  (cons
                       (cons 'disable
                             (cons (cons ':e (cons <type>-max 'nil))
                                   'nil))
                       'nil))
                 (cons
                  (cons
                   'defrule
                   (cons
                    (pack <type>-max '-bound)
                    (cons
                     (cons '>=
                           (cons (cons <type>-max 'nil)
                                 (cons maxbound 'nil)))
                     (cons
                      ':rule-classes
                      (cons
                       ':linear
                       (cons
                        ':enable
                        (cons
                         <type>-max
                         (cons
                          ':use
                          (cons
                           (cons
                            ':instance
                            (cons
                             'acl2::expt-is-weakly-increasing-for-base->-1
                             (cons
                              (cons
                               'm
                               (cons
                                   (if signedp (1- minbits) minbits)
                                   'nil))
                              (cons
                               (cons
                                'n
                                (cons
                                 (if signedp
                                  (cons
                                       '1-
                                       (cons (cons <type>-bits 'nil)
                                             'nil))
                                  (cons <type>-bits 'nil))
                                 'nil))
                               '((x 2))))))
                           'nil)))))))))
                  'nil)))))))))))
       (append
        (and
         signedp
         (cons
          (cons
           'define
           (cons
            <type>-min
            (cons
             'nil
             (cons
              ':returns
              (cons
               (cons <type>-min
                     '(integerp :rule-classes :type-prescription))
               (cons
                ':short
                (cons
                 (str::cat "Minimum ACL2 integer value of "
                           type-string ".")
                 (cons
                  (cons
                   '-
                   (cons
                    (cons
                     'expt
                     (cons
                      '2
                      (cons
                          (cons '1-
                                (cons (cons <type>-bits 'nil) 'nil))
                          'nil)))
                    'nil))
                  (cons
                   '///
                   (cons
                    (cons
                     'in-theory
                     (cons
                       (cons 'disable
                             (cons (cons ':e (cons <type>-min 'nil))
                                   'nil))
                       'nil))
                    (cons
                     (cons
                      'defrule
                      (cons
                       (pack <type>-min '-bound)
                       (cons
                        (cons '<=
                              (cons (cons <type>-min 'nil)
                                    (cons minbound 'nil)))
                        (cons
                         ':rule-classes
                         (cons
                          ':linear
                          (cons
                           ':enable
                           (cons
                            <type>-min
                            (cons
                             ':use
                             (cons
                              (cons
                               ':instance
                               (cons
                                'acl2::expt-is-weakly-increasing-for-base->-1
                                (cons
                                 (cons 'm (cons (1- minbits) 'nil))
                                 (cons
                                  (cons
                                   'n
                                   (cons
                                    (cons
                                       '1-
                                       (cons (cons <type>-bits 'nil)
                                             'nil))
                                    'nil))
                                  '((x 2))))))
                              'nil)))))))))
                     'nil)))))))))))
          'nil))
        (cons
         (cons
          'defruled
          (cons
           <type>-integerp-alt-def
           (cons
            ':short
            (cons
             (str::cat
                "Alternative definition of @(tsee "
                (str::downcase-string (symbol-name <type>-integerp))
                ") as integer range.")
             (cons
              (cons
               'equal
               (cons
                (cons <type>-integerp '(x))
                (cons
                 (cons
                  'and
                  (cons
                   '(integerp x)
                   (cons
                    (cons
                         '<=
                         (cons (if signedp (cons <type>-min 'nil) 0)
                               '(x)))
                    (cons
                     (cons
                          '<=
                          (cons 'x
                                (cons (cons <type>-max 'nil) 'nil)))
                     'nil))))
                 'nil)))
              (cons
               ':enable
               (cons
                  (cons <type>-integerp
                        (cons <type>-max
                              (and signedp (cons <type>-min 'nil))))
                  'nil)))))))
         'nil)))))))))

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

(defthm pseudo-event-formp-of-def-integer-range
  (b* ((event (def-integer-range type)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: def-integer-range-of-type-fix-type

(defthm def-integer-range-of-type-fix-type
  (equal (def-integer-range (type-fix type))
         (def-integer-range type)))

Theorem: def-integer-range-type-equiv-congruence-on-type

(defthm def-integer-range-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (def-integer-range type)
                  (def-integer-range type-equiv)))
  :rule-classes :congruence)