• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Vl-loadstate
        • Lexer
          • Lex-strings
          • Lex-identifiers
            • Vl-printable-not-whitespace-p
            • Vl-simple-id-tail-p
            • Vl-simple-id-head-p
            • Vl-lex-system-identifier
            • Vl-read-escaped-identifier
            • Vl-lex-simple-identifier-or-keyword
            • Vl-lex-escaped-identifier
            • Vl-printable-not-whitespace-list-p
            • Vl-simple-id-tail-list-p
            • Vl-simple-id-head-list-p
            • Vl-read-simple-identifier
          • Vl-typo-uppercase-p
          • Vl-typo-number-p
          • Vl-typo-lowercase-p
          • Lex-numbers
          • Chartypes
          • 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

• Lex-identifiers
• Chartypes

Vl-simple-id-tail-p

[a-zA-Z0-9_$]

Original definition was:

(or (and (char<= #a x) (char<= x #z))
    (and (char<= #A x) (char<= x #Z))
    (and (char<= #0 x) (char<= x #9))
    (eql x #_)
    (eql x #$))

The new definition is almost twice as fast according to simple tests. We take advantage of ASCII ordering. Uppercase comes before lowercase, and underscore is in between. Numbers are before uppercase, and dollar is before numbers. We first check against upper-case A. If it's greater, it must be a letter or underscore. Otherwise, it must be a number or dollar.

;; (time$
;;  ;; 7.698 seconds with original definition
;;  ;; 4.690 seconds with alt definition
;;  (loop for i fixnum from 1 to 1000000000 do
;;        (vl::vl-simple-id-tail-p #m)
;;        (vl::vl-simple-id-tail-p #M)
;;        (vl::vl-simple-id-tail-p #Space)))

Definitions and Theorems

Function: vl-simple-id-tail-p$inline

(defun vl-simple-id-tail-p$inline (x)
  (declare (type character x))
  (and (mbt (characterp x))
       (let ((code (char-code x)))
         (declare (type (unsigned-byte 8) code))
         (if (<= (explicit-char-code #\A) code)
             (and (<= code (explicit-char-code #\z))
                  (or (<= (explicit-char-code #\a) code)
                      (<= code (explicit-char-code #\Z))
                      (= code (explicit-char-code #\_))))
           (if (<= (explicit-char-code #\0) code)
               (<= code (explicit-char-code #\9))
             (= code (explicit-char-code #\$)))))))

Function: vl-simple-id-tail-echar-p$inline

(defun vl-simple-id-tail-echar-p$inline (x)
  (declare (xargs :guard (vl-echar-p x)))
  (vl-simple-id-tail-p (vl-echar->char x)))

Function: vl-simple-id-tail-list-p

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

Theorem: vl-simple-id-tail-list-p-of-cons

(defthm vl-simple-id-tail-list-p-of-cons
  (equal (vl-simple-id-tail-list-p (cons acl2::a acl2::x))
         (and (vl-simple-id-tail-p acl2::a)
              (vl-simple-id-tail-list-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-cdr-when-vl-simple-id-tail-list-p

(defthm
      vl-simple-id-tail-list-p-of-cdr-when-vl-simple-id-tail-list-p
  (implies (vl-simple-id-tail-list-p (double-rewrite acl2::x))
           (vl-simple-id-tail-list-p (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-when-not-consp

(defthm vl-simple-id-tail-list-p-when-not-consp
  (implies (not (consp acl2::x))
           (vl-simple-id-tail-list-p acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-p-of-car-when-vl-simple-id-tail-list-p

(defthm vl-simple-id-tail-p-of-car-when-vl-simple-id-tail-list-p
  (implies (vl-simple-id-tail-list-p acl2::x)
           (iff (vl-simple-id-tail-p (car acl2::x))
                (or (consp acl2::x)
                    (vl-simple-id-tail-p nil))))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-append

(defthm vl-simple-id-tail-list-p-of-append
  (equal (vl-simple-id-tail-list-p (append acl2::a acl2::b))
         (and (vl-simple-id-tail-list-p acl2::a)
              (vl-simple-id-tail-list-p acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-list-fix

(defthm vl-simple-id-tail-list-p-of-list-fix
  (equal (vl-simple-id-tail-list-p (list-fix acl2::x))
         (vl-simple-id-tail-list-p acl2::x))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-sfix

(defthm vl-simple-id-tail-list-p-of-sfix
  (iff (vl-simple-id-tail-list-p (sfix acl2::x))
       (or (vl-simple-id-tail-list-p acl2::x)
           (not (setp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-insert

(defthm vl-simple-id-tail-list-p-of-insert
  (iff (vl-simple-id-tail-list-p (insert acl2::a acl2::x))
       (and (vl-simple-id-tail-list-p (sfix acl2::x))
            (vl-simple-id-tail-p acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-delete

(defthm vl-simple-id-tail-list-p-of-delete
  (implies (vl-simple-id-tail-list-p acl2::x)
           (vl-simple-id-tail-list-p (delete acl2::k acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-mergesort

(defthm vl-simple-id-tail-list-p-of-mergesort
  (iff (vl-simple-id-tail-list-p (mergesort acl2::x))
       (vl-simple-id-tail-list-p (list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-union

(defthm vl-simple-id-tail-list-p-of-union
  (iff (vl-simple-id-tail-list-p (union acl2::x acl2::y))
       (and (vl-simple-id-tail-list-p (sfix acl2::x))
            (vl-simple-id-tail-list-p (sfix acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-intersect-1

(defthm vl-simple-id-tail-list-p-of-intersect-1
  (implies (vl-simple-id-tail-list-p acl2::x)
           (vl-simple-id-tail-list-p (intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-intersect-2

(defthm vl-simple-id-tail-list-p-of-intersect-2
  (implies (vl-simple-id-tail-list-p acl2::y)
           (vl-simple-id-tail-list-p (intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-difference

(defthm vl-simple-id-tail-list-p-of-difference
  (implies (vl-simple-id-tail-list-p acl2::x)
           (vl-simple-id-tail-list-p (difference acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-duplicated-members

(defthm vl-simple-id-tail-list-p-of-duplicated-members
  (implies (vl-simple-id-tail-list-p acl2::x)
           (vl-simple-id-tail-list-p (duplicated-members acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-rev

(defthm vl-simple-id-tail-list-p-of-rev
  (equal (vl-simple-id-tail-list-p (rev acl2::x))
         (vl-simple-id-tail-list-p (list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-rcons

(defthm vl-simple-id-tail-list-p-of-rcons
  (iff (vl-simple-id-tail-list-p (acl2::rcons acl2::a acl2::x))
       (and (vl-simple-id-tail-p acl2::a)
            (vl-simple-id-tail-list-p (list-fix acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-p-when-member-equal-of-vl-simple-id-tail-list-p

(defthm
  vl-simple-id-tail-p-when-member-equal-of-vl-simple-id-tail-list-p
  (and (implies (and (member-equal acl2::a acl2::x)
                     (vl-simple-id-tail-list-p acl2::x))
                (vl-simple-id-tail-p acl2::a))
       (implies (and (vl-simple-id-tail-list-p acl2::x)
                     (member-equal acl2::a acl2::x))
                (vl-simple-id-tail-p acl2::a)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-when-subsetp-equal

(defthm vl-simple-id-tail-list-p-when-subsetp-equal
  (and (implies (and (subsetp-equal acl2::x acl2::y)
                     (vl-simple-id-tail-list-p acl2::y))
                (vl-simple-id-tail-list-p acl2::x))
       (implies (and (vl-simple-id-tail-list-p acl2::y)
                     (subsetp-equal acl2::x acl2::y))
                (vl-simple-id-tail-list-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-set-equiv-congruence

(defthm vl-simple-id-tail-list-p-set-equiv-congruence
  (implies (set-equiv acl2::x acl2::y)
           (equal (vl-simple-id-tail-list-p acl2::x)
                  (vl-simple-id-tail-list-p acl2::y)))
  :rule-classes :congruence)

Theorem: vl-simple-id-tail-list-p-of-set-difference-equal

(defthm vl-simple-id-tail-list-p-of-set-difference-equal
 (implies
  (vl-simple-id-tail-list-p acl2::x)
  (vl-simple-id-tail-list-p (set-difference-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-intersection-equal-1

(defthm vl-simple-id-tail-list-p-of-intersection-equal-1
 (implies
    (vl-simple-id-tail-list-p (double-rewrite acl2::x))
    (vl-simple-id-tail-list-p (intersection-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-intersection-equal-2

(defthm vl-simple-id-tail-list-p-of-intersection-equal-2
 (implies
    (vl-simple-id-tail-list-p (double-rewrite acl2::y))
    (vl-simple-id-tail-list-p (intersection-equal acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-union-equal

(defthm vl-simple-id-tail-list-p-of-union-equal
  (equal (vl-simple-id-tail-list-p (union-equal acl2::x acl2::y))
         (and (vl-simple-id-tail-list-p (list-fix acl2::x))
              (vl-simple-id-tail-list-p (double-rewrite acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-take

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

Theorem: vl-simple-id-tail-list-p-of-repeat

(defthm vl-simple-id-tail-list-p-of-repeat
  (iff (vl-simple-id-tail-list-p (repeat acl2::n acl2::x))
       (or (vl-simple-id-tail-p acl2::x)
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-p-of-nth-when-vl-simple-id-tail-list-p

(defthm vl-simple-id-tail-p-of-nth-when-vl-simple-id-tail-list-p
  (implies (and (vl-simple-id-tail-list-p acl2::x)
                (< (nfix acl2::n) (len acl2::x)))
           (vl-simple-id-tail-p (nth acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-update-nth

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

Theorem: vl-simple-id-tail-list-p-of-butlast

(defthm vl-simple-id-tail-list-p-of-butlast
  (implies (vl-simple-id-tail-list-p (double-rewrite acl2::x))
           (vl-simple-id-tail-list-p (butlast acl2::x acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-nthcdr

(defthm vl-simple-id-tail-list-p-of-nthcdr
  (implies (vl-simple-id-tail-list-p (double-rewrite acl2::x))
           (vl-simple-id-tail-list-p (nthcdr acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-last

(defthm vl-simple-id-tail-list-p-of-last
  (implies (vl-simple-id-tail-list-p (double-rewrite acl2::x))
           (vl-simple-id-tail-list-p (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-remove

(defthm vl-simple-id-tail-list-p-of-remove
  (implies (vl-simple-id-tail-list-p acl2::x)
           (vl-simple-id-tail-list-p (remove acl2::a acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: vl-simple-id-tail-list-p-of-revappend

(defthm vl-simple-id-tail-list-p-of-revappend
  (equal (vl-simple-id-tail-list-p (revappend acl2::x acl2::y))
         (and (vl-simple-id-tail-list-p (list-fix acl2::x))
              (vl-simple-id-tail-list-p acl2::y)))
  :rule-classes ((:rewrite)))

Function: vl-read-while-simple-id-tail-impl

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

Function: vl-read-while-simple-id-tail$inline

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

Theorem: prefix-of-vl-read-while-simple-id-tail

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

Theorem: remainder-of-vl-read-while-simple-id-tail

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

Theorem: prefix-of-vl-read-while-simple-id-tail-when-vl-simple-id-tail-p

(defthm
    prefix-of-vl-read-while-simple-id-tail-when-vl-simple-id-tail-p
  (implies (vl-simple-id-tail-p (vl-echar->char (car echars)))
           (iff (mv-nth 0 (vl-read-while-simple-id-tail echars))
                (consp echars))))

Theorem: vl-read-while-simple-id-tail-sound

(defthm vl-read-while-simple-id-tail-sound
  (vl-simple-id-tail-list-p
       (vl-echarlist->chars
            (mv-nth 0
                    (vl-read-while-simple-id-tail echars)))))

Theorem: vl-read-while-simple-id-tail-complete

(defthm vl-read-while-simple-id-tail-complete
 (equal
    (vl-simple-id-tail-p
         (vl-echar->char
              (car (mv-nth 1
                           (vl-read-while-simple-id-tail echars)))))
    (if (consp (mv-nth 1
                       (vl-read-while-simple-id-tail echars)))
        nil
      (vl-simple-id-tail-p (vl-echar->char nil)))))

Theorem: append-of-vl-read-while-simple-id-tail

(defthm append-of-vl-read-while-simple-id-tail
  (equal (append (mv-nth 0 (vl-read-while-simple-id-tail echars))
                 (mv-nth 1
                         (vl-read-while-simple-id-tail echars)))
         echars))

Theorem: no-change-loser-of-vl-read-while-simple-id-tail

(defthm no-change-loser-of-vl-read-while-simple-id-tail
  (implies (not (mv-nth 0
                        (vl-read-while-simple-id-tail echars)))
           (equal (mv-nth 1 (vl-read-while-simple-id-tail echars))
                  echars)))

Theorem: acl2-count-of-vl-read-while-simple-id-tail-weak

(defthm acl2-count-of-vl-read-while-simple-id-tail-weak
  (<= (acl2-count (mv-nth 1
                          (vl-read-while-simple-id-tail echars)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-while-simple-id-tail-strong

(defthm acl2-count-of-vl-read-while-simple-id-tail-strong
 (implies
      (mv-nth 0 (vl-read-while-simple-id-tail echars))
      (< (acl2-count (mv-nth 1
                             (vl-read-while-simple-id-tail echars)))
         (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))