• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
        • 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

• Extended-characters

Vl-echarlist-from-str

Transform an ordinary stringp into a vl-echarlist-p.

Signature

(vl-echarlist-from-str x &key (filename '"[internal string]") 
                       (line '1) 
                       (col '0)) 
 
  → 
echarlist

Arguments

x — Guard (stringp x).

filename — Guard (stringp filename).

line — Guard (posp line).

col — Guard (natp col).

This is like vl-echarlist-from-chars, but we process an ACL2 string instead of a character list.

We go to some lengths to be able to more efficiently construct an echarlist from a string. The simplest approach to this would be:

1. coerce the string into a list
2. call vl-echarlist-from-chars on the resulting list

The above is our logical definition, and hence we leave this function enabled and reason about vl-echarlist-from-chars instead. But for better efficiency, we avoid the coerce and process the string directly.

Definitions and Theorems

Function: vl-echarlist-from-str-fn

(defun vl-echarlist-from-str-fn (x filename line col)
 (declare (xargs :guard (and (stringp x)
                             (stringp filename)
                             (posp line)
                             (natp col))))
 (let ((__function__ 'vl-echarlist-from-str))
  (declare (ignorable __function__))
  (mbe :logic (vl-echarlist-from-chars-fn (explode x)
                                          filename line col)
       :exec (vl-echarlist-from-str-nice x 0 (length (the string x))
                                         filename line col))))

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

(defthm vl-echarlist-from-str-fn-of-str-fix-x
  (equal (vl-echarlist-from-str-fn (str-fix x)
                                   filename line col)
         (vl-echarlist-from-str-fn x filename line col)))

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

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

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

(defthm vl-echarlist-from-str-fn-of-str-fix-filename
  (equal (vl-echarlist-from-str-fn x (str-fix filename)
                                   line col)
         (vl-echarlist-from-str-fn x filename line col)))

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

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

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

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

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

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

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

(defthm vl-echarlist-from-str-fn-of-nfix-col
  (equal (vl-echarlist-from-str-fn x filename line (nfix col))
         (vl-echarlist-from-str-fn x filename line col)))

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

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

Subtopics

Vl-echarlist-from-str-nice

Vl-echarlist-from-str-aux