symbol-print-full-escapes

other

(in-package "ACL2")

bar-escape-charsfunction

(defun bar-escape-chars
  (x)
  (declare (xargs :guard (character-listp x)))
  (cond ((atom x) nil)
    ((eql (car x) #\|) (list* #\\ #\| (bar-escape-chars (cdr x))))
    ((eql (car x) #\\) (list* #\\ #\\ (bar-escape-chars (cdr x))))
    (t (cons (car x) (bar-escape-chars (cdr x))))))

local

(local (defthm character-listp-of-bar-escape-chars
    (implies (character-listp x)
      (character-listp (bar-escape-chars x)))))

bar-escape-stringfunction

(defun bar-escape-string
  (x)
  (declare (type string x))
  (if (or (position #\| x) (position #\\ x))
    (coerce (bar-escape-chars (coerce x 'list)) 'string)
    x))

bar-escape-namefunction

(defun bar-escape-name
  (x)
  (declare (type string x))
  (concatenate 'string "|" (bar-escape-string x) "|"))

full-escape-symbolfunction

(defun full-escape-symbol
  (x)
  (declare (type symbol x))
  (concatenate 'string
    (bar-escape-name (symbol-package-name x))
    "::"
    (bar-escape-name (symbol-name x))))