Recognizer for strings whose characters are all decimal digits.
(dec-digit-string-p x) → bool
Corner case: this accepts the empty string since all of its characters are decimal digits.
Logically this is defined in terms of dec-digit-char-list*p. But in the execution, we use a char-based function that avoids exploding the string. This provides much better performance, e.g., on an AMD FX-8350 with CCL:
;; 0.48 seconds, no garbage (let ((x "1234")) (time$ (loop for i fixnum from 1 to 10000000 do (str::dec-digit-string-p x)))) ;; 0.82 seconds, 640 MB allocated (let ((x "1234")) (time$ (loop for i fixnum from 1 to 10000000 do (str::dec-digit-char-list*p (coerce x 'list)))))
Function:
(defun dec-digit-string-p$inline (x) (declare (type string x)) (let ((acl2::__function__ 'dec-digit-string-p)) (declare (ignorable acl2::__function__)) (mbe :logic (dec-digit-char-list*p (explode x)) :exec (dec-digit-string-p-aux x 0 (length x)))))
Theorem:
(defthm istreqv-implies-equal-dec-digit-string-p-1 (implies (istreqv x x-equiv) (equal (dec-digit-string-p x) (dec-digit-string-p x-equiv))) :rule-classes (:congruence))