		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Tree=>string

ACL2 string from the fringe of the ABNF tree.

Signature
(tree=>string tree) → fringe?
Arguments: tree — Guard (treep tree).
Returns: fringe? — Type (acl2::string-resultp fringe?).

For a tree that with no rulename leaves (satisfies tree-terminatedp), this is similar to tree->string. But instead of returning a list of numbers, those numbers are interpreted as Unicode codepoints and converted to UTF-8; then those byte values are converted to characters using code-char and assembled into an ACL2 string.

Another difference is that tree->string can have rulenames as leaves. This function will return a reserrp if the tree has any rulename leaves.

If any number in the fringe is not a valid codepoint, return a reserrp.

Definitions and Theorems

Function: tree=>string

(defun tree=>string (tree)
  (declare (xargs :guard (treep tree)))
  (let ((__function__ 'tree=>string))
    (declare (ignorable __function__))
    (b* ((abnf-string (tree->string tree))
         ((unless (nat-listp abnf-string))
          (reserrf (cons "Nonterminal leaves detected"
                         abnf-string)))
         ((unless (acl2::ustring? abnf-string))
          (reserrf (cons "Not a valid list of unicode codepoints"
                         abnf-string)))
         (utf8-bytes (acl2::ustring=>utf8 abnf-string)))
      (nats=>string utf8-bytes))))

Theorem: string-resultp-of-tree=>string

(defthm string-resultp-of-tree=>string
  (b* ((fringe? (tree=>string tree)))
    (acl2::string-resultp fringe?))
  :rule-classes :rewrite)