• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Vl-loadstate
        • Lexer
          • Lex-strings
          • Lex-identifiers
          • Vl-typo-uppercase-p
          • Vl-typo-number-p
          • Vl-typo-lowercase-p
          • Lex-numbers
          • Chartypes
            • Vl-decimal-digit-p
            • Vl-z-digit-p
            • Vl-x-digit-p
            • Vl-underscore-p
            • Vl-underscore-or-octal-digit-p
            • Vl-underscore-or-hex-digit-p
            • Vl-underscore-or-decimal-digit-p
            • Vl-underscore-or-binary-digit-p
            • Vl-simple-id-tail-p
            • Vl-simple-id-head-p
            • Vl-octal-digit-p
            • Vl-non-zero-decimal-digit-p
            • Vl-hex-digit-p
            • Vl-binary-digit-p
            • Whitespace
              • Vl-printable-not-whitespace-p
                • Printable-not-whitespace-not-whitespace
              • Vl-whitespace-p
              • Vl-printable-not-whitespace-list-p
              • Vl-whitespace-list-p
              • Whitespace-mask
            • Vl-underscore-or-octal-digit-list-p
            • Vl-underscore-or-hex-digit-list-p
            • Vl-underscore-or-decimal-digit-list-p
            • Vl-underscore-or-binary-digit-list-p
            • Vl-non-zero-decimal-digit-list-p
            • Vl-simple-id-tail-list-p
            • Vl-simple-id-head-list-p
            • Vl-decimal-digit-list-p
            • Vl-binary-digit-list-p
            • Vl-z-digit-list-p
            • Vl-x-digit-list-p
            • Vl-underscore-list-p
            • Vl-octal-digit-list-p
            • Vl-hex-digit-list-p
          • Vl-lex
          • Defchar
          • Tokens
          • Lex-keywords
          • Lexstate
          • Make-test-tokens
          • Lexer-utils
          • Lex-comments
          • Vl-typo-uppercase-list-p
          • Vl-typo-lowercase-list-p
          • Vl-typo-number-list-p
        • Parser
        • Vl-load-merge-descriptions
        • Vl-find-basename/extension
        • Vl-load-file
        • Vl-loadresult
        • Scope-of-defines
        • Vl-find-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-read-file
        • Vl-includeskips-report-gather
        • Vl-load-main
        • Extended-characters
        • Vl-load
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-preprocess-debug
        • Vl-write-preprocessor-debug-file
        • Vl-read-file-report-gather
        • Vl-load-descriptions
        • Vl-load-files
        • Translate-off
        • Vl-load-read-file-hook
        • Vl-read-file-report
        • Vl-loadstate-pad
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-loadstate->warnings
        • Vl-iskips-report
        • Vl-descriptionlist
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Whitespace
• Lex-identifiers

Vl-printable-not-whitespace-p

Match any printable non-whitespace character.

These characters are of interest in escaped identifiers. We don't have to explicitly check for whitespace, because that's ruled out by the character code range.

Definitions and Theorems

Function: vl-printable-not-whitespace-p$inline

(defun vl-printable-not-whitespace-p$inline (x)
  (declare (type character x))
  (and (mbt (characterp x))
       (b* (((the (unsigned-byte 8) code)
             (char-code x)))
         (and (<= 33 code) (<= code 126)))))

Function: vl-printable-not-whitespace-echar-p$inline

(defun vl-printable-not-whitespace-echar-p$inline (x)
  (declare (xargs :guard (vl-echar-p x)))
  (vl-printable-not-whitespace-p (vl-echar->char x)))

Function: vl-printable-not-whitespace-list-p

