		Search-engine friendly clone of the ACL2 documentation.

Trees

Tree-to-string

Turn a XDOC tree into the string it represents.

An XDOC tree is turned into a string as follows. A leaf tree is already a string and is left unchanged. For a non-leaf tree, the subtrees are recursively turned into strings and concatenated; then the resulting string is surrounded by text determined by the root of the non-leaf tree. If the root represents a tree concatenation, no surrounding text is actually added. If the root represents a preprocessor directive, the surrounding text "@(...)" creates the directive. If the root represents an XML tag, surrounding text "<tag ... attribute=\"value\" ...>...</tag>" creates the XML tag; the values of the tag's attributes (if present) are obtained by recursively turning the subtrees in the alist into strings.

As noted here, string concatenation is slow in ACL2 in general. The current implementation of this function uses straighforward string concatenation, but this could be optimized in the future, if concatenating strings turns out to be too slow in the actual usage of these XDOC constructors.

Note that the symbol-name of a keyword tag consists of uppercase letters. We use string-downcase$ to produce lowercase tags and directives. We expect that this function will never throw an error with the tags and directives supported.

Definitions and Theorems

Function: tree-to-string

(defun
 tree-to-string (tree)
 (declare (xargs :guard (treep tree)))
 (cond
     ((atom tree)
      (if (mbt (stringp tree)) tree ""))
     (t (let ((subtrees-string (tree-list-to-string (cdr tree))))
             (mv-let (left-string right-string)
                     (keyword-or-tree-tag-to-strings (car tree))
                     (concatenate 'string
                                  left-string
                                  subtrees-string right-string))))))

Function: tree-list-to-string

(defun tree-list-to-string (trees)
       (declare (xargs :guard (tree-listp trees)))
       (cond ((endp trees) "")
             (t (concatenate 'string
                             (tree-to-string (car trees))
                             (tree-list-to-string (cdr trees))))))

Function: keyword-or-tree-tag-to-strings

(defun
 keyword-or-tree-tag-to-strings
 (keyword/tag)
 (declare (xargs :guard (or (keywordp keyword/tag)
                            (tree-tagp keyword/tag))))
 (cond
  ((eq keyword/tag :&&) (mv "" ""))
  ((member-eq keyword/tag
              '(:|@''| :@{} :|@``| :@$$ :@[]))
   (let* ((left-char (char (symbol-name keyword/tag) 1))
          (right-char (char (symbol-name keyword/tag) 2))
          (left-chars (list #\@ #\( left-char))
          (right-chars (list right-char #\)))
          (left-string (coerce left-chars 'string))
          (right-string (coerce right-chars 'string)))
         (mv left-string right-string)))
  ((atom keyword/tag)
   (let
    ((keyword-chars (coerce (symbol-name keyword/tag)
                            'list)))
    (if (and (consp keyword-chars)
             (eql (car keyword-chars) #\@))
        (let* ((keyword-string (coerce (cdr keyword-chars) 'string))
               (keyword-string (string-downcase$ keyword-string))
               (left-string (concatenate 'string
                                         "@(" keyword-string " "))
               (right-string ")"))
              (mv left-string right-string))
        (prog2$ (er hard? 'tree-to-string
                    "Cannot process XDOC tree with root ~x0."
                    keyword/tag)
                (mv "" "")))))
  (t
   (let*
      ((keyword (car keyword/tag))
       (keyword-chars (coerce (symbol-name keyword) 'list))
       (keyword-string (coerce keyword-chars 'string))
       (keyword-string (string-downcase$ keyword-string))
       (attributes (cdr keyword/tag))
       (attributes-string (keyword-tree-alist-to-string attributes))
       (left-string
            (concatenate 'string
                         "<"
                         keyword-string attributes-string ">"))
       (right-string (concatenate 'string
                                  "</" keyword-string ">")))
      (mv left-string right-string)))))

Function: keyword-tree-alist-to-string

(defun
 keyword-tree-alist-to-string
 (attributes)
 (declare (xargs :guard (keyword-tree-alistp attributes)))
 (cond
   ((endp attributes) "")
   (t (let* ((attribute (car attributes))
             (keyword (car attribute))
             (tree (cdr attribute))
             (keyword-chars (coerce (symbol-name keyword) 'list))
             (keyword-string (coerce keyword-chars 'string))
             (keyword-string (string-downcase$ keyword-string))
             (tree-string (tree-to-string tree))
             (attribute-string
                  (concatenate 'string
                               " "
                               keyword-string "=\"" tree-string "\""))
             (rest-attributes (cdr attributes))
             (rest-attribute-string
                  (keyword-tree-alist-to-string rest-attributes)))
            (concatenate 'string
                         attribute-string
                         rest-attribute-string)))))

Theorem: stringp-of-tree-to-string

(defthm stringp-of-tree-to-string
        (stringp (tree-to-string tree)))

Theorem: stringp-of-tree-list-to-string

(defthm stringp-of-tree-list-to-string
        (stringp (tree-list-to-string trees)))

Theorem: stringp-of-mv-nth-0-keyword-or-tree-tag-to-strings

(defthm
 stringp-of-mv-nth-0-keyword-or-tree-tag-to-strings
 (implies
   (or (keywordp keyword/tag)
       (tree-tagp keyword/tag))
   (stringp (mv-nth 0
                    (keyword-or-tree-tag-to-strings keyword/tag)))))

Theorem: stringp-of-mv-nth-1-keyword-or-tree-tag-to-strings

(defthm
    stringp-of-mv-nth-1-keyword-or-tree-tag-to-strings
    (stringp (mv-nth 1
                     (keyword-or-tree-tag-to-strings keyword/tag))))

Theorem: stringp-of-keyword-tree-alist-to-string

(defthm stringp-of-keyword-tree-alist-to-string
        (stringp (keyword-tree-alist-to-string attributes)))