• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
        • Revappend-chars
        • Join
        • Append-chars
        • Cat
        • Rchars-to-string
        • Prefix-strings
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Concatenation

Revappend-chars

Append a string's characters onto a list, in reverse order.

(revappend-chars x y) takes the characters from the string x, reverses them, and appends the result onto y.

Its logical definition is nothing more than (revappend (explode x) y).

In the execution, we traverse the string x using char to avoid the overhead of coerce-ing it into a character list before performing the revappend. This reduces the overhead from 2n conses to n conses, where n is the length of x.

This function may seem strange at first glance, but it provides a convenient way to efficiently, incrementally build a string out of small parts. For instance, a sequence such as:

(let* ((acc nil)
       (acc (str::revappend-chars "Hello, " acc))
       (acc (str::revappend-chars "World!" acc))
       (acc ...))
   (reverse (implode acc)))

Is essentially the same as:

(let* ((acc "")
       (acc (str::cat acc "Hello, "))
       (acc (str::cat acc "World!"))
       (acc ...))
  acc)

But it is comparably much more efficient because it avoids the creation of the intermediate strings. See the performance discussion in cat for more details. Also see rchars-to-string, which is a potentially more efficient way to do the final reverse/coerce steps.

Definitions and Theorems

Function: revappend-chars-aux

(defun revappend-chars-aux (x n xl y)
  (declare (type string x)
           (type (integer 0 *) n xl)
           (xargs :guard (and (<= n xl) (equal xl (length x)))))
  (if (mbe :logic (zp (- (nfix xl) (nfix n)))
           :exec (eql n xl))
      y
    (revappend-chars-aux x
                         (the (integer 0 *)
                              (+ 1 (the (integer 0 *) (lnfix n))))
                         xl (cons (char x n) y))))

Theorem: revappend-chars-aux-correct

(defthm revappend-chars-aux-correct
  (implies (and (stringp x)
                (natp n)
                (<= n xl)
                (equal xl (length x)))
           (equal (revappend-chars-aux x n xl y)
                  (revappend (nthcdr n (coerce x 'list))
                             y))))

Function: revappend-chars$inline

(defun revappend-chars$inline (x y)
  (declare (type string x))
  (mbe :logic (revappend (coerce x 'list) y)
       :exec (revappend-chars-aux x 0 (length x) y)))

Theorem: character-listp-of-revappend-chars

(defthm character-listp-of-revappend-chars
  (equal (character-listp (revappend-chars x y))
         (character-listp y)))

Theorem: streqv-implies-equal-revappend-chars-1

(defthm streqv-implies-equal-revappend-chars-1
  (implies (streqv x x-equiv)
           (equal (revappend-chars x y)
                  (revappend-chars x-equiv y)))
  :rule-classes (:congruence))

Theorem: istreqv-implies-icharlisteqv-revappend-chars-1

(defthm istreqv-implies-icharlisteqv-revappend-chars-1
  (implies (istreqv x x-equiv)
           (icharlisteqv (revappend-chars x y)
                         (revappend-chars x-equiv y)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-revappend-chars-2

(defthm list-equiv-implies-list-equiv-revappend-chars-2
  (implies (list-equiv y y-equiv)
           (list-equiv (revappend-chars x y)
                       (revappend-chars x y-equiv)))
  :rule-classes (:congruence))

Theorem: charlisteqv-implies-charlisteqv-revappend-chars-2

(defthm charlisteqv-implies-charlisteqv-revappend-chars-2
  (implies (charlisteqv y y-equiv)
           (charlisteqv (revappend-chars x y)
                        (revappend-chars x y-equiv)))
  :rule-classes (:congruence))

Theorem: icharlisteqv-implies-icharlisteqv-revappend-chars-2

(defthm icharlisteqv-implies-icharlisteqv-revappend-chars-2
  (implies (icharlisteqv y y-equiv)
           (icharlisteqv (revappend-chars x y)
                         (revappend-chars x y-equiv)))
  :rule-classes (:congruence))