		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)))
 (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)