(defun vl-printable-not-whitespace-list-p (x)
  (declare (xargs :guard (character-listp x)))
  (let ((__function__ 'vl-printable-not-whitespace-list-p))
    (declare (ignorable __function__))
    (if (consp x)
        (and (vl-printable-not-whitespace-p (car x))
             (vl-printable-not-whitespace-list-p (cdr x)))
      t)))

Theorem: vl-printable-not-whitespace-list-p-of-cons

(defthm vl-printable-not-whitespace-list-p-of-cons
  (equal (vl-printable-not-whitespace-list-p (cons acl2::a acl2::x))
         (and (vl-printable-not-whitespace-p acl2::a)
              (vl-printable-not-whitespace-list-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-cdr-when-vl-printable-not-whitespace-list-p

(defthm
 vl-printable-not-whitespace-list-p-of-cdr-when-vl-printable-not-whitespace-list-p
 (implies
      (vl-printable-not-whitespace-list-p (double-rewrite acl2::x))
      (vl-printable-not-whitespace-list-p (cdr acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-when-not-consp

(defthm vl-printable-not-whitespace-list-p-when-not-consp
  (implies (not (consp acl2::x))
           (vl-printable-not-whitespace-list-p acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-p-of-car-when-vl-printable-not-whitespace-list-p

(defthm
 vl-printable-not-whitespace-p-of-car-when-vl-printable-not-whitespace-list-p
 (implies (vl-printable-not-whitespace-list-p acl2::x)
          (iff (vl-printable-not-whitespace-p (car acl2::x))
               (or (consp acl2::x)
                   (vl-printable-not-whitespace-p nil))))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-append

(defthm vl-printable-not-whitespace-list-p-of-append
  (equal
       (vl-printable-not-whitespace-list-p (append acl2::a acl2::b))
       (and (vl-printable-not-whitespace-list-p acl2::a)
            (vl-printable-not-whitespace-list-p acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-list-fix

(defthm vl-printable-not-whitespace-list-p-of-list-fix
  (equal (vl-printable-not-whitespace-list-p (list-fix acl2::x))
         (vl-printable-not-whitespace-list-p acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-sfix

(defthm vl-printable-not-whitespace-list-p-of-sfix
  (iff (vl-printable-not-whitespace-list-p (sfix acl2::x))
       (or (vl-printable-not-whitespace-list-p acl2::x)
           (not (setp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-insert

(defthm vl-printable-not-whitespace-list-p-of-insert
  (iff (vl-printable-not-whitespace-list-p (insert acl2::a acl2::x))
       (and (vl-printable-not-whitespace-list-p (sfix acl2::x))
            (vl-printable-not-whitespace-p acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-delete

(defthm vl-printable-not-whitespace-list-p-of-delete
 (implies
      (vl-printable-not-whitespace-list-p acl2::x)
      (vl-printable-not-whitespace-list-p (delete acl2::k acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-mergesort

(defthm vl-printable-not-whitespace-list-p-of-mergesort
  (iff (vl-printable-not-whitespace-list-p (mergesort acl2::x))
       (vl-printable-not-whitespace-list-p (list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-union

(defthm vl-printable-not-whitespace-list-p-of-union
  (iff (vl-printable-not-whitespace-list-p (union acl2::x acl2::y))
       (and (vl-printable-not-whitespace-list-p (sfix acl2::x))
            (vl-printable-not-whitespace-list-p (sfix acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-intersect-1

(defthm vl-printable-not-whitespace-list-p-of-intersect-1
 (implies
   (vl-printable-not-whitespace-list-p acl2::x)
   (vl-printable-not-whitespace-list-p (intersect acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-intersect-2

(defthm vl-printable-not-whitespace-list-p-of-intersect-2
 (implies
   (vl-printable-not-whitespace-list-p acl2::y)
   (vl-printable-not-whitespace-list-p (intersect acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-difference

(defthm vl-printable-not-whitespace-list-p-of-difference
 (implies
  (vl-printable-not-whitespace-list-p acl2::x)
  (vl-printable-not-whitespace-list-p (difference acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-duplicated-members

(defthm vl-printable-not-whitespace-list-p-of-duplicated-members
 (implies
  (vl-printable-not-whitespace-list-p acl2::x)
  (vl-printable-not-whitespace-list-p (duplicated-members acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-rev

(defthm vl-printable-not-whitespace-list-p-of-rev
  (equal (vl-printable-not-whitespace-list-p (rev acl2::x))
         (vl-printable-not-whitespace-list-p (list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-rcons

(defthm vl-printable-not-whitespace-list-p-of-rcons
 (iff
  (vl-printable-not-whitespace-list-p (acl2::rcons acl2::a acl2::x))
  (and (vl-printable-not-whitespace-p acl2::a)
       (vl-printable-not-whitespace-list-p (list-fix acl2::x))))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-p-when-member-equal-of-vl-printable-not-whitespace-list-p

(defthm
 vl-printable-not-whitespace-p-when-member-equal-of-vl-printable-not-whitespace-list-p
 (and (implies (and (member-equal acl2::a acl2::x)
                    (vl-printable-not-whitespace-list-p acl2::x))
               (vl-printable-not-whitespace-p acl2::a))
      (implies (and (vl-printable-not-whitespace-list-p acl2::x)
                    (member-equal acl2::a acl2::x))
               (vl-printable-not-whitespace-p acl2::a)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-when-subsetp-equal

(defthm vl-printable-not-whitespace-list-p-when-subsetp-equal
  (and (implies (and (subsetp-equal acl2::x acl2::y)
                     (vl-printable-not-whitespace-list-p acl2::y))
                (vl-printable-not-whitespace-list-p acl2::x))
       (implies (and (vl-printable-not-whitespace-list-p acl2::y)
                     (subsetp-equal acl2::x acl2::y))
                (vl-printable-not-whitespace-list-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-set-equiv-congruence

(defthm vl-printable-not-whitespace-list-p-set-equiv-congruence
  (implies (set-equiv acl2::x acl2::y)
           (equal (vl-printable-not-whitespace-list-p acl2::x)
                  (vl-printable-not-whitespace-list-p acl2::y)))
  :rule-classes :congruence)

Theorem: vl-printable-not-whitespace-list-p-of-set-difference-equal

(defthm vl-printable-not-whitespace-list-p-of-set-difference-equal
  (implies (vl-printable-not-whitespace-list-p acl2::x)
           (vl-printable-not-whitespace-list-p
                (set-difference-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-intersection-equal-1

(defthm vl-printable-not-whitespace-list-p-of-intersection-equal-1
  (implies
       (vl-printable-not-whitespace-list-p (double-rewrite acl2::x))
       (vl-printable-not-whitespace-list-p
            (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-intersection-equal-2

(defthm vl-printable-not-whitespace-list-p-of-intersection-equal-2
  (implies
       (vl-printable-not-whitespace-list-p (double-rewrite acl2::y))
       (vl-printable-not-whitespace-list-p
            (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-union-equal

(defthm vl-printable-not-whitespace-list-p-of-union-equal
 (equal
  (vl-printable-not-whitespace-list-p (union-equal acl2::x acl2::y))
  (and
     (vl-printable-not-whitespace-list-p (list-fix acl2::x))
     (vl-printable-not-whitespace-list-p (double-rewrite acl2::y))))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-take

(defthm vl-printable-not-whitespace-list-p-of-take
 (implies
    (vl-printable-not-whitespace-list-p (double-rewrite acl2::x))
    (iff (vl-printable-not-whitespace-list-p (take acl2::n acl2::x))
         (or (vl-printable-not-whitespace-p nil)
             (<= (nfix acl2::n) (len acl2::x)))))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-repeat

(defthm vl-printable-not-whitespace-list-p-of-repeat
  (iff (vl-printable-not-whitespace-list-p (repeat acl2::n acl2::x))
       (or (vl-printable-not-whitespace-p acl2::x)
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-p-of-nth-when-vl-printable-not-whitespace-list-p

(defthm
 vl-printable-not-whitespace-p-of-nth-when-vl-printable-not-whitespace-list-p
 (implies (and (vl-printable-not-whitespace-list-p acl2::x)
               (< (nfix acl2::n) (len acl2::x)))
          (vl-printable-not-whitespace-p (nth acl2::n acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-update-nth

(defthm vl-printable-not-whitespace-list-p-of-update-nth
  (implies
       (vl-printable-not-whitespace-list-p (double-rewrite acl2::x))
       (iff (vl-printable-not-whitespace-list-p
                 (update-nth acl2::n acl2::y acl2::x))
            (and (vl-printable-not-whitespace-p acl2::y)
                 (or (<= (nfix acl2::n) (len acl2::x))
                     (vl-printable-not-whitespace-p nil)))))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-butlast

(defthm vl-printable-not-whitespace-list-p-of-butlast
 (implies
     (vl-printable-not-whitespace-list-p (double-rewrite acl2::x))
     (vl-printable-not-whitespace-list-p (butlast acl2::x acl2::n)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-nthcdr

(defthm vl-printable-not-whitespace-list-p-of-nthcdr
 (implies
      (vl-printable-not-whitespace-list-p (double-rewrite acl2::x))
      (vl-printable-not-whitespace-list-p (nthcdr acl2::n acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-last

(defthm vl-printable-not-whitespace-list-p-of-last
  (implies
       (vl-printable-not-whitespace-list-p (double-rewrite acl2::x))
       (vl-printable-not-whitespace-list-p (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-remove

(defthm vl-printable-not-whitespace-list-p-of-remove
 (implies
      (vl-printable-not-whitespace-list-p acl2::x)
      (vl-printable-not-whitespace-list-p (remove acl2::a acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: vl-printable-not-whitespace-list-p-of-revappend

(defthm vl-printable-not-whitespace-list-p-of-revappend
 (equal
    (vl-printable-not-whitespace-list-p (revappend acl2::x acl2::y))
    (and (vl-printable-not-whitespace-list-p (list-fix acl2::x))
         (vl-printable-not-whitespace-list-p acl2::y)))
 :rule-classes ((:rewrite)))

Function: vl-read-while-printable-not-whitespace-impl

(defun vl-read-while-printable-not-whitespace-impl (echars acc)
 (declare (xargs :guard (vl-echarlist-p echars)))
 (cond
      ((atom echars) (mv acc echars))
      ((vl-printable-not-whitespace-p (vl-echar->char (car echars)))
       (vl-read-while-printable-not-whitespace-impl
            (cdr echars)
            (cons (car echars) acc)))
      (t (mv acc echars))))

Function: vl-read-while-printable-not-whitespace$inline

(defun vl-read-while-printable-not-whitespace$inline (echars)
 (declare (xargs :guard (vl-echarlist-p echars)))
 (mbe
  :logic
  (cond
      ((atom echars) (mv nil echars))
      ((vl-printable-not-whitespace-p (vl-echar->char (car echars)))
       (mv-let (prefix remainder)
               (vl-read-while-printable-not-whitespace (cdr echars))
         (mv (cons (car echars) prefix)
             remainder)))
      (t (mv nil echars)))
  :exec
  (mv-let (prefix-rev remainder)
          (vl-read-while-printable-not-whitespace-impl echars nil)
    (mv (reverse prefix-rev) remainder))))

Theorem: prefix-of-vl-read-while-printable-not-whitespace

(defthm prefix-of-vl-read-while-printable-not-whitespace
 (and
  (true-listp
       (mv-nth 0
               (vl-read-while-printable-not-whitespace echars)))
  (implies
    (force (vl-echarlist-p echars))
    (vl-echarlist-p
         (mv-nth 0
                 (vl-read-while-printable-not-whitespace echars)))))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (true-listp
        (mv-nth 0
                (vl-read-while-printable-not-whitespace echars))))))

Theorem: remainder-of-vl-read-while-printable-not-whitespace

(defthm remainder-of-vl-read-while-printable-not-whitespace
 (and
  (equal
      (true-listp
           (mv-nth 1
                   (vl-read-while-printable-not-whitespace echars)))
      (true-listp echars))
  (implies
    (vl-echarlist-p echars)
    (vl-echarlist-p
         (mv-nth 1
                 (vl-read-while-printable-not-whitespace echars)))))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
    (true-listp echars)
    (true-listp
       (mv-nth 1
               (vl-read-while-printable-not-whitespace echars)))))))

Theorem: prefix-of-vl-read-while-printable-not-whitespace-when-vl-printable-not-whitespace-p

(defthm
 prefix-of-vl-read-while-printable-not-whitespace-when-vl-printable-not-whitespace-p
 (implies
      (vl-printable-not-whitespace-p (vl-echar->char (car echars)))
      (iff (mv-nth 0
                   (vl-read-while-printable-not-whitespace echars))
           (consp echars))))

Theorem: vl-read-while-printable-not-whitespace-sound

(defthm vl-read-while-printable-not-whitespace-sound
 (vl-printable-not-whitespace-list-p
    (vl-echarlist->chars
         (mv-nth 0
                 (vl-read-while-printable-not-whitespace echars)))))

Theorem: vl-read-while-printable-not-whitespace-complete

(defthm vl-read-while-printable-not-whitespace-complete
 (equal
  (vl-printable-not-whitespace-p
   (vl-echar->char
    (car (mv-nth 1
                 (vl-read-while-printable-not-whitespace echars)))))
  (if
   (consp (mv-nth 1
                  (vl-read-while-printable-not-whitespace echars)))
   nil
   (vl-printable-not-whitespace-p (vl-echar->char nil)))))

Theorem: append-of-vl-read-while-printable-not-whitespace

(defthm append-of-vl-read-while-printable-not-whitespace
 (equal
   (append (mv-nth 0
                   (vl-read-while-printable-not-whitespace echars))
           (mv-nth 1
                   (vl-read-while-printable-not-whitespace echars)))
   echars))

Theorem: no-change-loser-of-vl-read-while-printable-not-whitespace

(defthm no-change-loser-of-vl-read-while-printable-not-whitespace
 (implies
     (not (mv-nth 0
                  (vl-read-while-printable-not-whitespace echars)))
     (equal (mv-nth 1
                    (vl-read-while-printable-not-whitespace echars))
            echars)))

Theorem: acl2-count-of-vl-read-while-printable-not-whitespace-weak

(defthm acl2-count-of-vl-read-while-printable-not-whitespace-weak
  (<= (acl2-count
           (mv-nth 1
                   (vl-read-while-printable-not-whitespace echars)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-while-printable-not-whitespace-strong

(defthm acl2-count-of-vl-read-while-printable-not-whitespace-strong
 (implies
   (mv-nth 0
           (vl-read-while-printable-not-whitespace echars))
   (< (acl2-count
           (mv-nth 1
                   (vl-read-while-printable-not-whitespace echars)))
      (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))

Subtopics

Printable-not-whitespace-not-whitespace