• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
          • Vl-echar-p
            • Make-vl-echar-fast
            • Vl-echar->char
            • Vl-echar
            • Vl-echar->loc
            • Vl-echarpack-p
          • Vl-location
          • Vl-echarlist->chars
          • Vl-echarlist-from-chars
          • Vl-echarlist-from-str
          • Vl-echarlist-unsigned-value
          • Vl-change-echarlist-locations
          • Vl-echar-digit-value
          • Vl-echarlist->string
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-echar-p

Make-vl-echar-fast

Fast creation of extended characters that bypasses constructing vl-location objects.

Signature

(make-vl-echar-fast &key char filename line col) → *

Arguments

char — Guard (characterp char).

filename — Guard (stringp filename).

line — Guard (posp line).

col — Guard (natp col).

Definitions and Theorems

Function: make-vl-echar-fast$inline

(defun make-vl-echar-fast$inline (char filename line col)
 (declare (xargs :guard (and (characterp char)
                             (stringp filename)
                             (posp line)
                             (natp col))))
 (let ((__function__ 'make-vl-echar-fast))
  (declare (ignorable __function__))
  (mbe
   :logic (vl-echar char
                    (make-vl-location :filename filename
                                      :line line
                                      :col col))
   :exec (vl-echar-raw
              filename
              (vl-echarpack (the (unsigned-byte 8) (char-code char))
                            line col)))))

Theorem: make-vl-echar-fast$inline-of-char-fix-char

(defthm make-vl-echar-fast$inline-of-char-fix-char
  (equal (make-vl-echar-fast$inline (char-fix char)
                                    filename line col)
         (make-vl-echar-fast$inline char filename line col)))

Theorem: make-vl-echar-fast$inline-chareqv-congruence-on-char

(defthm make-vl-echar-fast$inline-chareqv-congruence-on-char
 (implies
   (chareqv char char-equiv)
   (equal (make-vl-echar-fast$inline char filename line col)
          (make-vl-echar-fast$inline char-equiv filename line col)))
 :rule-classes :congruence)

Theorem: make-vl-echar-fast$inline-of-str-fix-filename

(defthm make-vl-echar-fast$inline-of-str-fix-filename
  (equal (make-vl-echar-fast$inline char (str-fix filename)
                                    line col)
         (make-vl-echar-fast$inline char filename line col)))

Theorem: make-vl-echar-fast$inline-streqv-congruence-on-filename

(defthm make-vl-echar-fast$inline-streqv-congruence-on-filename
 (implies
   (streqv filename filename-equiv)
   (equal (make-vl-echar-fast$inline char filename line col)
          (make-vl-echar-fast$inline char filename-equiv line col)))
 :rule-classes :congruence)

Theorem: make-vl-echar-fast$inline-of-pos-fix-line

(defthm make-vl-echar-fast$inline-of-pos-fix-line
  (equal (make-vl-echar-fast$inline char filename (pos-fix line)
                                    col)
         (make-vl-echar-fast$inline char filename line col)))

Theorem: make-vl-echar-fast$inline-pos-equiv-congruence-on-line

(defthm make-vl-echar-fast$inline-pos-equiv-congruence-on-line
 (implies
   (acl2::pos-equiv line line-equiv)
   (equal (make-vl-echar-fast$inline char filename line col)
          (make-vl-echar-fast$inline char filename line-equiv col)))
 :rule-classes :congruence)

Theorem: make-vl-echar-fast$inline-of-nfix-col

(defthm make-vl-echar-fast$inline-of-nfix-col
  (equal (make-vl-echar-fast$inline char filename line (nfix col))
         (make-vl-echar-fast$inline char filename line col)))

Theorem: make-vl-echar-fast$inline-nat-equiv-congruence-on-col

(defthm make-vl-echar-fast$inline-nat-equiv-congruence-on-col
 (implies
   (acl2::nat-equiv col col-equiv)
   (equal (make-vl-echar-fast$inline char filename line col)
          (make-vl-echar-fast$inline char filename line col-equiv)))
 :rule-classes :congruence)