		Search-engine friendly clone of the ACL2 documentation.

Strsubst

Replace substrings throughout a string.

(strsubst old new x) replaces each occurrence of old with new throughout x. Each argument is a string, and a new string is returned. The replacement is done globally and non-recursively.

Examples:

(strsubst "World" "Star" "Hello, World!")
  -->
"Hello, Star!"

(strsubst "oo" "aa" "xoooyoo")
  -->
"xaaoyaa"

ACL2 has a built in substitute function, but it only works on individual characters, whereas strsubst works on substrings.

Definitions and Theorems

Function: strsubst

(defun strsubst (old new x)
  (declare (xargs :guard (and (stringp old)
                              (stringp new)
                              (stringp x))))
  (let ((oldl (mbe :logic (len (explode old))
                   :exec (length old)))
        (xl (mbe :logic (len (explode x))
                 :exec (length x))))
    (if (zp oldl)
        (mbe :logic (str-fix x) :exec x)
      (rchars-to-string (strsubst-aux old new x 0 xl oldl nil)))))

Theorem: stringp-of-strsubst

(defthm stringp-of-strsubst
  (stringp (strsubst old new x))
  :rule-classes :type-prescription)

Subtopics

Strsubst-aux: Fast implementation of strsubst.