		Search-engine friendly clone of the ACL2 documentation.

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 (caadr x))
                     ((:vl-idtoken :vl-sysidtoken :vl-stringtoken
                                   :vl-timetoken :vl-extinttoken)
                      (cadr x))
                     (otherwise (cdr 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 (vl-plaintokentype-p type)))
          (equal (vl-token->etext (make-vl-plaintoken :type type
                                                      :etext etext))
                 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 (stringp expansion)))
   (equal
        (vl-token->etext (make-vl-stringtoken :etext etext
                                              :expansion expansion))
        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 (stringp name)))
           (equal (vl-token->etext (make-vl-idtoken :etext etext
                                                    :name name))
                  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 (stringp name)))
           (equal (vl-token->etext (make-vl-sysidtoken :etext etext
                                                       :name name))
                  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 (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))
         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)))
           (equal (vl-token->etext (make-vl-realtoken :etext etext))
                  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)))
       (equal (vl-token->etext (make-vl-timetoken :etext etext
                                                  :quantity quantity
                                                  :units units))
              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)))
       (equal (vl-token->etext (make-vl-extinttoken :etext etext
                                                    :value value))
              etext)))