• 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-lex
          • Defchar
          • Tokens
            • Vl-tokentype-p
            • Vl-inttoken-p
            • Vl-plaintoken-p
            • Vl-token->etext
            • Vl-token-p
            • Vl-idtoken-p
            • Vl-token->type
            • Vl-timetoken-p
            • Vl-stringtoken-p
            • Vl-sysidtoken-p
            • Vl-extinttoken-p
            • Vl-realtoken-p
            • Vl-kill-whitespace-and-comments
            • Vl-tokenlist->etext
            • Vl-tokenlist-p
            • Vl-tokenlist->string-with-spaces
            • Vl-idtoken-list-p
            • Vl-tokentypelist-p
            • Vl-token->breakp
            • Vl-token->loc
            • Vl-plaintokentypelist-p
            • Vl-tokenlistlist-p
            • Vl-token->string
          • 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

• Tokens

Vl-token->etext

Get the original text for a token.

Signature

(vl-token->etext x) → etext

Arguments

x — Guard (vl-token-p x).

Returns

etext — Type (vl-echarlist-p etext), given the guard.

Each of the valid vl-token-p objects includes an etext field which reflects the original characters in the source code that led to the creation of that token. Accordingly, we can extract the etext from any token.

Definitions and Theorems

Function: vl-token->etext$inline

(defun vl-token->etext$inline (x)
  (declare (xargs :guard (vl-token-p x)))
  (let ((__function__ 'vl-token->etext))
    (declare (ignorable __function__))
    (mbe :logic (cond ((vl-inttoken-p x)
                       (vl-inttoken->etext x))
                      ((vl-idtoken-p x) (vl-idtoken->etext x))
                      ((vl-sysidtoken-p x)
                       (vl-sysidtoken->etext x))
                      ((vl-stringtoken-p x)
                       (vl-stringtoken->etext x))
                      ((vl-realtoken-p x)
                       (vl-realtoken->etext x))
                      ((vl-timetoken-p x)
                       (vl-timetoken->etext x))
                      ((vl-extinttoken-p x)
                       (vl-extinttoken->etext x))
                      ((vl-plaintoken-p x)
                       (vl-plaintoken->etext x)))
         :exec (case (tag x)
                     ((:vl-inttoken :vl-timetoken) (caadr x))
                     (otherwise (cadr x))))))

Theorem: vl-echarlist-p-of-vl-token->etext

(defthm vl-echarlist-p-of-vl-token->etext
  (implies (and (force (vl-token-p x)))
           (b* ((etext (vl-token->etext$inline x)))
             (vl-echarlist-p etext)))
  :rule-classes :rewrite)

Theorem: consp-of-vl-token->etext

(defthm consp-of-vl-token->etext
  (implies (force (vl-token-p x))
           (consp (vl-token->etext x))))

Theorem: true-listp-of-vl-token->etext

(defthm true-listp-of-vl-token->etext
  (implies (force (vl-token-p x))
           (true-listp (vl-token->etext x))))

Theorem: vl-token->etext-of-vl-plaintoken

(defthm vl-token->etext-of-vl-plaintoken
  (implies
       (and (force (vl-echarlist-p etext))
            (force (consp etext))
            (force (true-listp etext))
            (force (booleanp breakp))
            (force (vl-plaintokentype-p type)))
       (equal (vl-token->etext (make-vl-plaintoken :type type
                                                   :etext etext
                                                   :breakp breakp))
              etext)))

Theorem: vl-token->etext-of-vl-stringtoken

(defthm vl-token->etext-of-vl-stringtoken
 (implies
   (and (force (vl-echarlist-p etext))
        (force (consp etext))
        (force (true-listp etext))
        (force (booleanp breakp))
        (force (stringp expansion)))
   (equal (vl-token->etext (make-vl-stringtoken :etext etext
                                                :expansion expansion
                                                :breakp breakp))
          etext)))

Theorem: vl-token->etext-of-vl-idtoken

(defthm vl-token->etext-of-vl-idtoken
  (implies (and (force (vl-echarlist-p etext))
                (force (consp etext))
                (force (true-listp etext))
                (force (booleanp breakp))
                (force (stringp name)))
           (equal (vl-token->etext (make-vl-idtoken :etext etext
                                                    :name name
                                                    :breakp breakp))
                  etext)))

Theorem: vl-token->etext-of-vl-sysidtoken

(defthm vl-token->etext-of-vl-sysidtoken
  (implies
       (and (force (vl-echarlist-p etext))
            (force (consp etext))
            (force (true-listp etext))
            (force (booleanp breakp))
            (force (stringp name)))
       (equal (vl-token->etext (make-vl-sysidtoken :etext etext
                                                   :name name
                                                   :breakp breakp))
              etext)))

Theorem: vl-token->etext-of-vl-inttoken

(defthm vl-token->etext-of-vl-inttoken
 (implies
    (and (force (vl-echarlist-p etext))
         (force (consp etext))
         (force (true-listp etext))
         (force (booleanp breakp))
         (force (posp width))
         (force (booleanp signedp))
         (force (maybe-natp value))
         (force (vl-inttoken-constraint-p width value bits))
         (force (vl-bitlist-p bits))
         (force (booleanp wasunsized)))
    (equal (vl-token->etext (make-vl-inttoken :etext etext
                                              :width width
                                              :signedp signedp
                                              :value value
                                              :bits bits
                                              :wasunsized wasunsized
                                              :breakp breakp))
           etext)))

Theorem: vl-token->etext-of-vl-realtoken

(defthm vl-token->etext-of-vl-realtoken
  (implies
       (and (force (vl-echarlist-p etext))
            (force (consp etext))
            (force (true-listp etext))
            (force (booleanp breakp)))
       (equal (vl-token->etext (make-vl-realtoken :etext etext
                                                  :breakp breakp))
              etext)))

Theorem: vl-token->etext-of-vl-timetoken

(defthm vl-token->etext-of-vl-timetoken
  (implies
       (and (force (vl-echarlist-p etext))
            (force (consp etext))
            (force (true-listp etext))
            (force (stringp quantity))
            (force (vl-timeunit-p units))
            (force (booleanp breakp)))
       (equal (vl-token->etext (make-vl-timetoken :etext etext
                                                  :quantity quantity
                                                  :units units
                                                  :breakp breakp))
              etext)))

Theorem: vl-token->etext-of-vl-extinttoken

(defthm vl-token->etext-of-vl-extinttoken
  (implies
       (and (force (vl-echarlist-p etext))
            (force (consp etext))
            (force (true-listp etext))
            (force (vl-bit-p value))
            (force (booleanp breakp)))
       (equal (vl-token->etext (make-vl-extinttoken :etext etext
                                                    :value value
                                                    :breakp breakp))
              etext)))