		Search-engine friendly clone of the ACL2 documentation.

Stv-doc

Stv-entry-to-xml

Encode a single value from an STV line.

Signature
(stv-entry-to-xml entry expansion acc) → acc
Arguments: entry — The value that the user gave, originally.; expansion — Its expanded out value, a sexpr list.
Returns: acc — Type (character-listp acc), given (character-listp acc).

Definitions and Theorems

Function: stv-entry-to-xml

(defun stv-entry-to-xml (entry expansion acc)
 (declare (xargs :guard t))
 (let ((__function__ 'stv-entry-to-xml))
  (declare (ignorable __function__))
  (cond
   ((natp entry)
    (if (< entry 10)
        (revappend (str::nat-to-dec-chars entry)
                   acc)
     (let* ((pound-x-hex-digits (explode-atom+ entry 16 t))
            (zero-x-hex-digits (cons #\0 (cdr pound-x-hex-digits))))
       (revappend zero-x-hex-digits acc))))
   ((eq entry 'x) (cons #\X acc))
   ((eq entry :ones)
    (str::revappend-chars "<i>ones</i>" acc))
   ((eq entry '~)
    (cond ((equal expansion (list *4vt-sexpr*))
           (cons #\1 acc))
          ((equal expansion (list *4vf-sexpr*))
           (cons #\0 acc))
          (t (progn$ (raise "Expansion of ~ should be 1 or 0.")
                     acc))))
   ((eq entry '_) acc)
   ((symbolp entry)
    (b* ((acc (str::revappend-chars "<b>" acc))
         ((mv ?col acc)
          (vl2014::vl-html-encode-string-aux
               (symbol-name entry)
               0 (length (symbol-name entry))
               0 8 acc))
         (acc (str::revappend-chars "</b>" acc)))
      acc))
   (t (raise "Bad entry in stv line: ~x0." entry)))))

Theorem: character-listp-of-stv-entry-to-xml

(defthm character-listp-of-stv-entry-to-xml
  (implies (character-listp acc)
           (b* ((acc (stv-entry-to-xml entry expansion acc)))
             (character-listp acc)))
  :rule-classes :rewrite)