		Search-engine friendly clone of the ACL2 documentation.

Vl-includeskips

Vl-skip-whitespace/comments

For use in vl-includeskips, just skip past any whitespace and comments.

Signature
(vl-skip-whitespace/comments x) → remainder
Arguments: x — Guard (vl-echarlist-p x).
Returns: remainder — Type (vl-echarlist-p remainder), given the guard.

Definitions and Theorems

Function: vl-skip-whitespace/comments

(defun vl-skip-whitespace/comments (x)
  (declare (xargs :guard (vl-echarlist-p x)))
  (let ((__function__ 'vl-skip-whitespace/comments))
    (declare (ignorable __function__))
    (b* (((when (atom x)) x)
         (char1 (vl-echar->char (first x)))
         ((when (vl-whitespace-p char1))
          (vl-skip-whitespace/comments (cdr x)))
         ((unless (and (eql char1 #\/) (consp (cdr x))))
          x)
         (char2 (vl-echar->char (second x)))
         (rest (cddr x))
         ((when (and (eql char2 #\/)
                     (not (vl-matches-string-p "@VL" rest))
                     (not (vl-matches-string-p "+VL" rest))))
          (b* (((mv ?okp ?prefix remainder)
                (vl-read-through-literal *nls* rest)))
            (vl-skip-whitespace/comments remainder)))
         ((when (and (eql char2 #\*)
                     (not (vl-matches-string-p "@VL" rest))
                     (not (vl-matches-string-p "+VL" rest))))
          (b* (((mv ?okp ?prefix remainder)
                (vl-read-through-literal "*/" rest)))
            (vl-skip-whitespace/comments remainder))))
      x)))

Theorem: vl-echarlist-p-of-vl-skip-whitespace/comments

(defthm vl-echarlist-p-of-vl-skip-whitespace/comments
  (implies (and (vl-echarlist-p x))
           (b* ((remainder (vl-skip-whitespace/comments x)))
             (vl-echarlist-p remainder)))
  :rule-classes :rewrite)