Get the type of a token.
(vl-token->type x) → type
For plain tokens, the symbol we return is the
For any other token, such as vl-inttoken-p or vl-idtoken-p
objects, the type is simply the
This is one of the most heavily used functions throughout our parser, so its
efficient implementation is beneficial. We specially arrange our definition of
vl-plaintoken-p so that the type of any token is always just its
Function:
(defun vl-token->type$inline (x) (declare (xargs :guard (vl-token-p x))) (let ((__function__ 'vl-token->type)) (declare (ignorable __function__)) (mbe :logic (if (vl-plaintoken-p x) (vl-plaintoken->type x) (tag x)) :exec (tag x))))
Theorem:
(defthm symbolp-of-vl-token->type (implies (and (force (vl-token-p x))) (b* ((type (vl-token->type$inline x))) (symbolp type))) :rule-classes :rewrite)
Theorem:
(defthm vl-token->type-possibilities (implies (vl-token-p x) (member (vl-token->type x) (append (list :vl-inttoken :vl-stringtoken :vl-idtoken :vl-sysidtoken :vl-realtoken :vl-timetoken :vl-extinttoken) *vl-plaintoken-types*))) :rule-classes nil)
Theorem:
(defthm vl-inttoken-p-when-token-of-type-inttoken (implies (and (equal (vl-token->type x) :vl-inttoken) (force (vl-token-p x))) (equal (vl-inttoken-p x) t)))
Theorem:
(defthm vl-stringtoken-p-when-token-of-type-stringtoken (implies (and (equal (vl-token->type x) :vl-stringtoken) (force (vl-token-p x))) (equal (vl-stringtoken-p x) t)))
Theorem:
(defthm vl-realtoken-p-when-token-of-type-realtoken (implies (and (equal (vl-token->type x) :vl-realtoken) (force (vl-token-p x))) (equal (vl-realtoken-p x) t)))
Theorem:
(defthm vl-timetoken-p-when-token-of-type-timetoken (implies (and (equal (vl-token->type x) :vl-timetoken) (force (vl-token-p x))) (equal (vl-timetoken-p x) t)))
Theorem:
(defthm vl-extinttoken-p-when-token-of-type-extinttoken (implies (and (equal (vl-token->type x) :vl-extinttoken) (force (vl-token-p x))) (equal (vl-extinttoken-p x) t)))
Theorem:
(defthm vl-idtoken-p-when-token-of-type-idtoken (implies (and (equal (vl-token->type x) :vl-idtoken) (force (vl-token-p x))) (equal (vl-idtoken-p x) t)))
Theorem:
(defthm vl-sysidtoken-p-when-token-of-type-sysidtoken (implies (and (equal (vl-token->type x) :vl-sysidtoken) (force (vl-token-p x))) (equal (vl-sysidtoken-p x) t)))