Vl-keyword-lookup
Determine if a string is a Verilog keyword.
- Signature
(vl-keyword-lookup x table) → sym
- Arguments
- x — An identifier that has just been lexed, which may or may not
be a valid Verilog keyword.
Guard (stringp x).
- table — Table of currently acceptable keywords.
Guard (vl-keyword-table-p table).
- Returns
- sym — When x is a keyword, the associated :vl-kwd-??? symbol;
otherwise nil.
Definitions and Theorems
Function: vl-keyword-lookup$inline
(defun vl-keyword-lookup$inline (x table)
(declare (xargs :guard (and (stringp x)
(vl-keyword-table-p table))))
(let ((__function__ 'vl-keyword-lookup))
(declare (ignorable __function__))
(cdr (hons-get x table))))
Theorem: symbolp-of-vl-keyword-lookup
(defthm symbolp-of-vl-keyword-lookup
(implies (vl-keyword-table-p table)
(symbolp (vl-keyword-lookup x table))))
Subtopics
- Vl-plaintokentype-p-of-vl-keyword-lookup
- Dumb technical lemma showing that we always get a good plaintoken as
long as we're using a valid keyword table.
