		Search-engine friendly clone of the ACL2 documentation.

Svtv-doc

Svtv-to-xml

Top-level routine to generate a nice XML description of an STV.

Signature
(svtv-to-xml svtv labels) → encoding
Arguments: svtv — Guard (svtv-p svtv).; labels — Guard (symbol-listp labels).
Returns: encoding — Type (or (stringp encoding) (not encoding)).

Definitions and Theorems

Function: svtv-to-xml

(defun svtv-to-xml (svtv labels)
 (declare (xargs :guard (and (svtv-p svtv)
                             (symbol-listp labels))))
 (let ((__function__ 'svtv-to-xml))
  (declare (ignorable __function__))
  (b*
   (((svtv svtv))
    (acc nil)
    (acc (str::revappend-chars "<stv>" acc))
    (acc
      (if labels
       (b*
         ((acc (str::revappend-chars "<stv_labels>" acc))
          (acc (str::revappend-chars "<stv_label></stv_label>" acc))
          (acc (stv-labels-to-xml labels acc))
          (acc (str::revappend-chars "</stv_labels>" acc)))
         acc)
       acc))
    (acc (cons #\Newline acc))
    (acc (str::revappend-chars "<stv_inputs>" acc))
    (acc (cons #\Newline acc))
    (acc (stv-lines-to-xml
              (stv-repeat-last-entries svtv.orig-ins svtv.nphases)
              svtv.expanded-ins acc))
    (acc (str::revappend-chars "</stv_inputs>" acc))
    (acc (cons #\Newline acc))
    (acc (str::revappend-chars "<stv_overrides>" acc))
    (acc (cons #\Newline acc))
    (acc
     (stv-lines-to-xml
          (stv-repeat-last-entries svtv.orig-overrides svtv.nphases)
          svtv.expanded-overrides acc))
    (acc (str::revappend-chars "</stv_overrides>" acc))
    (acc (str::revappend-chars "<stv_outputs>" acc))
    (acc (cons #\Newline acc))
    (acc (stv-lines-to-xml
              (stv-repeat-last-entries svtv.orig-outs svtv.nphases)
              nil acc))
    (acc (str::revappend-chars "</stv_outputs>" acc))
    (acc (cons #\Newline acc))
    (acc (str::revappend-chars "<stv_internals>" acc))
    (acc (cons #\Newline acc))
    (acc
     (stv-lines-to-xml
          (stv-repeat-last-entries svtv.orig-internals svtv.nphases)
          nil acc))
    (acc (str::revappend-chars "</stv_internals>" acc))
    (acc (cons #\Newline acc))
    (acc (cons #\Newline acc))
    (acc (str::revappend-chars "</stv>" acc)))
   (rchars-to-string acc))))

Theorem: return-type-of-svtv-to-xml

(defthm return-type-of-svtv-to-xml
  (b* ((encoding (svtv-to-xml svtv labels)))
    (or (stringp encoding) (not encoding)))
  :rule-classes :type-prescription)