		Search-engine friendly clone of the ACL2 documentation.

Vl-emodwire-p

Vl-emodwire->index

Return the index of an vl-emodwire-p as a natural, or nil if there is no index.

For instance, the index of |opcode[3]| is 3, and the index of |reset| is nil.

Definitions and Theorems

Function: vl-emodwire->index

(defun vl-emodwire->index (x)
  (declare (xargs :guard (vl-emodwire-p x)))
  (and (mbt (vl-emodwire-p x))
       (b* ((name (symbol-name x))
            (open (position #\[ name))
            ((when (not open)) nil)
            (close (position #\] name))
            (index-str (subseq name (+ open 1) close))
            ((mv index-val ?len)
             (str::parse-nat-from-string
                  index-str 0 0 0 (length index-str))))
         index-val)))

Theorem: type-of-vl-emodwire->index

(defthm type-of-vl-emodwire->index
  (or (not (vl-emodwire->index x))
      (natp (vl-emodwire->index x)))
  :rule-classes :type-prescription)

Theorem: vl-emodwire->index-of-vl-emodwire

(defthm vl-emodwire->index-of-vl-emodwire
  (implies (and (force (stringp basename))
                (force (maybe-natp index))
                (force (or index (not (equal basename "NIL")))))
           (equal (vl-emodwire->index (vl-emodwire basename index))
                  index)))