		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-string-fixnum-index

Signature
(jenkins-acc-string-fixnum-index str i len acc) → acc$
Returns: acc$ — Type (unsigned-byte-p 32 acc$).

Definitions and Theorems

Function: jenkins-acc-string-fixnum-index

(defun jenkins-acc-string-fixnum-index (str i len acc)
  (declare (type string str)
           (type (unsigned-byte 61) i)
           (type (unsigned-byte 61) len)
           (type (unsigned-byte 32) acc)
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard (and (<= i len)
                              (equal len (length str)))))
  (let ((__function__ 'jenkins-acc-string-fixnum-index))
    (declare (ignorable __function__))
    (let ((i (mbe :logic (nfix i) :exec i))
          (len (mbe :logic (nfix len) :exec len)))
      (declare (type (unsigned-byte 61) i)
               (type (unsigned-byte 61) len))
      (if (and (mbt (and (<= i len)
                         (<= len *u-fixnum-max*)))
               (< i len))
          (jenkins-acc-string-fixnum-index
               str (the (unsigned-byte 61) (1+ i))
               len
               (jenkins-acc-character (the character (char str i))
                                      acc))
        (mbe :logic (if (unsigned-byte-p 32 acc) acc 0)
             :exec acc)))))

Theorem: return-type-of-jenkins-acc-string-fixnum-index

(defthm return-type-of-jenkins-acc-string-fixnum-index
  (b* ((acc$ (jenkins-acc-string-fixnum-index str i len acc)))
    (unsigned-byte-p 32 acc$))
  :rule-classes :rewrite)