Replace substrings throughout a string.
(strsubst old new x) replaces each occurrence of
(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
(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)))))
(defthm stringp-of-strsubst (stringp (strsubst old new x)) :rule-classes :type-prescription)