		Search-engine friendly clone of the ACL2 documentation.

Upcase-string

Convert a string to upper case.

Signature
(upcase-string x) → *

(upcase-string x) converts a string to upper case, effectively by transforming each of its characters with upcase-char.

ACL2 has a built-in alternative to this function, common-lisp::string-upcase, but it is irritating to use because it has standard-char-p guards. In contrast, upcase-string works on strings with arbitrary characters.

We try to make this fast. For better performance, we avoid consing and simply return x unchanged when it has no characters that need to be converted. Of course, deciding whether some conversion is necessary will marginally slow this function down when some conversion is necessary, but we think the gain of not consing outweighs this. At any rate, this optimization does not affect the logical definition.

Despite trying to make this fast, the builtin string-upcase can really outperform us since it doesn't have to build the intermediate list, etc. It's really a shame that string-upcase has such a terrible guard. Well, at least we're better when no work needs to be done:

(time (loop for i fixnum from 1 to 1000000 do
        (str::upcase-string "Hello, World!")))  ;; 1.2 seconds, 336 MB
(time (loop for i fixnum from 1 to 1000000 do
        (string-upcase "Hello, World!")))       ;; .26 seconds, 64 MB

(time (loop for i fixnum from 1 to 1000000 do
        (str::upcase-string "HELLO, WORLD!")))  ;; .15 seconds, 0 MB
(time (loop for i fixnum from 1 to 1000000 do
        (string-upcase "HELLO, WORLD!")))       ;; .23 seconds, 64 MB

Definitions and Theorems

Function: upcase-string

(defun upcase-string (x)
  (declare (type string x))
  (let ((acl2::__function__ 'upcase-string))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (implode (upcase-charlist (explode x)))
         :exec
         (let ((xl (length x)))
           (if (not (string-has-some-down-alpha-p x 0 xl))
               x
             (rchars-to-string (upcase-string-aux x 0 xl nil)))))))

Theorem: istreqv-implies-equal-upcase-string-1

(defthm istreqv-implies-equal-upcase-string-1
  (implies (istreqv x x-equiv)
           (equal (upcase-string x)
                  (upcase-string x-equiv)))
  :rule-classes (:congruence))

Theorem: len-of-upcase-string

(defthm len-of-upcase-string
  (equal (len (explode (upcase-string x)))
         (len (explode x))))

Theorem: length-of-upcase-string

(defthm length-of-upcase-string
  (equal (length (upcase-string x))
         (len (explode x))))

Theorem: equal-of-empty-string-with-upcase-string

(defthm equal-of-empty-string-with-upcase-string
  (equal (equal "" (upcase-string x))
         (atom (explode x))))

Theorem: string-upcase-is-upcase-string

(defthm string-upcase-is-upcase-string
  (implies (standard-char-listp (explode x))
           (equal (common-lisp::string-upcase x)
                  (upcase-string (double-rewrite x)))))

Subtopics

Upcase-string-aux
String-has-some-down-alpha-p