• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Vl-loadstate
        • Lexer
        • 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-location
          • Vl-echar-p
          • Vl-echarlist->chars
          • Vl-echarlist-from-chars
          • Vl-echarlist-from-str
            • Vl-echarlist-from-str-nice
            • Vl-echarlist-from-str-aux
          • Vl-echarlist-unsigned-value
          • Vl-change-echarlist-locations
          • Vl-echar-digit-value
          • Vl-echarlist->string
        • 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

• Vl-echarlist-from-str

Vl-echarlist-from-str-nice

Signature

(vl-echarlist-from-str-nice x n xl filename line col) → *

Arguments

x — Guard (stringp x).

n — Guard (natp n).

xl — Guard (equal xl (length x)).

filename — Guard (stringp filename).

line — Guard (posp line).

col — Guard (natp col).

Definitions and Theorems

Function: vl-echarlist-from-str-nice

(defun vl-echarlist-from-str-nice (x n xl filename line col)
 (declare (xargs :guard (and (stringp x)
                             (natp n)
                             (stringp filename)
                             (posp line)
                             (natp col)
                             (equal xl (length x)))))
 (declare (type string x filename)
          (type integer n xl line col))
 (declare (xargs :split-types t :guard (<= n xl)))
 (let ((__function__ 'vl-echarlist-from-str-nice))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* (((when (zp (- (nfix xl) (nfix n)))) nil)
        (char (char-fix (char x n)))
        (line (pos-fix line))
        (col (nfix col))
        (echar (make-vl-echar-fast :char char
                                   :filename filename
                                   :line line
                                   :col col)))
     (cons echar
           (vl-echarlist-from-str-nice
                x (+ 1 (nfix n))
                xl filename
                (if (eql char #\Newline)
                    (+ 1 line)
                  line)
                (if (eql char #\Newline) 0 (+ 1 col)))))
   :exec
   (with-local-nrev
       (vl-echarlist-from-str-aux x n xl filename line col nrev)))))

Theorem: vl-echarlist-from-str-aux-correct

(defthm vl-echarlist-from-str-aux-correct
 (implies
  (and (posp line) (natp col))
  (equal
   (vl-echarlist-from-str-aux x n xl filename line col acc)
   (append acc
           (vl-echarlist-from-str-nice x n xl filename line col)))))

Theorem: vl-echarlist-from-str-nice-correct

(defthm vl-echarlist-from-str-nice-correct
  (equal (vl-echarlist-from-str-nice x n (len (explode x))
                                     filename line col)
         (vl-echarlist-from-chars-fn (nthcdr n (explode x))
                                     filename line col)))

Theorem: vl-echarlist-from-str-nice-of-str-fix-x

(defthm vl-echarlist-from-str-nice-of-str-fix-x
  (equal (vl-echarlist-from-str-nice (str-fix x)
                                     n xl filename line col)
         (vl-echarlist-from-str-nice x n xl filename line col)))

Theorem: vl-echarlist-from-str-nice-streqv-congruence-on-x

(defthm vl-echarlist-from-str-nice-streqv-congruence-on-x
 (implies
  (streqv x x-equiv)
  (equal
       (vl-echarlist-from-str-nice x n xl filename line col)
       (vl-echarlist-from-str-nice x-equiv n xl filename line col)))
 :rule-classes :congruence)

Theorem: vl-echarlist-from-str-nice-of-nfix-n

(defthm vl-echarlist-from-str-nice-of-nfix-n
  (equal (vl-echarlist-from-str-nice x (nfix n)
                                     xl filename line col)
         (vl-echarlist-from-str-nice x n xl filename line col)))

Theorem: vl-echarlist-from-str-nice-nat-equiv-congruence-on-n

(defthm vl-echarlist-from-str-nice-nat-equiv-congruence-on-n
 (implies
  (acl2::nat-equiv n n-equiv)
  (equal
       (vl-echarlist-from-str-nice x n xl filename line col)
       (vl-echarlist-from-str-nice x n-equiv xl filename line col)))
 :rule-classes :congruence)

Theorem: vl-echarlist-from-str-nice-of-str-fix-filename

(defthm vl-echarlist-from-str-nice-of-str-fix-filename
  (equal (vl-echarlist-from-str-nice x n xl (str-fix filename)
                                     line col)
         (vl-echarlist-from-str-nice x n xl filename line col)))

Theorem: vl-echarlist-from-str-nice-streqv-congruence-on-filename

(defthm vl-echarlist-from-str-nice-streqv-congruence-on-filename
 (implies
  (streqv filename filename-equiv)
  (equal
       (vl-echarlist-from-str-nice x n xl filename line col)
       (vl-echarlist-from-str-nice x n xl filename-equiv line col)))
 :rule-classes :congruence)

Theorem: vl-echarlist-from-str-nice-of-pos-fix-line

(defthm vl-echarlist-from-str-nice-of-pos-fix-line
  (equal (vl-echarlist-from-str-nice x n xl filename (pos-fix line)
                                     col)
         (vl-echarlist-from-str-nice x n xl filename line col)))

Theorem: vl-echarlist-from-str-nice-pos-equiv-congruence-on-line

(defthm vl-echarlist-from-str-nice-pos-equiv-congruence-on-line
 (implies
  (acl2::pos-equiv line line-equiv)
  (equal
       (vl-echarlist-from-str-nice x n xl filename line col)
       (vl-echarlist-from-str-nice x n xl filename line-equiv col)))
 :rule-classes :congruence)

Theorem: vl-echarlist-from-str-nice-of-nfix-col

(defthm vl-echarlist-from-str-nice-of-nfix-col
 (equal (vl-echarlist-from-str-nice x n xl filename line (nfix col))
        (vl-echarlist-from-str-nice x n xl filename line col)))

Theorem: vl-echarlist-from-str-nice-nat-equiv-congruence-on-col

(defthm vl-echarlist-from-str-nice-nat-equiv-congruence-on-col
 (implies
  (acl2::nat-equiv col col-equiv)
  (equal
       (vl-echarlist-from-str-nice x n xl filename line col)
       (vl-echarlist-from-str-nice x n xl filename line col-equiv)))
 :rule-classes :congruence)