		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-string-nonfixnum-index

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

Definitions and Theorems

Function: jenkins-acc-string-nonfixnum-index

(defun jenkins-acc-string-nonfixnum-index (str i len acc)
  (declare (type string str)
           (type unsigned-byte i)
           (type unsigned-byte len)
           (type (unsigned-byte 32) acc)
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard (and (<= i len)
                              (equal len (length str)))))
  (let ((i (mbe :logic (nfix i) :exec i))
        (len (mbe :logic (nfix len) :exec len)))
    (declare (type unsigned-byte i)
             (type unsigned-byte len))
    (if (and (mbt (<= i len)) (< i len))
        (jenkins-acc-string-nonfixnum-index
             str (the unsigned-byte (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-nonfixnum-index

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