		Search-engine friendly clone of the ACL2 documentation.

Vl-kill-whitespace-and-comments

Prepare a token list for parsing by removing whitespace and comment tokens, and construct a comment map from any comment tokens.

Signature
(vl-kill-whitespace-and-comments tokens) → (mv filtered-tokens comment-map)
Arguments: tokens — Token list to process.
Guard (vl-tokenlist-p tokens).
Returns: filtered-tokens — A copy of tokens with comments and whitespace removed.; comment-map — A comment map generated from the comment tokens.

Definitions and Theorems

Function: vl-kill-whitespace-and-comments

(defun vl-kill-whitespace-and-comments (tokens)
 (declare (xargs :guard (vl-tokenlist-p tokens)))
 (let ((__function__ 'vl-kill-whitespace-and-comments))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b*
    (((when (atom tokens)) (mv nil nil))
     ((mv tokens-rest cmap-rest)
      (vl-kill-whitespace-and-comments (cdr tokens)))
     (type (vl-token->type (car tokens)))
     (new-tokens (if (or (eq type :vl-ws)
                         (eq type :vl-comment))
                     tokens-rest
                   (cons (car tokens) tokens-rest)))
     (new-cmap
       (if
        (eq type :vl-comment)
        (cons (cons (change-vl-location (vl-token->loc (car tokens))
                                        :col 0)
                    (vl-token->string (car tokens)))
              cmap-rest)
        cmap-rest)))
    (mv new-tokens new-cmap))
   :exec
   (b* (((local-stobjs nrev nrev2)
         (mv tokens cmap nrev nrev2))
        ((mv nrev nrev2)
         (vl-kill-whitespace-and-comments-core tokens nrev nrev2))
        ((mv tokens nrev) (nrev-finish nrev))
        ((mv cmap nrev2) (nrev-finish nrev2)))
     (mv tokens cmap nrev nrev2)))))

Theorem: vl-kill-whitespace-and-comments-mvtypes-0

(defthm vl-kill-whitespace-and-comments-mvtypes-0
  (true-listp (mv-nth 0
                      (vl-kill-whitespace-and-comments tokens)))
  :rule-classes :type-prescription)

Theorem: vl-kill-whitespace-and-comments-mvtypes-1

(defthm vl-kill-whitespace-and-comments-mvtypes-1
  (true-listp (mv-nth 1
                      (vl-kill-whitespace-and-comments tokens)))
  :rule-classes :type-prescription)

Theorem: vl-tokenlist-p-of-vl-kill-whitespace-and-comments

(defthm vl-tokenlist-p-of-vl-kill-whitespace-and-comments
  (implies (force (vl-tokenlist-p tokens))
           (vl-tokenlist-p
                (mv-nth 0
                        (vl-kill-whitespace-and-comments tokens)))))

Theorem: vl-commentmap-p-of-vl-kill-whitespace-and-comments

(defthm vl-commentmap-p-of-vl-kill-whitespace-and-comments
  (implies (force (vl-tokenlist-p tokens))
           (vl-commentmap-p
                (mv-nth 1
                        (vl-kill-whitespace-and-comments tokens)))))

Subtopics

Vl-kill-whitespace-and-comments-core