names - ACL2 Book

other

(in-package "XDOC")

other

(include-book "str")

other

(include-book "std/strings/printtree-concat" :dir :system)

other

(program)

funny-char-codefunction

(defun funny-char-code
  (x acc)
  (declare (type character x))
  (b* ((code (char-code x)) (high (ash code -4))
      (low (logand code 15)))
    (list* (digit-to-char high)
      (digit-to-char low)
      acc)))

file-name-mangle-auxfunction

(defun file-name-mangle-aux
  (x n xl acc)
  (declare (type string x))
  (b* (((when (= n xl)) acc) (char (char x n))
      ((when (or (and (char<= #\a char) (char<= char #\z))
           (and (char<= #\A char) (char<= char #\Z))
           (and (char<= #\0 char) (char<= char #\9))
           (eql char #\-)
           (eql char #\.))) (file-name-mangle-aux x
          (+ n 1)
          xl
          (cons char acc)))
      ((when (eql char #\:)) (file-name-mangle-aux x
          (+ n 1)
          xl
          (list* #\_ #\_ acc))))
    (file-name-mangle-aux x
      (+ n 1)
      xl
      (funny-char-code char (cons #\_ acc)))))

file-name-manglefunction

(defun file-name-mangle
  (x acc)
  (declare (type symbol x))
  (b* ((str (cat (symbol-package-name x)
         "::"
         (symbol-name x))))
    (file-name-mangle-aux str
      0
      (length str)
      acc)))

urlfunction

(defun url
  (x)
  (declare (type symbol x))
  (rchars-to-string (file-name-mangle x nil)))

in-package-pfunction

(defun in-package-p
  (sym base-pkg)
  (equal (intern-in-package-of-symbol (symbol-name sym)
      base-pkg)
    sym))

sneaky-downcasefunction

(defun sneaky-downcase
  (x)
  (b* ((down (downcase-string x)))
    (strsubst "acl2" "ACL2" down)))

name-lowfunction

(defun name-low
  (name)
  (declare (type string name))
  (b* ((has-lowercase-p (string-has-some-down-alpha-p name
         0
         (length name))) (name-low (if has-lowercase-p
          name
          (sneaky-downcase name))))
    name-low))

seefunction

(defun see
  (x)
  (declare (type symbol x))
  (b* ((acc nil) (acc (revappend-chars "<see topic="" acc))
      (acc (file-name-mangle x acc))
      (acc (revappend-chars "">" acc))
      (low (name-low (symbol-name x)))
      (acc (simple-html-encode-str low
          0
          (length low)
          acc))
      (acc (revappend-chars "</see>" acc)))
    (rchars-to-string acc)))

other

(encapsulate nil
  (logic)
  (defstub base-pkg-display-override
    (base-pkg)
    t)
  (defun base-pkg-display-override-default
    (base-pkg)
    (declare (xargs :mode :logic :guard t))
    base-pkg)
  (defattach base-pkg-display-override
    base-pkg-display-override-default))

other

(encapsulate nil
  (logic)
  (encapsulate (((rendered-name *) =>
       *
       :formals (name)
       :guard (stringp name)))
    (local (defun rendered-name (x) x)))
  (defun rendered-name-default
    (name)
    (declare (xargs :mode :logic :guard (stringp name)))
    name)
  (defattach rendered-name
    rendered-name-default))

sym-manglefunction

(defun sym-mangle
  (x base-pkg archive-p acc)
  (b* (((when archive-p) (b* ((acc (printtree-rconcat "@(sym |" acc)) (acc (if (in-package-p x base-pkg)
               acc
               (b* ((acc (printtree-rconcat (symbol-package-name x)
                      acc)))
                 (printtree-rconcat "|::|" acc))))
           (acc (printtree-rconcat (symbol-name x) acc)))
         (printtree-rconcat "|)" acc))) (base-pkg (base-pkg-display-override base-pkg))
      (name-low (name-low (rendered-name (symbol-name x))))
      (acc (if (in-package-p x base-pkg)
          acc
          (let ((pkg-low (name-low (symbol-package-name x))))
            (list* #\:
              #\:
              (simple-html-encode-chars (explode pkg-low)
                acc))))))
    (simple-html-encode-chars (explode name-low)
      acc)))

sym-mangle-capfunction

(defun sym-mangle-cap
  (x base-pkg archive-p acc)
  (b* (((when archive-p) (b* ((acc (printtree-rconcat "@(csym |" acc)) (acc (if (in-package-p x base-pkg)
               acc
               (b* ((acc (printtree-rconcat (symbol-package-name x)
                      acc)))
                 (printtree-rconcat "|::|" acc))))
           (acc (printtree-rconcat (symbol-name x) acc)))
         (printtree-rconcat "|)" acc))) (base-pkg (base-pkg-display-override base-pkg))
      (name-low (name-low (rendered-name (symbol-name x))))
      ((when (in-package-p x base-pkg)) (let* ((name-cap (upcase-first name-low)))
          (simple-html-encode-chars (explode name-cap)
            acc)))
      (pkg-low (name-low (symbol-package-name x)))
      (pkg-cap (upcase-first pkg-low))
      (acc (list* #\:
          #\:
          (simple-html-encode-chars (explode pkg-cap)
            acc))))
    (simple-html-encode-chars (explode name-low)
      acc)))