Join together a token list into a single string, putting a single space between each token.
(vl-tokenlist->string-with-spaces x) → 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.
Function:
(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:
(defthm stringp-of-vl-tokenlist->string-with-spaces (b* ((str (vl-tokenlist->string-with-spaces x))) (stringp str)) :rule-classes :type-prescription)