Convert a string to upper case.
(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,
We try to make this fast. For better performance, we avoid consing and
Despite trying to make this fast, the builtin
(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
(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)))))))
(defthm istreqv-implies-equal-upcase-string-1 (implies (istreqv x x-equiv) (equal (upcase-string x) (upcase-string x-equiv))) :rule-classes (:congruence))
(defthm equal-of-empty-string-with-upcase-string (equal (equal "" (upcase-string x)) (atom (explode x))))
(defthm string-upcase-is-upcase-string (equal (common-lisp::string-upcase x) (upcase-string (double-rewrite x))))