		Search-engine friendly clone of the ACL2 documentation.

Tokens

Vl-tokenlist->string-with-spaces

Join together a token list into a single string, putting a single space between each token.

Signature
(vl-tokenlist->string-with-spaces x) → str
Arguments: x — Guard (vl-tokenlist-p x).
Returns: str — Type (stringp str).

This is occasionally useful for error reporting in the parser, where typically the tokens have already had the comments/whitespace stripped out of them. So, to display them in any sort of sensible way, we need to at least insert spaces between them.

Definitions and Theorems

Function: vl-tokenlist->string-with-spaces

(defun vl-tokenlist->string-with-spaces (x)
  (declare (xargs :guard (vl-tokenlist-p x)))
  (let ((__function__ 'vl-tokenlist->string-with-spaces))
    (declare (ignorable __function__))
    (mbe :logic
         (cond ((atom x) "")
               ((atom (cdr x))
                (vl-token->string (car x)))
               (t (cat (vl-token->string (car x))
                       " "
                       (vl-tokenlist->string-with-spaces (cdr x)))))
         :exec (str::rchars-to-string
                    (vl-tokenlist->string-with-spaces-aux x nil)))))

Theorem: stringp-of-vl-tokenlist->string-with-spaces

(defthm stringp-of-vl-tokenlist->string-with-spaces
  (b* ((str (vl-tokenlist->string-with-spaces x)))
    (stringp str))
  :rule-classes :type-prescription)

Subtopics

Vl-tokenlist->string-with-spaces-aux