		Search-engine friendly clone of the ACL2 documentation.

Stv-doc

Stv-to-xml

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

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

Definitions and Theorems

Function: stv-to-xml

(defun stv-to-xml (stv cstv labels)
 (declare (xargs :guard (and (stvdata-p stv)
                             (compiled-stv-p cstv)
                             (symbol-listp labels))))
 (let ((__function__ 'stv-to-xml))
  (declare (ignorable __function__))
  (b*
   ((stv (stv-widen stv))
    ((stvdata stv) stv)
    (ex-ins (compiled-stv->expanded-ins cstv))
    ((unless (true-list-listp ex-ins))
     (raise "Expanded inputs aren't a true-list-listp?"))
    (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.inputs ex-ins acc))
    (acc (str::revappend-chars "</stv_inputs>" acc))
    (acc (cons #\Newline acc))
    (acc (str::revappend-chars "<stv_outputs>" acc))
    (acc (cons #\Newline acc))
    (acc (stv-lines-to-xml stv.outputs 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.internals nil acc))
    (acc (str::revappend-chars "</stv_internals>" acc))
    (acc (cons #\Newline acc))
    (acc (str::revappend-chars "<stv_overrides>" acc))
    (acc (cons #\Newline acc))
    (acc (stv-lines-to-xml stv.overrides nil acc))
    (acc (str::revappend-chars "</stv_overrides>" acc))
    (acc (cons #\Newline acc))
    (acc (str::revappend-chars "</stv>" acc)))
   (str::rchars-to-string acc))))

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

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