		Search-engine friendly clone of the ACL2 documentation.

Constructor-preliminaries

String-escape

Escape certain characters in a string, using backslashes.

We escape each single quote and backquote character that occurs in the string.

This is used in generate-primitive-constructor-for-dir/&&, since some of the macros generated by that macro have names that include the characters escaped by this function. These characters would cause XDOC errors if not escaped.

Definitions and Theorems

Function: chars-escape

(defun chars-escape (chars)
  (declare (xargs :guard (character-listp chars)))
  (cond ((endp chars) nil)
        (t (if (member (car chars) '(#\' #\`))
               (list* #\\ #\' (chars-escape (cdr chars)))
             (cons (car chars)
                   (chars-escape (cdr chars)))))))

Theorem: character-listp-of-chars-escape

(defthm character-listp-of-chars-escape
  (implies (character-listp chars)
           (character-listp (chars-escape chars))))

Function: string-escape

(defun string-escape (string)
  (declare (xargs :guard (stringp string)))
  (let* ((chars (coerce string 'list))
         (chars (chars-escape chars))
         (string (coerce chars 'string)))
    string))

Theorem: stringp-of-string-escape

(defthm stringp-of-string-escape
  (stringp (string-escape string)))