• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
        • Ps
        • Verilog-printing
        • Basic-printing
        • Printing-locally
        • Formatted-printing
          • Vl-basic-fmt
            • Vl-basic-fmt-parse-tilde
            • Vl-skip-ws
            • Vl-basic-fmt-aux
            • Vl-fmt-tilde-x
            • Vl-fmt-print-space
            • Vl-fmt-tilde-&
            • Vl-fmt-tilde-s
            • Vl-fmt-print-normal
          • Vl-basic-cw-obj
          • Vl-basic-cw
        • Accessing-printed-output
        • Json-printing
        • Vl-printedlist
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-basic-fmt

Vl-skip-ws

Skip past whitespace in a string.

Signature

(vl-skip-ws x n xl) → new-n

Arguments

x — String we're scanning through.
    Guard (stringp x).

n — Current position in the string.
    Guard (natp n).

xl — Pre-computed length of the string.
    Guard (eql xl (length x)).

Returns

new-n — Index of the first non-whitespace character at or after position n.
    Type (natp new-n).

Definitions and Theorems

Function: vl-skip-ws

(defun vl-skip-ws (x n xl)
  (declare (xargs :guard (and (stringp x)
                              (natp n)
                              (eql xl (length x)))))
  (declare (xargs :guard (<= n xl)))
  (let ((__function__ 'vl-skip-ws))
    (declare (ignorable __function__))
    (b* ((n (lnfix n))
         ((when (mbe :logic (zp (- (nfix xl) (nfix n)))
                     :exec (eql n xl)))
          n)
         ((the character char) (char x n))
         ((when (or (eql char #\Space)
                    (eql char #\Newline)
                    (eql char #\Tab)
                    (eql char #\Page)))
          (vl-skip-ws x (+ 1 n) xl)))
      n)))

Theorem: natp-of-vl-skip-ws

(defthm natp-of-vl-skip-ws
  (b* ((new-n (vl-skip-ws x n xl)))
    (natp new-n))
  :rule-classes :type-prescription)

Theorem: upper-bound-of-vl-skip-ws

(defthm upper-bound-of-vl-skip-ws
  (implies (and (<= (nfix n) xl) (natp xl))
           (<= (vl-skip-ws x n xl) xl))
  :rule-classes ((:rewrite) (:linear)))

Theorem: lower-bound-of-vl-skip-ws

(defthm lower-bound-of-vl-skip-ws
  (implies (natp n)
           (<= n (vl-skip-ws x n xl)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-skip-ws-of-str-fix-x

(defthm vl-skip-ws-of-str-fix-x
  (equal (vl-skip-ws (str-fix x) n xl)
         (vl-skip-ws x n xl)))

Theorem: vl-skip-ws-streqv-congruence-on-x

(defthm vl-skip-ws-streqv-congruence-on-x
  (implies (streqv x x-equiv)
           (equal (vl-skip-ws x n xl)
                  (vl-skip-ws x-equiv n xl)))
  :rule-classes :congruence)

Theorem: vl-skip-ws-of-nfix-n

(defthm vl-skip-ws-of-nfix-n
  (equal (vl-skip-ws x (nfix n) xl)
         (vl-skip-ws x n xl)))

Theorem: vl-skip-ws-nat-equiv-congruence-on-n

(defthm vl-skip-ws-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-skip-ws x n xl)
                  (vl-skip-ws x n-equiv xl)))
  :rule-classes :congruence)