Trim whitespace from a string, but preserving space that might be syntactically significant.
Generally whitespace is not supposed to be syntactically significant, but there is one case where it is: escaped identifiers that are written beginning with a backslash and ending with a space, tab, or newline. We need to leave a space after any such escaped identifier. Conversely, though, it is important NOT to include a space in something like prefix below:
`define MY_MACRO(suffix, prefix) logic ``prefix``_foo_``suffix``; module test (); `MY_MACRO(aaa, bbb) endmodule // test
As a hack to accommodate both these particularities, we'll always trim whitespace from the beginning of the string and also trim whitespace from the end unless either (1) there is no whitespace at the end, or (2) there is a backslash character somewhere within the continuous block of non-whitespace characters immediately preceding the final block of whitespace.
Function:
(defun vl-trim-for-preproc (x) (declare (xargs :guard (stringp x))) (let ((__function__ 'vl-trim-for-preproc)) (declare (ignorable __function__)) (b* ((x (mbe :logic (str-fix x) :exec x)) (len (length x)) (first-non-whitespace-idx (scan-for-non-whitespace 0 x)) (last-non-whitespace-idx (scan-backward-for-non-whitespace len x)) ((when (eql last-non-whitespace-idx len)) "") ((when (eql last-non-whitespace-idx (1- len))) (b* (((when (eql first-non-whitespace-idx 0)) x)) (subseq x first-non-whitespace-idx nil))) (last-non-trailing-whitespace-idx (scan-backward-for-whitespace last-non-whitespace-idx x)) (search-start (if (eql last-non-trailing-whitespace-idx len) 0 (1+ last-non-trailing-whitespace-idx))) (has-backslash (str::strpos-fast "\\" x search-start 1 len)) ((when has-backslash) (subseq x first-non-whitespace-idx (+ 2 last-non-whitespace-idx)))) (subseq x first-non-whitespace-idx (+ 1 last-non-whitespace-idx)))))
Theorem:
(defthm stringp-of-vl-trim-for-preproc (b* ((trim (vl-trim-for-preproc x))) (stringp trim)) :rule-classes :type-prescription)